English
The distance between the orthocenter and the reflection of the circumcenter in a side equals the circumradius.
Русский
Расстояние между ортоцентром и отражением центра окружности описанной в стороны равно радиусу описанной окружности.
LaTeX
$$$\operatorname{dist}(H, \text{reflection}_{\text{side}}(O)) = R.$$$
Lean4
/-- The distance from the orthocenter to the reflection of the
circumcenter in a side equals the circumradius. -/
theorem dist_orthocenter_reflection_circumcenter (t : Triangle ℝ P) {i₁ i₂ : Fin 3} (h : i₁ ≠ i₂) :
dist t.orthocenter (reflection (affineSpan ℝ (t.points '' { i₁, i₂ })) t.circumcenter) = t.circumradius :=
by
rw [← mul_self_inj_of_nonneg dist_nonneg t.circumradius_nonneg,
t.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter h, t.orthocenter_eq_mongePoint,
mongePoint_eq_affineCombination_of_pointsWithCircumcenter,
dist_affineCombination t.pointsWithCircumcenter (sum_mongePointWeightsWithCircumcenter _)
(sum_reflectionCircumcenterWeightsWithCircumcenter h)]
simp_rw [sum_pointsWithCircumcenter, Pi.sub_apply, mongePointWeightsWithCircumcenter,
reflectionCircumcenterWeightsWithCircumcenter]
have hu : ({ i₁, i₂ } : Finset (Fin 3)) ⊆ univ := subset_univ _
obtain ⟨i₃, hi₃, hi₃₁, hi₃₂⟩ : ∃ i₃, univ \ ({ i₁, i₂ } : Finset (Fin 3)) = { i₃ } ∧ i₃ ≠ i₁ ∧ i₃ ≠ i₂ := by
decide +revert
simp_rw [← sum_sdiff hu, hi₃]
norm_num [hi₃₁, hi₃₂]
