English
If two sides of a triangle from a common vertex are equal, the base angles are equal.
Русский
Если две стороны равны, углы при вершинах у основания треугольника равны.
LaTeX
$$$\operatorname{dist}(p_1,p_2) = \operatorname{dist}(p_1,p_3) \Rightarrow \angle p_1 p_2 p_3 = \angle p_1 p_3 p_2$$$
Lean4
/-- **Isosceles Triangle Theorem**: Pons asinorum, angle-at-point form. -/
theorem angle_eq_angle_of_dist_eq {p₁ p₂ p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) : ∠ p₁ p₂ p₃ = ∠ p₁ p₃ p₂ :=
by
rw [dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃] at h
unfold angle
convert angle_sub_eq_angle_sub_rev_of_norm_eq h
· exact (vsub_sub_vsub_cancel_left p₃ p₂ p₁).symm
· exact (vsub_sub_vsub_cancel_left p₂ p₃ p₁).symm