English
In a triangle, the sum of external angle and two adjacent interior angles equals the apex angle.
Русский
В треугольнике сумма внешнего угла и двух соседних внутренних углов равна углу вершины.
LaTeX
$$$\angle(b,a,p) + \angle(p,a,c) = \angle(b,a,c)$$$
Lean4
/-- Given a triangle `ABC` with `A ≠ B` and `A ≠ C` and a point `P` on `BC`,
`∠ B A P + ∠ P A C = ∠ B A C`. -/
theorem angle_add_of_ne_of_ne {a b c p : P} (hb : a ≠ b) (hc : a ≠ c) (hp : Wbtw ℝ b p c) :
∠ b a p + ∠ p a c = ∠ b a c := by
by_cases pb : p = b; · simpa [pb] using angle_self_of_ne hb.symm
by_cases pc : p = c; · simpa [pc] using angle_self_of_ne hc.symm
have ea := angle_add_angle_add_angle_eq_pi c hb
have eb := angle_add_angle_add_angle_eq_pi p hb
have ec := angle_add_angle_add_angle_eq_pi p hc.symm
replace hp : ∠ b p c = π := angle_eq_pi_iff_sbtw.mpr ⟨hp, pb, pc⟩
have hp' : ∠ c p b = π := by rwa [angle_comm] at hp
rw [angle_comm p b a, angle_eq_angle_of_angle_eq_pi a hp, angle_comm a b c] at eb
rw [angle_eq_angle_of_angle_eq_pi a hp', angle_comm c p a] at ec
have ep := angle_add_angle_eq_pi_of_angle_eq_pi a hp
linarith only [ea, eb, ec, ep]
