Angles and incenters and excenters.

This file proves lemmas relating incenters and excenters of a simplex to angle bisection.

theorem Affine.Simplex.ExcenterExists.angle_excenter_touchpoint_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) {p : P} {i₁ i₂ : Fin (n + 1)} (hp₁ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) (hp₂ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) : EuclideanGeometry.angle (s.excenter signs) p (s.touchpoint signs i₁) = EuclideanGeometry.angle (s.excenter signs) p (s.touchpoint signs i₂)

An excenter of a simplex bisects the angle at a point shared between two faces, as measured between that excenter and its touchpoints on those faces.

theorem Affine.Simplex.angle_incenter_touchpoint_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {p : P} {i₁ i₂ : Fin (n + 1)} (hp₁ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) (hp₂ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) : EuclideanGeometry.angle s.incenter p (s.touchpoint ∅ i₁) = EuclideanGeometry.angle s.incenter p (s.touchpoint ∅ i₂)

The incenter of a simplex bisects the angle at a point shared between two faces, as measured between the incenter and its touchpoints on those faces.

theorem Affine.Simplex.exists_excenterExists_and_eq_excenter_of_forall_angle_orthogonalProjectionSpan_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex ℝ P n} {p : P} (hp : p ∈ affineSpan ℝ (Set.range s.points)) {i₁ : Fin (n + 1)} (h : ∀ (i₂ : Fin (n + 1)), i₂ ≠ i₁ → ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points), p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧ EuclideanGeometry.angle p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) = EuclideanGeometry.angle p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)) : ∃ (signs : Finset (Fin (n + 1))), s.ExcenterExists signs ∧ p = s.excenter signs

Given a face of a simplex, if a point bisects the angle between that face and each other face, as measured at points shared between those faces between that point and its projections onto the faces, that point is an excenter of the simplex.

theorem Affine.Triangle.dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {p : P} : dist p ↑((Simplex.faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((Simplex.faceOpposite t i₂).orthogonalProjectionSpan p) ↔ 2 • EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p = 2 • EuclideanGeometry.oangle p (t.points i₁) (t.points i₃)

A point p is equidistant to two sides of a triangle if and only if the oriented angles at their common vertex are equal modulo π.

theorem Affine.Triangle.two_zsmul_oangle_excenter_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) (signs : Finset (Fin 3)) : 2 • EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Simplex.excenter t signs) = 2 • EuclideanGeometry.oangle (Simplex.excenter t signs) (t.points i₁) (t.points i₃)

An excenter of a triangle bisects the angle at a vertex modulo π.

theorem Affine.Triangle.oangle_incenter_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Simplex.incenter t) = EuclideanGeometry.oangle (Simplex.incenter t) (t.points i₁) (t.points i₃)

The incenter of a triangle bisects the angle at a vertex.

theorem Affine.Triangle.oangle_excenter_singleton_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Simplex.excenter t {i₁}) = EuclideanGeometry.oangle (Simplex.excenter t {i₁}) (t.points i₁) (t.points i₃)

The excenter of a triangle opposite a vertex bisects the angle at that vertex.

theorem Affine.Triangle.oangle_excenter_singleton_eq_add_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.oangle (t.points i₁) (t.points i₂) (Simplex.excenter t {i₁}) = EuclideanGeometry.oangle (Simplex.excenter t {i₁}) (t.points i₂) (t.points i₃) + ↑Real.pi

The excenter of a triangle opposite a vertex bisects the exterior angle at another vertex (that is, the interior angles between vertices and the excenter differ by π).

theorem Affine.Triangle.eq_excenter_of_two_zsmul_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {p : P} (h₁ : 2 • EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p = 2 • EuclideanGeometry.oangle p (t.points i₁) (t.points i₃)) (h₂ : 2 • EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p = 2 • EuclideanGeometry.oangle p (t.points i₂) (t.points i₁)) : ∃ (signs : Finset (Fin 3)), p = Simplex.excenter t signs

A point lying on angle bisectors from two vertices is an excenter.

theorem Affine.Triangle.eq_incenter_or_eq_excenter_singleton_of_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {signs : Finset (Fin 3)} (h : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Simplex.excenter t signs) = EuclideanGeometry.oangle (Simplex.excenter t signs) (t.points i₁) (t.points i₃)) : Simplex.excenter t signs = Simplex.incenter t ∨ Simplex.excenter t signs = Simplex.excenter t {i₁}

An excenter lying on the internal angle bisector from a vertex is either the incenter or the excenter opposite that vertex.

theorem Affine.Triangle.eq_excenter_singleton_of_oangle_eq_add_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {signs : Finset (Fin 3)} (h : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Simplex.excenter t signs) = EuclideanGeometry.oangle (Simplex.excenter t signs) (t.points i₁) (t.points i₃) + ↑Real.pi) : Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}

An excenter lying on the external angle bisector from a vertex is the excenter opposite another vertex.

theorem Affine.Triangle.eq_incenter_of_oangle_eq {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {p : P} (h₁ : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p = EuclideanGeometry.oangle p (t.points i₁) (t.points i₃)) (h₂ : EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p = EuclideanGeometry.oangle p (t.points i₂) (t.points i₁)) : p = Simplex.incenter t

A point lying on two internal angle bisectors is the incenter.

theorem Affine.Triangle.eq_excenter_singleton_of_oangle_eq_of_oangle_eq_add_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {p : P} (h₁ : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p = EuclideanGeometry.oangle p (t.points i₁) (t.points i₃)) (h₂ : EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p = EuclideanGeometry.oangle p (t.points i₂) (t.points i₁) + ↑Real.pi) : p = Simplex.excenter t {i₁}

A point lying on the internal angle bisector from vertex i₁ and the external angle bisector from another vertex is the excenter opposite vertex i₁.

theorem Affine.Triangle.eq_excenter_singleton_of_oangle_eq_add_pi_of_oangle_eq_add_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {t : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) {p : P} (h₁ : EuclideanGeometry.oangle (t.points i₂) (t.points i₁) p = EuclideanGeometry.oangle p (t.points i₁) (t.points i₃) + ↑Real.pi) (h₂ : EuclideanGeometry.oangle (t.points i₃) (t.points i₂) p = EuclideanGeometry.oangle p (t.points i₂) (t.points i₁) + ↑Real.pi) : p = Simplex.excenter t {i₃}

A point lying on two external angle bisectors is the excenter opposite the third vertex.

theorem Affine.Triangle.angle_incenter_eq_angle_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Simplex.incenter t) = EuclideanGeometry.angle (t.points i₂) (t.points i₁) (t.points i₃) / 2

The incenter of a triangle bisects the angle at a vertex.

theorem Affine.Triangle.two_mul_angle_incenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : 2 * EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Simplex.incenter t) = EuclideanGeometry.angle (t.points i₂) (t.points i₁) (t.points i₃)

The incenter of a triangle bisects the angle at a vertex.

theorem Affine.Triangle.angle_incenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Simplex.incenter t) = EuclideanGeometry.angle (Simplex.incenter t) (t.points i₁) (t.points i₃)

The incenter of a triangle bisects the angle at a vertex.

theorem Affine.Triangle.angle_excenter_singleton_eq_angle_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Simplex.excenter t {i₁}) = EuclideanGeometry.angle (t.points i₂) (t.points i₁) (t.points i₃) / 2

The excenter of a triangle opposite a vertex bisects the angle at that vertex.

theorem Affine.Triangle.two_mul_angle_excenter_singleton {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : 2 * EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Simplex.excenter t {i₁}) = EuclideanGeometry.angle (t.points i₂) (t.points i₁) (t.points i₃)

The excenter of a triangle opposite a vertex bisects the angle at that vertex.

theorem Affine.Triangle.angle_excenter_singleton {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Simplex.excenter t {i₁}) = EuclideanGeometry.angle (Simplex.excenter t {i₁}) (t.points i₁) (t.points i₃)

The excenter of a triangle opposite a vertex bisects the angle at that vertex.

theorem Affine.Triangle.angle_excenter_singleton_eq_angle_add_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₁) (t.points i₂) (Simplex.excenter t {i₁}) = (EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃) + Real.pi) / 2

The excenter of a triangle opposite a vertex bisects the angle at another vertex.

theorem Affine.Triangle.two_mul_angle_excenter_singleton_eq_angle_add_pi {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : 2 * EuclideanGeometry.angle (t.points i₁) (t.points i₂) (Simplex.excenter t {i₁}) = EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃) + Real.pi

The excenter of a triangle opposite a vertex bisects the angle at another vertex.

theorem Affine.Triangle.angle_excenter_singleton_eq_pi_sub_angle_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₃) (t.points i₂) (Simplex.excenter t {i₁}) = (Real.pi - EuclideanGeometry.angle (t.points i₃) (t.points i₂) (t.points i₁)) / 2

The excenter of a triangle opposite a vertex bisects the angle at another vertex.

theorem Affine.Triangle.two_mul_angle_excenter_singleton_eq_pi_sub_angle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : 2 * EuclideanGeometry.angle (t.points i₃) (t.points i₂) (Simplex.excenter t {i₁}) = Real.pi - EuclideanGeometry.angle (t.points i₃) (t.points i₂) (t.points i₁)

The excenter of a triangle opposite a vertex bisects the angle at another vertex.

theorem Affine.Triangle.angle_excenter_singleton_sub {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₁) (t.points i₂) (Simplex.excenter t {i₁}) - EuclideanGeometry.angle (t.points i₃) (t.points i₂) (Simplex.excenter t {i₁}) = EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃)

The excenter of a triangle opposite a vertex bisects the angle at another vertex.

theorem Affine.Triangle.dist_nsPole_point_eq_dist_nsPole_excenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) (signs : Finset (Fin 3)) {i₁ i₂ : Fin 3} (h₁₂ : i₁ ≠ i₂) : dist (Simplex.nsPole t signs i₁) (t.points i₂) = dist (Simplex.nsPole t signs i₁) (Simplex.excenter t signs)

The incenter-excenter lemma, trillium theorem, trident lemma or north/south pole theorem: given a triangle ABC, suppose an angle bisector from A through the incenter or excenter I meets the circumcircle again at X (including the case of an external bisector at A tangent to the circle, in which case X = A). Then XB = XI (= XC, by applying this lemma again).

theorem Affine.Triangle.dist_southPole_point_eq_dist_southPole_incenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ : Fin 3} (h₁₂ : i₁ ≠ i₂) : dist (Simplex.southPole t i₁) (t.points i₂) = dist (Simplex.southPole t i₁) (Simplex.incenter t)

The incenter-excenter lemma, trillium theorem, trident lemma or south pole theorem: given a triangle ABC, suppose the angle bisector from A through the incenter I meets the circumcircle again at S. Then SB = SI (= SC, by applying this lemma again).

theorem Affine.Triangle.dist_southPole_point_eq_dist_southPole_excenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ : Fin 3} (h₁₂ : i₁ ≠ i₂) : dist (Simplex.southPole t i₁) (t.points i₂) = dist (Simplex.southPole t i₁) (Simplex.excenter t {i₁})

The incenter-excenter lemma, trillium theorem, trident lemma or south pole theorem: given a triangle ABC, suppose the angle bisector from A through the excenter I opposite A meets the circumcircle again at S. Then SB = SI (= SC, by applying this lemma again).

theorem Affine.Triangle.dist_northPole_point_eq_dist_northPole_excenter {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ : Fin 3} (h₁₂ : i₁ ≠ i₂) : dist (t.northPole i₁) (t.points i₂) = dist (t.northPole i₁) (Simplex.excenter t {i₂})

The incenter-excenter lemma, trillium theorem, trident lemma or north pole theorem: given a triangle ABC, suppose the angle bisector from A through the excenters not opposite A meets the circumcircle again at N. Then NB = NI (= NC, by applying this lemma again).