English
Two triangles are congruent if the three side lengths match; equivalently, the corresponding distance matrices are equal.
Русский
Два треугольника конгруэнтны, если три его стороны равны соответствующим сторонам другого треугольника.
LaTeX
$$$\forall i,j \in \{0,1,2\}, dist(t_1(i),t_1(j)) = dist(t_2(i),t_2(j)) \Rightarrow t_1 \cong t_2$$$
Lean4
/-- **Side–Side–Side (SSS) congruence**
If all three corresponding sides of two triangles are equal, then the triangles are congruent.
This holds even if the triangles are degenerate. -/
theorem side_side_side (hd₁ : dist a b = dist a' b') (hd₂ : dist b c = dist b' c') (hd₃ : dist c a = dist c' a') :
![a, b, c] ≅ ![a', b', c'] := by
rw [triangle_congruent_iff_dist_eq]
intro i j
fin_cases i <;> fin_cases j <;> simp_all [dist_comm]
