English
The line through the orthocenter and a vertex is contained in the corresponding altitude.
Русский
Прямая, проходящая через ортоцентр и вершину, содержится в соответствующей высоте.
LaTeX
$$$\operatorname{affineSpan}(\{t.\text{orthocenter}, t.\text{points}_i\}) \subseteq t.\text{altitude}_i$$$
Lean4
/-- The orthocenter is the only point lying in any two of the
altitudes. -/
theorem eq_orthocenter_of_forall_mem_altitude {t : Triangle ℝ P} {i₁ i₂ : Fin 3} {p : P} (h₁₂ : i₁ ≠ i₂)
(h₁ : p ∈ t.altitude i₁) (h₂ : p ∈ t.altitude i₂) : p = t.orthocenter :=
by
obtain ⟨i₃, h₂₃, h₁₃⟩ : ∃ i₃, i₂ ≠ i₃ ∧ i₁ ≠ i₃ := by
clear h₁ h₂
decide +revert
rw [t.altitude_eq_mongePlane h₁₃ h₁₂ h₂₃.symm] at h₁
rw [t.altitude_eq_mongePlane h₂₃ h₁₂.symm h₁₃.symm] at h₂
rw [orthocenter_eq_mongePoint]
have ha : ∀ i, i₃ ≠ i → p ∈ t.mongePlane i₃ i := by
intro i hi
obtain rfl | rfl : i₁ = i ∨ i₂ = i := by cutsat
all_goals assumption
exact eq_mongePoint_of_forall_mem_mongePlane ha
