chore(Topology/MetricSpace/Ultra): deprecate mem_ball_iff and mem_closedBall_iff (duplicates) (#28524)

Author: euprunin

Mathlib/Topology/MetricSpace/Ultra/Basic.lean

@@ -71,13 +71,7 @@ lemma ball_eq_of_mem {x y : X} {r : ℝ} (h : y ∈ ball x r) : ball x r = ball
   constructor <;> intro h' <;>
   exact (dist_triangle_max _ _ _).trans_lt (max_lt h' (dist_comm x _ ▸ h))
 
-lemma mem_ball_iff {x y : X} {r : ℝ} : y ∈ ball x r ↔ x ∈ ball y r := by
-  cases lt_or_ge 0 r with
-  | inl hr =>
-    constructor <;> intro h <;>
-    rw [← ball_eq_of_mem h] <;>
-    simp [hr]
-  | inr hr => simp [ball_eq_empty.mpr hr]
+@[deprecated (since := "2025-08-16")] alias mem_ball_iff := mem_ball_comm
 
 lemma ball_subset_trichotomy :
     ball x r ⊆ ball y s ∨ ball y s ⊆ ball x r ∨ Disjoint (ball x r) (ball y s) := by
@@ -103,14 +97,7 @@ lemma closedBall_eq_of_mem {x y : X} {r : ℝ} (h : y ∈ closedBall x r) :
   constructor <;> intro h' <;>
   exact (dist_triangle_max _ _ _).trans (max_le h' (dist_comm x _ ▸ h))
 
-lemma mem_closedBall_iff {x y : X} {r : ℝ} :
-    y ∈ closedBall x r ↔ x ∈ closedBall y r := by
-  cases le_or_gt 0 r with
-  | inl hr =>
-    constructor <;> intro h <;>
-    rw [← closedBall_eq_of_mem h] <;>
-    simp [hr]
-  | inr hr => simp [closedBall_eq_empty.mpr hr]
+@[deprecated (since := "2025-08-16")] alias mem_closedBall_iff := mem_closedBall_comm
 
 lemma closedBall_subset_trichotomy :
     closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨