Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case right.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₁) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

pp: case right.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₂) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

pp: case right.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₃) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

Tactic:
· convert! Triangle.dist_orthocenter_reflection_circumcenter t hj₂₃

Goal state after:
case right.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₂) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

case right.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₃) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t