chore: Remove ball and bex from lemma names (#10816)

`ball` for "bounded forall" and `bex` for "bounded exists" are from experience very confusing abbreviations. This PR renames them to `forall_mem` and `exists_mem` in the few `Set` lemma names that mention them.

Also deprecate `ball_image_of_ball`, `mem_image_elim`, `mem_image_elim_on` since those lemmas are duplicates of the renamed lemmas (apart from argument order and implicitness, which I am also fixing by making the binder in the RHS of `forall_mem_image` semi-implicit), have obscure names and are completely unused.

Archive/Imo/Imo1972Q5.lean

@@ -33,7 +33,7 @@ theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y
   let k : ℝ := sSup S
   -- Show that `‖f x‖ ≤ k`.
   have hk₁ : ∀ x, ‖f x‖ ≤ k := by
-    have h : BddAbove S := ⟨1, Set.forall_range_iff.mpr hf2⟩
+    have h : BddAbove S := ⟨1, Set.forall_mem_range.mpr hf2⟩
     intro x
     exact le_csSup h (Set.mem_range_self x)
   -- Show that `2 * (‖f x‖ * ‖g y‖) ≤ 2 * k`.

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -315,7 +315,7 @@ theorem ballot_pos (p q : ℕ) :
   have : (1 :: ·) '' countedSequence p (q + 1) ∩ staysPositive =
       (1 :: ·) '' (countedSequence p (q + 1) ∩ staysPositive) := by
     simp only [image_inter List.cons_injective, Set.ext_iff, mem_inter_iff, and_congr_right_iff,
-      ball_image_iff, List.cons_injective.mem_set_image, staysPositive_cons_pos _ one_pos]
+      forall_mem_image, List.cons_injective.mem_set_image, staysPositive_cons_pos _ one_pos]
     exact fun _ _ ↦ trivial
   rw [this, count_injective_image]
   exact List.cons_injective
@@ -344,7 +344,7 @@ theorem ballot_neg (p q : ℕ) (qp : q < p) :
   have : List.cons (-1) '' countedSequence (p + 1) q ∩ staysPositive =
       List.cons (-1) '' (countedSequence (p + 1) q ∩ staysPositive) := by
     simp only [image_inter List.cons_injective, Set.ext_iff, mem_inter_iff, and_congr_right_iff,
-      ball_image_iff, List.cons_injective.mem_set_image, staysPositive_cons, and_iff_left_iff_imp]
+      forall_mem_image, List.cons_injective.mem_set_image, staysPositive_cons, and_iff_left_iff_imp]
     intro l hl _
     simp [sum_of_mem_countedSequence hl, lt_sub_iff_add_lt', qp]
   rw [this, count_injective_image]

Counterexamples/SorgenfreyLine.lean

@@ -84,7 +84,7 @@ theorem nhds_basis_Ico (a : ℝₗ) : (𝓝 a).HasBasis (a < ·) (Ico a ·) := b
   haveI : Nonempty { x // x ≤ a } := Set.nonempty_Iic_subtype
   have : (⨅ x : { i // i ≤ a }, 𝓟 (Ici ↑x)) = 𝓟 (Ici a) := by
     refine' (IsLeast.isGLB _).iInf_eq
-    exact ⟨⟨⟨a, le_rfl⟩, rfl⟩, forall_range_iff.2 fun b => principal_mono.2 <| Ici_subset_Ici.2 b.2⟩
+    exact ⟨⟨⟨a, le_rfl⟩, rfl⟩, forall_mem_range.2 fun b => principal_mono.2 <| Ici_subset_Ici.2 b.2⟩
   simp only [mem_setOf_eq, iInf_and, iInf_exists, @iInf_comm _ (_ ∈ _), @iInf_comm _ (Set ℝₗ),
     iInf_iInf_eq_right, mem_Ico]
   simp_rw [@iInf_comm _ ℝₗ (_ ≤ _), iInf_subtype', ← Ici_inter_Iio, ← inf_principal,

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -715,7 +715,7 @@ theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalSubalgebra R A} :
     (↑(⨅ i, S i) : Set A) = ⋂ i, S i := by simp [iInf]
 
 theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalSubalgebra R A} {x : A} :
-    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by simp only [iInf, mem_sInf, Set.forall_range_iff]
+    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by simp only [iInf, mem_sInf, Set.forall_mem_range]
 
 @[simp]
 theorem iInf_toSubmodule {ι : Sort*} (S : ι → NonUnitalSubalgebra R A) :

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -856,7 +856,7 @@ theorem coe_iInf {ι : Sort*} {S : ι → Subalgebra R A} : (↑(⨅ i, S i) : S
 #align algebra.coe_infi Algebra.coe_iInf
 
 theorem mem_iInf {ι : Sort*} {S : ι → Subalgebra R A} {x : A} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
-  simp only [iInf, mem_sInf, Set.forall_range_iff]
+  simp only [iInf, mem_sInf, Set.forall_mem_range]
 #align algebra.mem_infi Algebra.mem_iInf
 
 open Subalgebra in

Mathlib/Algebra/Module/LocalizedModule.lean

@@ -607,7 +607,7 @@ theorem isLocalizedModule_iff_isLocalization {A Aₛ} [CommSemiring A] [Algebra
   refine and_congr ?_ (and_congr (forall_congr' fun _ ↦ ?_) (forall₂_congr fun _ _ ↦ ?_))
   · simp_rw [← (Algebra.lmul R Aₛ).commutes, Algebra.lmul_isUnit_iff, Subtype.forall,
       Algebra.algebraMapSubmonoid, ← SetLike.mem_coe, Submonoid.coe_map,
-      Set.ball_image_iff, ← IsScalarTower.algebraMap_apply]
+      Set.forall_mem_image, ← IsScalarTower.algebraMap_apply]
   · simp_rw [Prod.exists, Subtype.exists, Algebra.algebraMapSubmonoid]
     simp [← IsScalarTower.algebraMap_apply, Submonoid.mk_smul, Algebra.smul_def, mul_comm]
   · congr!; simp_rw [Subtype.exists, Algebra.algebraMapSubmonoid]; simp [Algebra.smul_def]

Mathlib/Algebra/Order/CompleteField.lean

@@ -69,8 +69,8 @@ instance (priority := 100) ConditionallyCompleteLinearOrderedField.to_archimedea
       by_contra! h
       obtain ⟨x, h⟩ := h
       have := csSup_le _ _ (range_nonempty Nat.cast)
-        (forall_range_iff.2 fun m =>
-          le_sub_iff_add_le.2 <| le_csSup _ _ ⟨x, forall_range_iff.2 h⟩ ⟨m+1, Nat.cast_succ m⟩)
+        (forall_mem_range.2 fun m =>
+          le_sub_iff_add_le.2 <| le_csSup _ _ ⟨x, forall_mem_range.2 h⟩ ⟨m+1, Nat.cast_succ m⟩)
       linarith)
 #align conditionally_complete_linear_ordered_field.to_archimedean ConditionallyCompleteLinearOrderedField.to_archimedean
 
@@ -143,7 +143,7 @@ theorem cutMap_nonempty (a : α) : (cutMap β a).Nonempty :=
 
 theorem cutMap_bddAbove (a : α) : BddAbove (cutMap β a) := by
   obtain ⟨q, hq⟩ := exists_rat_gt a
-  exact ⟨q, ball_image_iff.2 fun r hr => mod_cast (hq.trans' hr).le⟩
+  exact ⟨q, forall_mem_image.2 fun r hr => mod_cast (hq.trans' hr).le⟩
 #align linear_ordered_field.cut_map_bdd_above LinearOrderedField.cutMap_bddAbove
 
 theorem cutMap_add (a b : α) : cutMap β (a + b) = cutMap β a + cutMap β b := by

Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

@@ -740,7 +740,7 @@ theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalStarSubalgebra R A} :
     (↑(⨅ i, S i) : Set A) = ⋂ i, S i := by simp [iInf]
 
 theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalStarSubalgebra R A} {x : A} :
-    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by simp only [iInf, mem_sInf, Set.forall_range_iff]
+    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by simp only [iInf, mem_sInf, Set.forall_mem_range]
 
 @[simp]
 theorem iInf_toNonUnitalSubalgebra {ι : Sort*} (S : ι → NonUnitalStarSubalgebra R A) :

Mathlib/Algebra/Star/Subalgebra.lean

@@ -696,7 +696,7 @@ theorem coe_iInf {ι : Sort*} {S : ι → StarSubalgebra R A} : (↑(⨅ i, S i)
 #align star_subalgebra.coe_infi StarSubalgebra.coe_iInf
 
 theorem mem_iInf {ι : Sort*} {S : ι → StarSubalgebra R A} {x : A} :
-    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by simp only [iInf, mem_sInf, Set.forall_range_iff]
+    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by simp only [iInf, mem_sInf, Set.forall_mem_range]
 #align star_subalgebra.mem_infi StarSubalgebra.mem_iInf
 
 @[simp]

Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

@@ -522,7 +522,7 @@ theorem HasFDerivWithinAt.uniqueDiffWithinAt {x : E} (h : HasFDerivWithinAt f f'
 theorem UniqueDiffOn.image {f' : E → E →L[𝕜] F} (hs : UniqueDiffOn 𝕜 s)
     (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hd : ∀ x ∈ s, DenseRange (f' x)) :
     UniqueDiffOn 𝕜 (f '' s) :=
-  ball_image_iff.2 fun x hx => (hf' x hx).uniqueDiffWithinAt (hs x hx) (hd x hx)
+  forall_mem_image.2 fun x hx => (hf' x hx).uniqueDiffWithinAt (hs x hx) (hd x hx)
 #align unique_diff_on.image UniqueDiffOn.image
 
 theorem HasFDerivWithinAt.uniqueDiffWithinAt_of_continuousLinearEquiv {x : E} (e' : E ≃L[𝕜] F)

Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

@@ -286,7 +286,7 @@ theorem open_image (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRi
     (hs : IsOpen s) (hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹) : IsOpen (f '' s) := by
   cases' hc with hE hc
   · exact isOpen_discrete _
-  simp only [isOpen_iff_mem_nhds, nhds_basis_closedBall.mem_iff, ball_image_iff] at hs ⊢
+  simp only [isOpen_iff_mem_nhds, nhds_basis_closedBall.mem_iff, forall_mem_image] at hs ⊢
   intro x hx
   rcases hs x hx with ⟨ε, ε0, hε⟩
   refine' ⟨(f'symm.nnnorm⁻¹ - c) * ε, mul_pos (sub_pos.2 hc) ε0, _⟩

Mathlib/Analysis/Calculus/MeanValue.lean

@@ -1414,7 +1414,7 @@ theorem domain_mvt {f : E → ℝ} {s : Set E} {x y : E} {f' : E → E →L[ℝ]
     · exact fun t Ht => (hfg t <| hsub Ht).hasDerivAt (Icc_mem_nhds Ht.1 Ht.2)
   -- reinterpret on domain
   rcases hMVT with ⟨t, Ht, hMVT'⟩
-  rw [segment_eq_image_lineMap, bex_image_iff]
+  rw [segment_eq_image_lineMap, exists_mem_image]
   refine ⟨t, hsub Ht, ?_⟩
   simpa [g] using hMVT'.symm
 #align domain_mvt domain_mvt

Mathlib/Analysis/Convex/Basic.lean

@@ -101,7 +101,7 @@ theorem convex_sInter {S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s) : Conve
 
 theorem convex_iInter {ι : Sort*} {s : ι → Set E} (h : ∀ i, Convex 𝕜 (s i)) :
     Convex 𝕜 (⋂ i, s i) :=
-  sInter_range s ▸ convex_sInter <| forall_range_iff.2 h
+  sInter_range s ▸ convex_sInter <| forall_mem_range.2 h
 #align convex_Inter convex_iInter
 
 theorem convex_iInter₂ {ι : Sort*} {κ : ι → Sort*} {s : ∀ i, κ i → Set E}

Mathlib/Analysis/Convex/Cone/Extension.lean

@@ -71,7 +71,7 @@ theorem step (nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x)
     set Sp := f '' { x : f.domain | (x : E) + y ∈ s }
     set Sn := f '' { x : f.domain | -(x : E) - y ∈ s }
     suffices (upperBounds Sn ∩ lowerBounds Sp).Nonempty by
-      simpa only [Set.Nonempty, upperBounds, lowerBounds, ball_image_iff] using this
+      simpa only [Set.Nonempty, upperBounds, lowerBounds, forall_mem_image] using this
     refine' exists_between_of_forall_le (Nonempty.image f _) (Nonempty.image f (dense y)) _
     · rcases dense (-y) with ⟨x, hx⟩
       rw [← neg_neg x, NegMemClass.coe_neg, ← sub_eq_add_neg] at hx

Mathlib/Analysis/Convex/Integral.lean

@@ -75,7 +75,7 @@ theorem Convex.integral_mem [IsProbabilityMeasure μ] (hs : Convex ℝ s) (hsc :
   · rw [← ENNReal.toReal_sum, (G n).sum_range_measure_preimage_singleton, measure_univ,
       ENNReal.one_toReal]
     exact fun _ _ => measure_ne_top _ _
-  · simp only [SimpleFunc.mem_range, forall_range_iff]
+  · simp only [SimpleFunc.mem_range, forall_mem_range]
     intro x
     apply inter_subset_right (range g)
     exact SimpleFunc.approxOn_mem hgm.measurable h₀ _ _

Mathlib/Analysis/Convex/Star.lean

@@ -115,7 +115,7 @@ theorem starConvex_sInter {S : Set (Set E)} (h : ∀ s ∈ S, StarConvex 𝕜 x
 
 theorem starConvex_iInter {ι : Sort*} {s : ι → Set E} (h : ∀ i, StarConvex 𝕜 x (s i)) :
     StarConvex 𝕜 x (⋂ i, s i) :=
-  sInter_range s ▸ starConvex_sInter <| forall_range_iff.2 h
+  sInter_range s ▸ starConvex_sInter <| forall_mem_range.2 h
 #align star_convex_Inter starConvex_iInter
 
 theorem StarConvex.union (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 x t) :

Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

@@ -59,11 +59,11 @@ theorem LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure [NormedSpace 
   so it suffices to prove the theorem for `y = f x - x`. -/
   have : IsClosed {x | Tendsto (birkhoffAverage 𝕜 f _root_.id · x) atTop (𝓝 0)} :=
     isClosed_setOf_tendsto_birkhoffAverage 𝕜 hf uniformContinuous_id continuous_const
-  refine closure_minimal (Set.forall_range_iff.2 fun x ↦ ?_) this (hg_ker hy)
+  refine closure_minimal (Set.forall_mem_range.2 fun x ↦ ?_) this (hg_ker hy)
   /- Finally, for `y = f x - x` the average is equal to the difference between averages
   along the orbits of `f x` and `x`, and most of the terms cancel. -/
   have : IsBounded (Set.range (_root_.id <| f^[·] x)) :=
-    isBounded_iff_forall_norm_le.2 ⟨‖x‖, Set.forall_range_iff.2 fun n ↦ by
+    isBounded_iff_forall_norm_le.2 ⟨‖x‖, Set.forall_mem_range.2 fun n ↦ by
       have H : f^[n] 0 = 0 := (f : E →+ E).iterate_map_zero n
       simpa [H] using (hf.iterate n).dist_le_mul x 0⟩
   have H : ∀ n x y, f^[n] (x - y) = f^[n] x - f^[n] y := (f : E →+ E).iterate_map_sub

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -77,7 +77,7 @@ theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h
   let δ := ⨅ w : K, ‖u - w‖
   letI : Nonempty K := ne.to_subtype
   have zero_le_δ : 0 ≤ δ := le_ciInf fun _ => norm_nonneg _
-  have δ_le : ∀ w : K, δ ≤ ‖u - w‖ := ciInf_le ⟨0, Set.forall_range_iff.2 fun _ => norm_nonneg _⟩
+  have δ_le : ∀ w : K, δ ≤ ‖u - w‖ := ciInf_le ⟨0, Set.forall_mem_range.2 fun _ => norm_nonneg _⟩
   have δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖ := fun w hw => δ_le ⟨w, hw⟩
   -- Step 1: since `δ` is the infimum, can find a sequence `w : ℕ → K` in `K`
   -- such that `‖u - w n‖ < δ + 1 / (n + 1)` (which implies `‖u - w n‖ --> δ`);
@@ -386,7 +386,7 @@ instance HasOrthogonalProjection.map_linearIsometryEquiv [HasOrthogonalProjectio
     HasOrthogonalProjection (K.map (f.toLinearEquiv : E →ₗ[𝕜] E')) where
   exists_orthogonal v := by
     rcases HasOrthogonalProjection.exists_orthogonal (K := K) (f.symm v) with ⟨w, hwK, hw⟩
-    refine ⟨f w, Submodule.mem_map_of_mem hwK, Set.ball_image_iff.2 fun u hu ↦ ?_⟩
+    refine ⟨f w, Submodule.mem_map_of_mem hwK, Set.forall_mem_image.2 fun u hu ↦ ?_⟩
     erw [← f.symm.inner_map_map, f.symm_apply_apply, map_sub, f.symm_apply_apply, hw u hu]
 
 instance HasOrthogonalProjection.map_linearIsometryEquiv' [HasOrthogonalProjection K]
@@ -948,7 +948,7 @@ theorem orthogonalProjection_tendsto_closure_iSup [CompleteSpace E] {ι : Type*}
   rw [norm_sub_rev, orthogonalProjection_minimal]
   refine' lt_of_le_of_lt _ hay
   change _ ≤ ‖y - (⟨a, hU hi hI⟩ : U i)‖
-  exact ciInf_le ⟨0, Set.forall_range_iff.mpr fun _ => norm_nonneg _⟩ _
+  exact ciInf_le ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩ _
 #align orthogonal_projection_tendsto_closure_supr orthogonalProjection_tendsto_closure_iSup
 
 /-- Given a monotone family `U` of complete submodules of `E` with dense span supremum,

Mathlib/Analysis/LocallyConvex/Bounded.lean

@@ -396,7 +396,7 @@ theorem isVonNBounded_iff' (s : Set E) :
 
 theorem image_isVonNBounded_iff (f : E' → E) (s : Set E') :
     Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r : ℝ, ∀ x ∈ s, ‖f x‖ ≤ r := by
-  simp_rw [isVonNBounded_iff', Set.ball_image_iff]
+  simp_rw [isVonNBounded_iff', Set.forall_mem_image]
 #align normed_space.image_is_vonN_bounded_iff NormedSpace.image_isVonNBounded_iff
 
 /-- In a normed space, the von Neumann bornology (`Bornology.vonNBornology`) is equal to the

Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

@@ -539,7 +539,7 @@ theorem WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded (f : G →
     (hp : WithSeminorms p) :
     Bornology.IsVonNBounded 𝕜 (f '' s) ↔
       ∀ I : Finset ι, ∃ r > 0, ∀ x ∈ s, I.sup p (f x) < r := by
-  simp_rw [hp.isVonNBounded_iff_finset_seminorm_bounded, Set.ball_image_iff]
+  simp_rw [hp.isVonNBounded_iff_finset_seminorm_bounded, Set.forall_mem_image]
 
 set_option linter.uppercaseLean3 false in
 #align with_seminorms.image_is_vonN_bounded_iff_finset_seminorm_bounded WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded
@@ -571,7 +571,7 @@ set_option linter.uppercaseLean3 false in
 theorem WithSeminorms.image_isVonNBounded_iff_seminorm_bounded (f : G → E) {s : Set G}
     (hp : WithSeminorms p) :
     Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ i : ι, ∃ r > 0, ∀ x ∈ s, p i (f x) < r := by
-  simp_rw [hp.isVonNBounded_iff_seminorm_bounded, Set.ball_image_iff]
+  simp_rw [hp.isVonNBounded_iff_seminorm_bounded, Set.forall_mem_image]
 
 set_option linter.uppercaseLean3 false in
 #align with_seminorms.image_is_vonN_bounded_iff_seminorm_bounded WithSeminorms.image_isVonNBounded_iff_seminorm_bounded
@@ -694,7 +694,7 @@ protected theorem _root_.WithSeminorms.equicontinuous_TFAE {κ : Type*}
       simpa using (hx k).le
     have bdd : BddAbove (range fun k ↦ (q i).comp (f k)) :=
       Seminorm.bddAbove_of_absorbent (absorbent_nhds_zero this)
-        (fun x hx ↦ ⟨1, forall_range_iff.mpr hx⟩)
+        (fun x hx ↦ ⟨1, forall_mem_range.mpr hx⟩)
     rw [← Seminorm.coe_iSup_eq bdd]
     refine ⟨bdd, Seminorm.continuous' (r := 1) ?_⟩
     filter_upwards [this] with x hx

Mathlib/Analysis/Normed/Group/Pointwise.lean

@@ -44,7 +44,7 @@ theorem Bornology.IsBounded.of_mul (hst : IsBounded (s * t)) : IsBounded s ∨ I
 
 @[to_additive]
 theorem Bornology.IsBounded.inv : IsBounded s → IsBounded s⁻¹ := by
-  simp_rw [isBounded_iff_forall_norm_le', ← image_inv, ball_image_iff, norm_inv']
+  simp_rw [isBounded_iff_forall_norm_le', ← image_inv, forall_mem_image, norm_inv']
   exact id
 #align metric.bounded.inv Bornology.IsBounded.inv
 #align metric.bounded.neg Bornology.IsBounded.neg

Mathlib/Analysis/Normed/Group/Quotient.lean

@@ -130,7 +130,7 @@ theorem image_norm_nonempty {S : AddSubgroup M} (x : M ⧸ S) :
 #align image_norm_nonempty image_norm_nonempty
 
 theorem bddBelow_image_norm (s : Set M) : BddBelow (norm '' s) :=
-  ⟨0, ball_image_iff.2 fun _ _ ↦ norm_nonneg _⟩
+  ⟨0, forall_mem_image.2 fun _ _ ↦ norm_nonneg _⟩
 #align bdd_below_image_norm bddBelow_image_norm
 
 theorem isGLB_quotient_norm {S : AddSubgroup M} (x : M ⧸ S) :
@@ -168,7 +168,7 @@ theorem quotient_norm_mk_eq (S : AddSubgroup M) (m : M) :
 
 /-- The quotient norm is nonnegative. -/
 theorem quotient_norm_nonneg (S : AddSubgroup M) (x : M ⧸ S) : 0 ≤ ‖x‖ :=
-  Real.sInf_nonneg _ <| ball_image_iff.2 fun _ _ ↦ norm_nonneg _
+  Real.sInf_nonneg _ <| forall_mem_image.2 fun _ _ ↦ norm_nonneg _
 #align quotient_norm_nonneg quotient_norm_nonneg
 
 /-- The quotient norm is nonnegative. -/
@@ -186,7 +186,7 @@ theorem quotient_norm_eq_zero_iff (S : AddSubgroup M) (m : M) :
 
 theorem QuotientAddGroup.norm_lt_iff {S : AddSubgroup M} {x : M ⧸ S} {r : ℝ} :
     ‖x‖ < r ↔ ∃ m : M, ↑m = x ∧ ‖m‖ < r := by
-  rw [isGLB_lt_iff (isGLB_quotient_norm _), bex_image_iff]
+  rw [isGLB_lt_iff (isGLB_quotient_norm _), exists_mem_image]
   rfl
 
 /-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x`
@@ -211,7 +211,7 @@ theorem quotient_norm_add_le (S : AddSubgroup M) (x y : M ⧸ S) : ‖x + y‖ 
   rcases And.intro (mk_surjective x) (mk_surjective y) with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
   simp only [← mk'_apply, ← map_add, quotient_norm_mk_eq, sInf_image']
   refine le_ciInf_add_ciInf fun a b ↦ ?_
-  refine ciInf_le_of_le ⟨0, forall_range_iff.2 fun _ ↦ norm_nonneg _⟩ (a + b) ?_
+  refine ciInf_le_of_le ⟨0, forall_mem_range.2 fun _ ↦ norm_nonneg _⟩ (a + b) ?_
   exact (congr_arg norm (add_add_add_comm _ _ _ _)).trans_le (norm_add_le _ _)
 #align quotient_norm_add_le quotient_norm_add_le
 

Mathlib/Analysis/NormedSpace/BanachSteinhaus.lean

@@ -35,7 +35,7 @@ theorem banach_steinhaus {ι : Type*} [CompleteSpace E] {g : ι → E →SL[σ
     (h : ∀ x, ∃ C, ∀ i, ‖g i x‖ ≤ C) : ∃ C', ∀ i, ‖g i‖ ≤ C' := by
   rw [show (∃ C, ∀ i, ‖g i‖ ≤ C) ↔ _ from (NormedSpace.equicontinuous_TFAE g).out 5 2]
   refine (norm_withSeminorms 𝕜₂ F).banach_steinhaus (fun _ x ↦ ?_)
-  simpa [bddAbove_def, forall_range_iff] using h x
+  simpa [bddAbove_def, forall_mem_range] using h x
 #align banach_steinhaus banach_steinhaus
 
 open ENNReal

Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

@@ -563,7 +563,7 @@ spaces is an open subset of the space of linear maps between them.
 -/
 
 protected theorem isOpen [CompleteSpace E] : IsOpen (range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F)) := by
-  rw [isOpen_iff_mem_nhds, forall_range_iff]
+  rw [isOpen_iff_mem_nhds, forall_mem_range]
   refine' fun e => IsOpen.mem_nhds _ (mem_range_self _)
   let O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (e.symm : F →L[𝕜] E).comp f
   have h_O : Continuous O := isBoundedBilinearMap_comp.continuous_right

Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

@@ -106,10 +106,10 @@ theorem geometric_hahn_banach_open (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (ht
   refine' ⟨f, sInf (f '' t), image_subset_iff.1 (_ : f '' s ⊆ Iio (sInf (f '' t))), fun b hb => _⟩
   · rw [← interior_Iic]
     refine' interior_maximal (image_subset_iff.2 fun a ha => _) (f.isOpenMap_of_ne_zero _ _ hs₂)
-    · exact le_csInf (Nonempty.image _ ⟨_, hb₀⟩) (ball_image_of_ball <| forall_le _ ha)
+    · exact le_csInf (Nonempty.image _ ⟨_, hb₀⟩) (forall_mem_image.2 <| forall_le _ ha)
     · rintro rfl
       simp at hf₁
-  · exact csInf_le ⟨f a₀, ball_image_of_ball <| forall_le _ ha₀⟩ (mem_image_of_mem _ hb)
+  · exact csInf_le ⟨f a₀, forall_mem_image.2 <| forall_le _ ha₀⟩ (mem_image_of_mem _ hb)
 #align geometric_hahn_banach_open geometric_hahn_banach_open
 
 theorem geometric_hahn_banach_open_point (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (disj : x ∉ s) :

Mathlib/Analysis/NormedSpace/MazurUlam.lean

@@ -50,7 +50,7 @@ theorem midpoint_fixed {x y : PE} :
   haveI : Nonempty s := ⟨⟨IsometryEquiv.refl PE, rfl, rfl⟩⟩
   -- On the one hand, `e` cannot send the midpoint `z` of `[x, y]` too far
   have h_bdd : BddAbove (range fun e : s => dist ((e : PE ≃ᵢ PE) z) z) := by
-    refine' ⟨dist x z + dist x z, forall_range_iff.2 <| Subtype.forall.2 _⟩
+    refine' ⟨dist x z + dist x z, forall_mem_range.2 <| Subtype.forall.2 _⟩
     rintro e ⟨hx, _⟩
     calc
       dist (e z) z ≤ dist (e z) x + dist x z := dist_triangle (e z) x z