chore: golf NormedSpace.sphere_nonempty (#27910)

This result has nothing to do with pointwise operators on sets, and in finding the right file I also found a lemma which golfs it.

The motivation here was wanting this lemma in the file about operator norms.

Author: eric-wieser

Mathlib/Analysis/NormedSpace/Pointwise.lean

@@ -379,18 +379,6 @@ theorem smul_unitClosedBall_of_nonneg {r : ℝ} (hr : 0 ≤ r) :
 @[deprecated (since := "2024-12-01")]
 alias smul_closedUnitBall_of_nonneg := smul_unitClosedBall_of_nonneg
 
-/-- In a nontrivial real normed space, a sphere is nonempty if and only if its radius is
-nonnegative. -/
-@[simp]
-theorem NormedSpace.sphere_nonempty [Nontrivial E] {x : E} {r : ℝ} :
-    (sphere x r).Nonempty ↔ 0 ≤ r := by
-  obtain ⟨y, hy⟩ := exists_ne x
-  refine ⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr =>
-    ⟨r • ‖y - x‖⁻¹ • (y - x) + x, ?_⟩⟩
-  have : ‖y - x‖ ≠ 0 := by simpa [sub_eq_zero]
-  simp only [mem_sphere_iff_norm, add_sub_cancel_right, norm_smul, Real.norm_eq_abs, norm_inv]
-  simp only [abs_norm]
-  rw [inv_mul_cancel₀ this, mul_one, abs_eq_self.mpr hr]
 
 theorem smul_sphere [Nontrivial E] (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) :
     c • sphere x r = sphere (c • x) (‖c‖ * r) := by

Mathlib/Analysis/NormedSpace/RCLike.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kalle Kytölä
 -/
 import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Analysis.NormedSpace.Real
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
-import Mathlib.Analysis.NormedSpace.Pointwise
 
 /-!
 # Normed spaces over R or C

Mathlib/Analysis/NormedSpace/Real.lean

@@ -130,6 +130,15 @@ theorem nnnorm_surjective : Surjective (nnnorm : E → ℝ≥0) := fun c =>
 theorem range_nnnorm : range (nnnorm : E → ℝ≥0) = univ :=
   (nnnorm_surjective E).range_eq
 
+variable {E} in
+/-- In a nontrivial real normed space, a sphere is nonempty if and only if its radius is
+nonnegative. -/
+@[simp]
+theorem NormedSpace.sphere_nonempty {x : E} {r : ℝ} : (sphere x r).Nonempty ↔ 0 ≤ r := by
+  refine ⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr => ?_⟩
+  obtain ⟨y, hy⟩ := exists_norm_eq E hr
+  exact ⟨x + y, by simpa using hy⟩
+
 end Surj
 
 theorem interior_closedBall' (x : E) (r : ℝ) : interior (closedBall x r) = ball x r := by