English
If ∠BCD = π, then ∠ABC = ∠ABD.
Русский
Если ∠BCD = π, тогда ∠ABC = ∠ABD.
LaTeX
$$$\angle B C D = \pi \Rightarrow \angle A B C = \angle A B D$$$
Lean4
/-- If the second of three points is strictly between the other two, the angle at that point
is π. -/
theorem _root_.Sbtw.angle₁₂₃_eq_pi {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : ∠ p₁ p₂ p₃ = π :=
by
rw [angle, angle_eq_pi_iff]
rcases h with ⟨⟨r, ⟨hr0, hr1⟩, hp₂⟩, hp₂p₁, hp₂p₃⟩
refine ⟨vsub_ne_zero.2 hp₂p₁.symm, -(1 - r) / r, ?_⟩
have hr0' : r ≠ 0 := by
rintro rfl
rw [← hp₂] at hp₂p₁
simp at hp₂p₁
have hr1' : r ≠ 1 := by
rintro rfl
rw [← hp₂] at hp₂p₃
simp at hp₂p₃
replace hr0 := hr0.lt_of_ne hr0'.symm
replace hr1 := hr1.lt_of_ne hr1'
refine ⟨div_neg_of_neg_of_pos (Left.neg_neg_iff.2 (sub_pos.2 hr1)) hr0, ?_⟩
rw [← hp₂, AffineMap.lineMap_apply, vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, vsub_self, zero_sub, smul_neg,
smul_smul, div_mul_cancel₀ _ hr0', neg_smul, neg_neg, sub_eq_iff_eq_add, ← add_smul, sub_add_cancel, one_smul]
