feat(Geometry/Euclidean/Angle): add the Alternate segment theorem

Author: Scarlett-le

Mathlib/Geometry/Euclidean/Angle/Sphere.lean

@@ -227,6 +227,28 @@ theorem two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi {s : Sphere P} {p₁
   rw [← oangle_center_eq_two_zsmul_oangle hp₁ hp₂ hp₃ hp₂p₁ hp₂p₃,
     oangle_eq_pi_sub_two_zsmul_oangle_center_right hp₁ hp₃ hp₁p₃, add_sub_cancel]
 
+/-- **Alternate segment theorem**: Oriented angle version of "the angle between a tangent and
+a chord equals the inscribed angle subtending that chord", for oriented angles mod π,
+represented here as equality of twice the angles. -/
+theorem two_zsmul_oangle_tangent_eq {s : Sphere P} {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
+    (hp₃ : p₃ ∈ s) (htan : s.IsTangentAt p₁ line[ℝ, p₁, p₄]) (hp₄p₁ : p₄ ≠ p₁) (hp₃p₁ : p₃ ≠ p₁)
+    (hp₃p₂ : p₃ ≠ p₂) (hp₂p₁ : p₂ ≠ p₁) :
+    (2 : ℤ) • ∡ p₄ p₁ p₂ = (2 : ℤ) • ∡ p₁ p₃ p₂ := by
+  have hcenter : s.center ≠ p₁ := by
+    rintro rfl
+    exact hp₃p₁ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₃, ← mem_sphere.mp hp₁, dist_self]))
+  have htan_chord : (2 : ℤ) • ∡ p₄ p₁ p₂ = π + (2 : ℤ) • ∡ s.center p₁ p₂ := by
+    have hright : (2 : ℤ) • ∡ p₄ p₁ s.center = π := by
+      rw [Real.Angle.two_zsmul_eq_pi_iff, ← Real.Angle.abs_toReal_eq_pi_div_two_iff,
+        ← angle_eq_abs_oangle_toReal hp₄p₁ hcenter]
+      exact htan.angle_eq_pi_div_two (right_mem_affineSpan_pair ℝ p₁ p₄)
+    rw [← oangle_add hp₄p₁ hcenter hp₂p₁, smul_add, hright]
+  have hinscribed : (2 : ℤ) • ∡ p₁ p₃ p₂ = π + (2 : ℤ) • ∡ s.center p₁ p₂ := by
+    have h := two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₃ hp₂ hp₃p₁ hp₃p₂ hp₂p₁.symm
+    rw [oangle_rev, smul_neg] at h
+    rw [← h]; abel
+  exact htan_chord.trans hinscribed.symm
+
 /-- A base angle of an isosceles triangle with apex at the center of a circle is acute. -/
 theorem abs_oangle_center_left_toReal_lt_pi_div_two {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s)
     (hp₂ : p₂ ∈ s) : |(∡ s.center p₂ p₁).toReal| < π / 2 :=