From 5000c5fa0bce7177e5d6d59e22bc6f9992308308 Mon Sep 17 00:00:00 2001
From: Scarlett-le <735979178@qq.com>
Date: Sun, 28 Jun 2026 18:07:37 +0800
Subject: [PATCH 1/2] feat(Geometry/Euclidean/Angle): the unoriented angle at
 the center in terms of the angle at the circumference

---
 Mathlib/Geometry/Euclidean/Angle/Sphere.lean | 40 ++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean
index eb8f55b8d8c157..8b6e32efd0eb42 100644
--- a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean
+++ b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean
@@ -179,6 +179,46 @@ theorem oangle_center_eq_two_zsmul_oangle {s : Sphere P} {p₁ p₂ p₃ : P} (h
   rw [oangle, oangle, o.oangle_eq_two_zsmul_oangle_sub_of_norm_eq_real _ _ hp₂ hp₁ hp₃] <;>
     simp [hp₂p₁, hp₂p₃]
 
+/-- The angle at the center of a circle equals twice the angle at the circumference, unoriented
+angle version, provided twice the angle at the circumference is at most `π`. -/
+theorem angle_center_eq_two_mul_angle_of_two_mul_angle_le_pi {s : Sphere P} {p₁ p₂ p₃ : P}
+    (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃)
+    (h : 2 * ∠ p₁ p₂ p₃ ≤ π) : ∠ p₁ s.center p₃ = 2 * ∠ p₁ p₂ p₃ := by
+  have hp₁c : p₁ ≠ s.center := by
+    rintro rfl
+    rw [center_mem_iff] at hp₁
+    exact hp₂p₁ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₁]))
+  have hp₃c : p₃ ≠ s.center := by
+    rintro rfl
+    rw [center_mem_iff] at hp₃
+    exact hp₂p₃ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₃]))
+  refine Real.injOn_cos ⟨angle_nonneg p₁ s.center p₃, angle_le_pi p₁ s.center p₃⟩
+    ⟨mul_nonneg zero_le_two (angle_nonneg p₁ p₂ p₃), h⟩ ?_
+  rw [← cos_oangle_eq_cos_angle hp₁c hp₃c,
+    oangle_center_eq_two_zsmul_oangle hp₁ hp₂ hp₃ hp₂p₁ hp₂p₃, Real.cos_two_mul,
+    ← cos_oangle_eq_cos_angle hp₂p₁.symm hp₂p₃.symm, two_zsmul, Real.Angle.cos_add]
+  nlinarith [Real.Angle.cos_sq_add_sin_sq (∡ p₁ p₂ p₃)]
+
+/-- The angle at the center of a circle is `2 * π` minus twice the angle at the circumference,
+unoriented angle version, provided twice the angle at the circumference is at least `π`. -/
+theorem angle_center_eq_two_pi_sub_two_mul_angle_of_pi_le_two_mul_angle {s : Sphere P}
+    {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁)
+    (hp₂p₃ : p₂ ≠ p₃) (h : π ≤ 2 * ∠ p₁ p₂ p₃) :
+    ∠ p₁ s.center p₃ = 2 * π - 2 * ∠ p₁ p₂ p₃ := by
+  have hp₁c : p₁ ≠ s.center := by
+    rintro rfl; rw [center_mem_iff] at hp₁
+    exact hp₂p₁ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₁]))
+  have hp₃c : p₃ ≠ s.center := by
+    rintro rfl; rw [center_mem_iff] at hp₃
+    exact hp₂p₃ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₃]))
+  refine Real.injOn_cos ⟨angle_nonneg p₁ s.center p₃, angle_le_pi p₁ s.center p₃⟩
+    ⟨by linarith [angle_le_pi p₁ p₂ p₃], by linarith⟩ ?_
+  rw [show (2 : ℝ) * π - 2 * ∠ p₁ p₂ p₃ = -(2 * ∠ p₁ p₂ p₃) + 2 * π by ring,
+    Real.cos_add_two_pi, Real.cos_neg, ← cos_oangle_eq_cos_angle hp₁c hp₃c,
+    oangle_center_eq_two_zsmul_oangle hp₁ hp₂ hp₃ hp₂p₁ hp₂p₃, Real.cos_two_mul,
+    ← cos_oangle_eq_cos_angle hp₂p₁.symm hp₂p₃.symm, two_zsmul, Real.Angle.cos_add]
+  nlinarith [Real.Angle.cos_sq_add_sin_sq (∡ p₁ p₂ p₃)]
+
 /-- Oriented angle version of "angles in same segment are equal" and "opposite angles of a
 cyclic quadrilateral add to π", for oriented angles mod π (for which those are the same result),
 represented here as equality of twice the angles. -/

From 6246b7289d1bf053b7bf0b5f28948f770dffe7cc Mon Sep 17 00:00:00 2001
From: Scarlett-le <735979178@qq.com>
Date: Mon, 29 Jun 2026 17:34:21 +0800
Subject: [PATCH 2/2] chore(Geometry/Euclidean/Angle/Sphere): simplify using
 ne_center_of_mem_of_mem_of_ne

---
 Mathlib/Geometry/Euclidean/Angle/Sphere.lean | 18 ++++--------------
 1 file changed, 4 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean
index 8b6e32efd0eb42..fe5ed66fc16932 100644
--- a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean
+++ b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean
@@ -184,14 +184,8 @@ angle version, provided twice the angle at the circumference is at most `π`. -/
 theorem angle_center_eq_two_mul_angle_of_two_mul_angle_le_pi {s : Sphere P} {p₁ p₂ p₃ : P}
     (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃)
     (h : 2 * ∠ p₁ p₂ p₃ ≤ π) : ∠ p₁ s.center p₃ = 2 * ∠ p₁ p₂ p₃ := by
-  have hp₁c : p₁ ≠ s.center := by
-    rintro rfl
-    rw [center_mem_iff] at hp₁
-    exact hp₂p₁ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₁]))
-  have hp₃c : p₃ ≠ s.center := by
-    rintro rfl
-    rw [center_mem_iff] at hp₃
-    exact hp₂p₃ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₃]))
+  have hp₁c : p₁ ≠ s.center := ne_center_of_mem_of_mem_of_ne hp₁ hp₂ hp₂p₁.symm
+  have hp₃c : p₃ ≠ s.center := ne_center_of_mem_of_mem_of_ne hp₃ hp₂ hp₂p₃.symm
   refine Real.injOn_cos ⟨angle_nonneg p₁ s.center p₃, angle_le_pi p₁ s.center p₃⟩
     ⟨mul_nonneg zero_le_two (angle_nonneg p₁ p₂ p₃), h⟩ ?_
   rw [← cos_oangle_eq_cos_angle hp₁c hp₃c,
@@ -205,12 +199,8 @@ theorem angle_center_eq_two_pi_sub_two_mul_angle_of_pi_le_two_mul_angle {s : Sph
     {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁)
     (hp₂p₃ : p₂ ≠ p₃) (h : π ≤ 2 * ∠ p₁ p₂ p₃) :
     ∠ p₁ s.center p₃ = 2 * π - 2 * ∠ p₁ p₂ p₃ := by
-  have hp₁c : p₁ ≠ s.center := by
-    rintro rfl; rw [center_mem_iff] at hp₁
-    exact hp₂p₁ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₁]))
-  have hp₃c : p₃ ≠ s.center := by
-    rintro rfl; rw [center_mem_iff] at hp₃
-    exact hp₂p₃ (dist_eq_zero.mp (by rw [mem_sphere.mp hp₂, hp₃]))
+  have hp₁c : p₁ ≠ s.center := ne_center_of_mem_of_mem_of_ne hp₁ hp₂ hp₂p₁.symm
+  have hp₃c : p₃ ≠ s.center := ne_center_of_mem_of_mem_of_ne hp₃ hp₂ hp₂p₃.symm
   refine Real.injOn_cos ⟨angle_nonneg p₁ s.center p₃, angle_le_pi p₁ s.center p₃⟩
     ⟨by linarith [angle_le_pi p₁ p₂ p₃], by linarith⟩ ?_
   rw [show (2 : ℝ) * π - 2 * ∠ p₁ p₂ p₃ = -(2 * ∠ p₁ p₂ p₃) + 2 * π by ring,