English
A triangle is equilateral iff the three pairwise distances are equal; equivalently dist01 = dist02 and dist01 = dist12.
Русский
Треугольник равносторонний тогда и только тогда, когда три расстояния между вершинами равны: dist01 = dist02 и dist01 = dist12.
LaTeX
$$$\text{Equilateral}(t) \iff dist(t.p0,t.p1) = dist(t.p0,t.p2) \land dist(t.p0,t.p1) = dist(t.p1,t.p2)$$$
Lean4
theorem equilateral_iff_dist_eq_and_dist_eq {t : Triangle R P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃)
(h₂₃ : i₂ ≠ i₃) :
t.Equilateral ↔
dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃) :=
by
refine ⟨fun ⟨r, hr⟩ ↦ ?_, fun h ↦ ?_⟩
· simp [hr _ _ h₁₂, hr _ _ h₁₃, hr _ _ h₂₃]
· refine ⟨dist (t.points i₁) (t.points i₂), ?_⟩
intro i j hij
have hi :
(i = i₁ ∧ j = i₂) ∨
(i = i₂ ∧ j = i₁) ∨ (i = i₁ ∧ j = i₃) ∨ (i = i₃ ∧ j = i₁) ∨ (i = i₂ ∧ j = i₃) ∨ (i = i₃ ∧ j = i₂) :=
by
clear h
decide +revert
rcases h with ⟨h₁, h₂⟩
rcases hi with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩
· rfl
· exact dist_comm _ _
· exact h₁.symm
· rw [h₁, dist_comm]
· rw [h₂, dist_comm]
· rw [h₂, dist_comm]
