From 320fd22f4931871b2ff998bf594be8a5c61d73da Mon Sep 17 00:00:00 2001
From: Scarlett-le <735979178@qq.com>
Date: Mon, 29 Jun 2026 15:58:42 +0800
Subject: [PATCH 1/2] feat(Geometry/Euclidean/Sphere): add lemmas about points
 on a sphere

---
 Mathlib/Geometry/Euclidean/Sphere/Basic.lean | 32 +++++++++++++++++---
 1 file changed, 28 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Geometry/Euclidean/Sphere/Basic.lean b/Mathlib/Geometry/Euclidean/Sphere/Basic.lean
index e641855739337f..ce5bf9b85d6f92 100644
--- a/Mathlib/Geometry/Euclidean/Sphere/Basic.lean
+++ b/Mathlib/Geometry/Euclidean/Sphere/Basic.lean
@@ -138,6 +138,13 @@ lemma Sphere.radius_nonneg_of_mem {s : Sphere P} {p : P} (h : p ∈ s) : 0 ≤ s
 @[simp] lemma Sphere.center_mem_iff {s : Sphere P} : s.center ∈ s ↔ s.radius = 0 := by
   simp [mem_sphere, eq_comm]
 
+/-- A point of a sphere that differs from another point of the sphere is not its center. -/
+lemma Sphere.ne_center_of_mem_of_mem_of_ne {s : Sphere P} {p q : P}
+    (hp : p ∈ s) (hq : q ∈ s) (hpq : p ≠ q) : p ≠ s.center := by
+  rintro rfl
+  rw [Sphere.center_mem_iff] at hp
+  exact hpq (dist_eq_zero.mp (by rw [mem_sphere.mp hq, hp])).symm
+
 /-- A set of points is cospherical if they are equidistant from some
 point. In two dimensions, this is the same thing as being
 concyclic. -/
@@ -206,6 +213,12 @@ theorem Cospherical.subtype_val {S : AffineSubspace ℝ P} [Nonempty S] {ps : Se
     (hps : Cospherical ps) : Cospherical (Subtype.val '' ps) :=
   Isometry.cospherical S.subtypeₐᵢ.isometry hps
 
+omit [NormedSpace ℝ V] in
+/-- For a point on a sphere, the norm of its displacement from the center equals the radius. -/
+theorem norm_vsub_center_eq_radius {s : Sphere P} {p : P} (hp : p ∈ s) :
+    ‖p -ᵥ s.center‖ = s.radius := by
+  rw [← dist_eq_norm_vsub']; exact mem_sphere'.mp hp
+
 lemma Sphere.nonempty_iff [Nontrivial V] {s : Sphere P} : (s : Set P).Nonempty ↔ 0 ≤ s.radius := by
   refine ⟨fun ⟨p, hp⟩ ↦ radius_nonneg_of_mem hp, fun h ↦ ?_⟩
   obtain ⟨v, hv⟩ := (NormedSpace.sphere_nonempty (x := (0 : V)) (r := s.radius)).2 h
@@ -456,8 +469,8 @@ theorem Sphere.dist_center_lt_radius_of_sbtw {p₁ p₂ p : P} {s : Sphere P}
   have ht₁' : t < 1 := lt_of_le_of_ne ht₁ fun h => hne₂ <| by
     rw [← hpt, h, AffineMap.lineMap_apply_one]
   set u := p₁ -ᵥ o; set v := p₂ -ᵥ o
-  have hu : ‖u‖ = s.radius := by rw [← dist_eq_norm_vsub]; exact mem_sphere.mp hp₁
-  have hv : ‖v‖ = s.radius := by rw [← dist_eq_norm_vsub]; exact mem_sphere.mp hp₂
+  have hu : ‖u‖ = s.radius := norm_vsub_center_eq_radius hp₁
+  have hv : ‖v‖ = s.radius := norm_vsub_center_eq_radius hp₂
   have huv : u ≠ v := fun h => hne₁ <| by
     rw [← hpt, vsub_left_cancel h, AffineMap.lineMap_same, AffineMap.const_apply]
   have hpo : p -ᵥ o = (1 - t) • u + t • v := by
@@ -551,8 +564,8 @@ the radius vector at one endpoint is negative. -/
 theorem inner_vsub_center_vsub_pos {p₁ p₂ : P} {s : Sphere P}
     (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₁p₂ : p₁ ≠ p₂) :
     0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫ := by
-  have hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius := by rw [← dist_eq_norm_vsub']; exact mem_sphere'.mp hp₁
-  have hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius := by rw [← dist_eq_norm_vsub']; exact mem_sphere'.mp hp₂
+  have hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius := norm_vsub_center_eq_radius hp₁
+  have hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius := norm_vsub_center_eq_radius hp₂
   have hd : ‖p₂ -ᵥ s.center‖ ^ 2 =
       ‖p₂ -ᵥ p₁‖ ^ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + ‖p₁ -ᵥ s.center‖ ^ 2 := by
     rw [← vsub_add_vsub_cancel p₂ p₁ s.center, norm_add_sq_real]
@@ -593,6 +606,17 @@ lemma isDiameter_iff_mem_and_mem_and_wbtw :
   rw [mem_sphere.1 h₁, mem_sphere'.1 h₂, ← two_mul, eq_comm] at hd
   exact isDiameter_iff_mem_and_mem_and_dist.2 ⟨h₁, h₂, hd⟩
 
+/-- The center lies on the line through two distinct points of a sphere if and only if those
+points are the endpoints of a diameter. -/
+theorem center_mem_affineSpan_pair_iff_isDiameter
+    (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₁p₂ : p₁ ≠ p₂) :
+    s.center ∈ line[ℝ, p₁, p₂] ↔ s.IsDiameter p₁ p₂ := by
+  rw [isDiameter_iff_mem_and_mem_and_wbtw]
+  refine ⟨fun h => ⟨hp₁, hp₂, ?_⟩, fun h => h.2.2.mem_affineSpan⟩
+  refine wbtw_of_collinear_of_dist_center_le_radius ?_ hp₁ ?_ hp₂ hp₁p₂
+  · rw [Set.insert_comm]; exact collinear_insert_of_mem_affineSpan_pair h
+  · simpa using radius_nonneg_of_mem hp₁
+
 end Sphere
 
 end EuclideanSpace

From e50a6ccb22b3757cd80518d1d8d9208f60744f51 Mon Sep 17 00:00:00 2001
From: Jireh Loreaux <loreaujy@gmail.com>
Date: Tue, 30 Jun 2026 21:51:21 -0500
Subject: [PATCH 2/2] Apply suggestion from @j-loreaux

---
 Mathlib/Geometry/Euclidean/Sphere/Basic.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Geometry/Euclidean/Sphere/Basic.lean b/Mathlib/Geometry/Euclidean/Sphere/Basic.lean
index ce5bf9b85d6f92..89c2f614e760ed 100644
--- a/Mathlib/Geometry/Euclidean/Sphere/Basic.lean
+++ b/Mathlib/Geometry/Euclidean/Sphere/Basic.lean
@@ -141,9 +141,7 @@ lemma Sphere.radius_nonneg_of_mem {s : Sphere P} {p : P} (h : p ∈ s) : 0 ≤ s
 /-- A point of a sphere that differs from another point of the sphere is not its center. -/
 lemma Sphere.ne_center_of_mem_of_mem_of_ne {s : Sphere P} {p q : P}
     (hp : p ∈ s) (hq : q ∈ s) (hpq : p ≠ q) : p ≠ s.center := by
-  rintro rfl
-  rw [Sphere.center_mem_iff] at hp
-  exact hpq (dist_eq_zero.mp (by rw [mem_sphere.mp hq, hp])).symm
+  grind [dist_eq_zero, mem_sphere']
 
 /-- A set of points is cospherical if they are equidistant from some
 point. In two dimensions, this is the same thing as being