chore(Geometry/Euclidean/Angle/Sphere): address review

Author: Scarlett-le

Mathlib/Geometry/Euclidean/Angle/Sphere.lean

@@ -227,21 +227,26 @@ 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]
 
+/-- For a tangent line to a sphere, twice the oriented angle between the line and the radius at the
+tangent point equals `π`. -/
+theorem IsTangentAt.two_zsmul_oangle_eq_pi {s : Sphere P} {p q : P} {as : AffineSubspace ℝ P}
+    (h : s.IsTangentAt p as) (hq : q ∈ as) (hqp : q ≠ p) (hcp : s.center ≠ p) :
+    (2 : ℤ) • ∡ q 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 hqp hcp]
+  exact h.angle_eq_pi_div_two hq
+
 /-- **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 hcenter : s.center ≠ p₁ := (ne_center_of_mem_of_mem_of_ne hp₁ hp₃ hp₃p₁.symm).symm
   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₄)
+    have hright : (2 : ℤ) • ∡ p₄ p₁ s.center = π :=
+      htan.two_zsmul_oangle_eq_pi (right_mem_affineSpan_pair ℝ p₁ p₄) hp₄p₁ hcenter
     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