English
If two triangles have two equal angles and the included side equal, then the triangles are congruent (assuming non-degeneracy constraint).
Русский
Если два треугольника имеют два равных угла и равную включенную сторону, то треугольники конгруэнтны (при условии небездоровости).
LaTeX
$$$\text{If } \angle ABC = \angle A'B'C',\ dist(AB)=dist(A'B'),\ dist(BC)=dist(B'C'), \text{and nondegeneracy holds} \Rightarrow ![A,B,C] \cong ![A',B',C']$$$
Lean4
/-- **Angle–Side–Angle (ASA) congruence**
If two triangles have two equal angles and the included side equal, then the triangles are
congruent. We require that one of the triangles is non-degenerate, the non-collinearity of the
other is then implied by the given equalities.
-/
theorem angle_side_angle (h : ¬Collinear ℝ { a, b, c }) (ha₁ : ∠ a b c = ∠ a' b' c') (hd : dist b c = dist b' c')
(ha₂ : ∠ b c a = ∠ b' c' a') : ![a, b, c] ≅ ![a', b', c'] :=
by
have h' : ¬Collinear ℝ { a', b', c' } := by
grind only [collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, angle_self_right, angle_self_left, dist_eq_zero,
Set.insert_comm, Set.pair_comm]
have ha₃ := angle_add_angle_add_angle_eq_pi b (ne₁₃_of_not_collinear h)
have ha₃' := angle_add_angle_add_angle_eq_pi b' (ne₁₃_of_not_collinear h')
simp only [← ha₃', ha₁, ha₂, angle_comm b' c' a', add_right_cancel_iff] at ha₃
have h_bac : ¬Collinear ℝ { b, a, c } := by simpa [Set.insert_comm] using h
have h_bac' : ¬Collinear ℝ { b', a', c' } := by simpa [Set.insert_comm] using h'
have dist_ab_eq : dist a b = dist a' b' := by
rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd, angle_comm, ha₂,
angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
exact side_angle_side ha₁ dist_ab_eq hd
