chore: remove more bex and ball from lemma names (#11615)

Follow-up to #10816.

Remaining places containing such lemmas are
- `Option.bex_ne_none` and `Option.ball_ne_none`: defined in Lean core
- `Nat.decidableBallLT` and `Nat.decidableBallLE`: defined in Lean core
- `bef_def` is still used in a number of places and could be renamed
- `BAll.imp_{left,right}`, `BEx.imp_{left,right}`, `BEx.intro` and `BEx.elim`

I only audited the first ~150 lemmas mentioning "ball"; too many lemmas named after Metric.ball/openBall/closedBall.



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Archive/Wiedijk100Theorems/Partition.lean

@@ -306,7 +306,7 @@ theorem oddGF_prop [Field α] (n m : ℕ) (h : n < m * 2) :
     (Finset.card (Nat.Partition.odds n) : α) = coeff α n (partialOddGF m) := by
   rw [← partialOddGF_prop, Nat.Partition.odds]
   congr with p
-  apply ball_congr
+  apply forall₂_congr
   intro i hi
   have hin : i ≤ n := by
     simpa [p.parts_sum] using Multiset.single_le_sum (fun _ _ => Nat.zero_le _) _ hi

Mathlib/Analysis/Convex/Basic.lean

@@ -187,10 +187,8 @@ theorem convex_segment (x y : E) : Convex 𝕜 [x -[𝕜] y] := by
 #align convex_segment convex_segment
 
 theorem Convex.linear_image (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (f '' s) := by
-  intro x hx y hy a b ha hb hab
-  obtain ⟨x', hx', rfl⟩ := mem_image_iff_bex.1 hx
-  obtain ⟨y', hy', rfl⟩ := mem_image_iff_bex.1 hy
-  exact ⟨a • x' + b • y', hs hx' hy' ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩
+  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ a b ha hb hab
+  exact ⟨a • x + b • y, hs hx hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩
 #align convex.linear_image Convex.linear_image
 
 theorem Convex.is_linear_image (hs : Convex 𝕜 s) {f : E → F} (hf : IsLinearMap 𝕜 f) :

Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

@@ -547,7 +547,7 @@ theorem WithSeminorms.isVonNBounded_iff_seminorm_bounded {s : Set E} (hp : WithS
   by_cases hI : I.Nonempty
   · choose r hr h using hi
     have h' : 0 < I.sup' hI r := by
-      rcases hI.bex with ⟨i, hi⟩
+      rcases hI with ⟨i, hi⟩
       exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)
     refine' ⟨I.sup' hI r, h', fun x hx => finset_sup_apply_lt h' fun i hi => _⟩
     refine' lt_of_lt_of_le (h i x hx) _

Mathlib/Analysis/NormedSpace/Banach.lean

@@ -232,7 +232,7 @@ protected theorem isOpenMap (surj : Surjective f) : IsOpenMap f := by
   intro s hs
   rcases exists_preimage_norm_le f surj with ⟨C, Cpos, hC⟩
   refine' isOpen_iff.2 fun y yfs => _
-  rcases mem_image_iff_bex.1 yfs with ⟨x, xs, fxy⟩
+  rcases yfs with ⟨x, xs, fxy⟩
   rcases isOpen_iff.1 hs x xs with ⟨ε, εpos, hε⟩
   refine' ⟨ε / C, div_pos εpos Cpos, fun z hz => _⟩
   rcases hC (z - y) with ⟨w, wim, wnorm⟩

Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

@@ -159,7 +159,7 @@ theorem equalizer_sheaf_condition :
     ← Equiv.forall_congr_left (firstObjEqFamily P (S : Presieve X)).toEquiv.symm]
   simp_rw [← compatible_iff]
   simp only [inv_hom_id_apply, Iso.toEquiv_symm_fun]
-  apply ball_congr
+  apply forall₂_congr
   intro x _
   apply exists_unique_congr
   intro t
@@ -247,7 +247,7 @@ theorem sheaf_condition : R.IsSheafFor P ↔ Nonempty (IsLimit (Fork.ofι _ (w P
   rw [Types.type_equalizer_iff_unique]
   erw [← Equiv.forall_congr_left (firstObjEqFamily P R).toEquiv.symm]
   simp_rw [← compatible_iff, ← Iso.toEquiv_fun, Equiv.apply_symm_apply]
-  apply ball_congr
+  apply forall₂_congr
   intro x _
   apply exists_unique_congr
   intro t
@@ -344,7 +344,7 @@ theorem sheaf_condition : (Presieve.ofArrows X π).IsSheafFor P ↔
   rw [Types.type_equalizer_iff_unique, isSheafFor_arrows_iff]
   erw [← Equiv.forall_congr_left (Types.productIso _).toEquiv.symm]
   simp_rw [← compatible_iff, ← Iso.toEquiv_fun, Equiv.apply_symm_apply]
-  apply ball_congr
+  apply forall₂_congr
   intro x _
   apply exists_unique_congr
   intro t

Mathlib/CategoryTheory/Sites/IsSheafFor.lean

@@ -504,7 +504,7 @@ theorem isSheafFor_iff_yonedaSheafCondition {P : Cᵒᵖ ⥤ Type v₁} :
   simp_rw [extension_iff_amalgamation]
   rw [Equiv.forall_congr_left' natTransEquivCompatibleFamily]
   rw [Subtype.forall]
-  apply ball_congr
+  apply forall₂_congr
   intro x hx
   rw [Equiv.exists_unique_congr_left _]
   simp

Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean

@@ -96,7 +96,7 @@ private theorem distinctPairs_increment :
   rintro ⟨Ui, Vj⟩
   simp only [distinctPairs, increment, mem_offDiag, bind_parts, mem_biUnion, Prod.exists,
     exists_and_left, exists_prop, mem_product, mem_attach, true_and_iff, Subtype.exists, and_imp,
-    mem_offDiag, forall_exists_index, bex_imp, Ne]
+    mem_offDiag, forall_exists_index, exists₂_imp, Ne]
   refine' fun U V hUV hUi hVj => ⟨⟨_, hUV.1, hUi⟩, ⟨_, hUV.2.1, hVj⟩, _⟩
   rintro rfl
   obtain ⟨i, hi⟩ := nonempty_of_mem_parts _ hUi

Mathlib/Data/Analysis/Topology.lean

@@ -136,7 +136,7 @@ protected theorem mem_nhds [T : TopologicalSpace α] (F : Realizer α) {s : Set
 
 theorem isOpen_iff [TopologicalSpace α] (F : Realizer α) {s : Set α} :
     IsOpen s ↔ ∀ a ∈ s, ∃ b, a ∈ F.F b ∧ F.F b ⊆ s :=
-  isOpen_iff_mem_nhds.trans <| ball_congr fun _a _h ↦ F.mem_nhds
+  isOpen_iff_mem_nhds.trans <| forall₂_congr fun _a _h ↦ F.mem_nhds
 #align ctop.realizer.is_open_iff Ctop.Realizer.isOpen_iff
 
 theorem isClosed_iff [TopologicalSpace α] (F : Realizer α) {s : Set α} :

Mathlib/Data/Finset/Basic.lean

@@ -501,9 +501,10 @@ alias ⟨_, Nonempty.to_set⟩ := coe_nonempty
 alias ⟨_, Nonempty.coe_sort⟩ := nonempty_coe_sort
 #align finset.nonempty.coe_sort Finset.Nonempty.coe_sort
 
-theorem Nonempty.bex {s : Finset α} (h : s.Nonempty) : ∃ x : α, x ∈ s :=
+theorem Nonempty.exists_mem {s : Finset α} (h : s.Nonempty) : ∃ x : α, x ∈ s :=
   h
-#align finset.nonempty.bex Finset.Nonempty.bex
+#align finset.nonempty.bex Finset.Nonempty.exists_mem
+@[deprecated] alias Nonempty.bex := Nonempty.exists_mem -- 2024-03-23
 
 theorem Nonempty.mono {s t : Finset α} (hst : s ⊆ t) (hs : s.Nonempty) : t.Nonempty :=
   Set.Nonempty.mono hst hs

Mathlib/Data/Finset/Image.lean

@@ -396,7 +396,7 @@ instance canLift (c) (p) [CanLift β α c p] :
 theorem image_congr (h : (s : Set α).EqOn f g) : Finset.image f s = Finset.image g s := by
   ext
   simp_rw [mem_image, ← bex_def]
-  exact bex_congr fun x hx => by rw [h hx]
+  exact exists₂_congr fun x hx => by rw [h hx]
 #align finset.image_congr Finset.image_congr
 
 theorem _root_.Function.Injective.mem_finset_image (hf : Injective f) :
@@ -659,7 +659,7 @@ theorem disjoint_image {s t : Finset α} {f : α → β} (hf : Injective f) :
 
 theorem image_const {s : Finset α} (h : s.Nonempty) (b : β) : (s.image fun _ => b) = singleton b :=
   ext fun b' => by
-    simp only [mem_image, exists_prop, exists_and_right, h.bex, true_and_iff, mem_singleton,
+    simp only [mem_image, exists_prop, exists_and_right, h.exists_mem, true_and_iff, mem_singleton,
       eq_comm]
 #align finset.image_const Finset.image_const
 

Mathlib/Data/Finset/Lattice.lean

@@ -1290,7 +1290,7 @@ theorem lt_sup'_iff : a < s.sup' H f ↔ ∃ b ∈ s, a < f b := by
 @[simp]
 theorem sup'_lt_iff : s.sup' H f < a ↔ ∀ i ∈ s, f i < a := by
   rw [← WithBot.coe_lt_coe, coe_sup', Finset.sup_lt_iff (WithBot.bot_lt_coe a)]
-  exact ball_congr (fun _ _ => WithBot.coe_lt_coe)
+  exact forall₂_congr (fun _ _ => WithBot.coe_lt_coe)
 #align finset.sup'_lt_iff Finset.sup'_lt_iff
 
 @[simp]

Mathlib/Data/Finset/Prod.lean

@@ -74,12 +74,12 @@ theorem subset_product_image_snd [DecidableEq β] : (s ×ˢ t).image Prod.snd 
 
 theorem product_image_fst [DecidableEq α] (ht : t.Nonempty) : (s ×ˢ t).image Prod.fst = s := by
   ext i
-  simp [mem_image, ht.bex]
+  simp [mem_image, ht.exists_mem]
 #align finset.product_image_fst Finset.product_image_fst
 
 theorem product_image_snd [DecidableEq β] (ht : s.Nonempty) : (s ×ˢ t).image Prod.snd = t := by
   ext i
-  simp [mem_image, ht.bex]
+  simp [mem_image, ht.exists_mem]
 #align finset.product_image_snd Finset.product_image_snd
 
 theorem subset_product [DecidableEq α] [DecidableEq β] {s : Finset (α × β)} :

Mathlib/Data/List/Basic.lean

@@ -274,8 +274,6 @@ theorem forall_mem_of_forall_mem_cons {p : α → Prop} {a : α} {l : List α} (
 
 #align list.forall_mem_append List.forall_mem_append
 
-theorem not_exists_mem_nil (p : α → Prop) : ¬∃ x ∈ @nil α, p x :=
-  nofun
 #align list.not_exists_mem_nil List.not_exists_mem_nilₓ -- bExists change
 
 -- Porting note: bExists in Lean3 and And in Lean4

Mathlib/Data/List/Pairwise.lean

@@ -127,7 +127,7 @@ theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h
   induction' l with a l ihl
   · simp
   obtain ⟨_, hl⟩ : p a ∧ ∀ b, b ∈ l → p b := by simpa using h
-  simp only [ihl hl, pairwise_cons, bex_imp, pmap, and_congr_left_iff, mem_pmap]
+  simp only [ihl hl, pairwise_cons, exists₂_imp, pmap, and_congr_left_iff, mem_pmap]
   refine' fun _ => ⟨fun H b hb _ hpb => H _ _ hb rfl, _⟩
   rintro H _ b hb rfl
   exact H b hb _ _

Mathlib/Data/List/Sigma.lean

@@ -144,7 +144,7 @@ theorem perm_nodupKeys {l₁ l₂ : List (Sigma β)} (h : l₁ ~ l₂) : NodupKe
 theorem nodupKeys_join {L : List (List (Sigma β))} :
     NodupKeys (join L) ↔ (∀ l ∈ L, NodupKeys l) ∧ Pairwise Disjoint (L.map keys) := by
   rw [nodupKeys_iff_pairwise, pairwise_join, pairwise_map]
-  refine' and_congr (ball_congr fun l _ => by simp [nodupKeys_iff_pairwise]) _
+  refine' and_congr (forall₂_congr fun l _ => by simp [nodupKeys_iff_pairwise]) _
   apply iff_of_eq; congr with (l₁ l₂)
   simp [keys, disjoint_iff_ne]
 #align list.nodupkeys_join List.nodupKeys_join

Mathlib/Data/Nat/Squarefree.lean

@@ -376,7 +376,7 @@ and generalizes to arbitrary commutative monoids. See `Squarefree.of_mul_left` a
 theorem squarefree_mul {m n : ℕ} (hmn : m.Coprime n) :
     Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n := by
   simp only [squarefree_iff_prime_squarefree, ← sq, ← forall_and]
-  refine' ball_congr fun p hp => _
+  refine' forall₂_congr fun p hp => _
   simp only [hmn.isPrimePow_dvd_mul (hp.isPrimePow.pow two_ne_zero), not_or]
 #align nat.squarefree_mul Nat.squarefree_mul
 

Mathlib/Data/Set/Basic.lean

@@ -614,9 +614,10 @@ theorem subset_eq_empty {s t : Set α} (h : t ⊆ s) (e : s = ∅) : t = ∅ :=
   subset_empty_iff.1 <| e ▸ h
 #align set.subset_eq_empty Set.subset_eq_empty
 
-theorem ball_empty_iff {p : α → Prop} : (∀ x ∈ (∅ : Set α), p x) ↔ True :=
+theorem forall_mem_empty {p : α → Prop} : (∀ x ∈ (∅ : Set α), p x) ↔ True :=
   iff_true_intro fun _ => False.elim
-#align set.ball_empty_iff Set.ball_empty_iff
+#align set.ball_empty_iff Set.forall_mem_empty
+@[deprecated] alias ball_empty_iff := forall_mem_empty -- 2024-03-23
 
 instance (α : Type u) : IsEmpty.{u + 1} (↥(∅ : Set α)) :=
   ⟨fun x => x.2⟩
@@ -1206,15 +1207,17 @@ theorem forall_insert_of_forall {P : α → Prop} {a : α} {s : Set α} (H : ∀
 
 /- Porting note: ∃ x ∈ insert a s, P x is parsed as ∃ x, x ∈ insert a s ∧ P x,
  where in Lean3 it was parsed as `∃ x, ∃ (h : x ∈ insert a s), P x` -/
-theorem bex_insert_iff {P : α → Prop} {a : α} {s : Set α} :
+theorem exists_mem_insert {P : α → Prop} {a : α} {s : Set α} :
     (∃ x ∈ insert a s, P x) ↔ (P a ∨ ∃ x ∈ s, P x) := by
   simp [mem_insert_iff, or_and_right, exists_and_left, exists_or]
-#align set.bex_insert_iff Set.bex_insert_iff
+#align set.bex_insert_iff Set.exists_mem_insert
+@[deprecated] alias bex_insert_iff := exists_mem_insert -- 2024-03-23
 
-theorem ball_insert_iff {P : α → Prop} {a : α} {s : Set α} :
+theorem forall_mem_insert {P : α → Prop} {a : α} {s : Set α} :
     (∀ x ∈ insert a s, P x) ↔ P a ∧ ∀ x ∈ s, P x :=
-  ball_or_left.trans <| and_congr_left' forall_eq
-#align set.ball_insert_iff Set.ball_insert_iff
+  forall₂_or_left.trans <| and_congr_left' forall_eq
+#align set.ball_insert_iff Set.forall_mem_insert
+@[deprecated] alias ball_insert_iff := forall_mem_insert -- 2024-03-23
 
 /-! ### Lemmas about singletons -/
 

Mathlib/Data/Set/Finite.lean

@@ -1531,7 +1531,7 @@ theorem Finite.iSup_biInf_of_monotone {ι ι' α : Type*} [Preorder ι'] [Nonemp
     (hf : ∀ i ∈ s, Monotone (f i)) : ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j := by
   induction' s, hs using Set.Finite.dinduction_on with a s _ _ ihs hf
   · simp [iSup_const]
-  · rw [ball_insert_iff] at hf
+  · rw [forall_mem_insert] at hf
     simp only [iInf_insert, ← ihs hf.2]
     exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj
 #align set.finite.supr_binfi_of_monotone Set.Finite.iSup_biInf_of_monotone
@@ -1675,8 +1675,8 @@ protected theorem Finite.bddAbove (hs : s.Finite) : BddAbove s :=
 /-- A finite union of sets which are all bounded above is still bounded above. -/
 theorem Finite.bddAbove_biUnion {I : Set β} {S : β → Set α} (H : I.Finite) :
     BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i) :=
-  Finite.induction_on H (by simp only [biUnion_empty, bddAbove_empty, ball_empty_iff])
-    fun _ _ hs => by simp only [biUnion_insert, ball_insert_iff, bddAbove_union, hs]
+  Finite.induction_on H (by simp only [biUnion_empty, bddAbove_empty, forall_mem_empty])
+    fun _ _ hs => by simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]
 #align set.finite.bdd_above_bUnion Set.Finite.bddAbove_biUnion
 
 theorem infinite_of_not_bddAbove : ¬BddAbove s → s.Infinite :=

Mathlib/Data/Set/Function.lean

@@ -231,7 +231,7 @@ theorem EqOn.mono (hs : s₁ ⊆ s₂) (hf : EqOn f₁ f₂ s₂) : EqOn f₁ f
 
 @[simp]
 theorem eqOn_union : EqOn f₁ f₂ (s₁ ∪ s₂) ↔ EqOn f₁ f₂ s₁ ∧ EqOn f₁ f₂ s₂ :=
-  ball_or_left
+  forall₂_or_left
 #align set.eq_on_union Set.eqOn_union
 
 theorem EqOn.union (h₁ : EqOn f₁ f₂ s₁) (h₂ : EqOn f₁ f₂ s₂) : EqOn f₁ f₂ (s₁ ∪ s₂) :=

Mathlib/Data/Set/Image.lean

@@ -207,6 +207,7 @@ variable {f : α → β} {s t : Set α}
 -- Porting note: `Set.image` is already defined in `Init.Set`
 #align set.image Set.image
 
+@[deprecated mem_image] -- 2024-03-23
 theorem mem_image_iff_bex {f : α → β} {s : Set α} {y : β} :
     y ∈ f '' s ↔ ∃ (x : _) (_ : x ∈ s), f x = y :=
   bex_def.symm

Mathlib/Data/Set/Lattice.lean

@@ -1542,7 +1542,7 @@ theorem InjOn.image_iInter_eq [Nonempty ι] {s : ι → Set α} {f : α → β}
     (f '' ⋂ i, s i) = ⋂ i, f '' s i := by
   inhabit ι
   refine' Subset.antisymm (image_iInter_subset s f) fun y hy => _
-  simp only [mem_iInter, mem_image_iff_bex] at hy
+  simp only [mem_iInter, mem_image] at hy
   choose x hx hy using hy
   refine' ⟨x default, mem_iInter.2 fun i => _, hy _⟩
   suffices x default = x i by

Mathlib/Data/Sigma/Interval.lean

@@ -40,18 +40,18 @@ instance instLocallyFiniteOrder : LocallyFiniteOrder (Σ i, α i) where
   finsetIoo := sigmaLift fun _ => Ioo
   finset_mem_Icc := fun ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ => by
     simp_rw [mem_sigmaLift, le_def, mem_Icc, exists_and_left, ← exists_and_right, ← exists_prop]
-    exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
+    exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
   finset_mem_Ico := fun ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ => by
     simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ico, exists_and_left, ← exists_and_right, ←
       exists_prop]
-    exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
+    exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
   finset_mem_Ioc := fun ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ => by
     simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ioc, exists_and_left, ← exists_and_right, ←
       exists_prop]
-    exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
+    exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
   finset_mem_Ioo := fun ⟨i, a⟩ ⟨j, b⟩ ⟨k, c⟩ => by
     simp_rw [mem_sigmaLift, lt_def, mem_Ioo, exists_and_left, ← exists_and_right, ← exists_prop]
-    exact bex_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
+    exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩
 
 section
 

Mathlib/GroupTheory/GroupAction/Basic.lean

@@ -434,7 +434,7 @@ theorem quotient_preimage_image_eq_union_mul (U : Set α) :
   · intro hx
     rw [Set.mem_iUnion] at hx
     obtain ⟨g, u, hu₁, hu₂⟩ := hx
-    rw [Set.mem_preimage, Set.mem_image_iff_bex]
+    rw [Set.mem_preimage, Set.mem_image]
     refine' ⟨g⁻¹ • a, _, by simp only [f, Quotient.eq']; use g⁻¹⟩
     rw [← hu₂]
     convert hu₁

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -1402,8 +1402,7 @@ theorem coe_map (f : G →* N) (K : Subgroup G) : (K.map f : Set N) = f '' K :=
 #align add_subgroup.coe_map AddSubgroup.coe_map
 
 @[to_additive (attr := simp)]
-theorem mem_map {f : G →* N} {K : Subgroup G} {y : N} : y ∈ K.map f ↔ ∃ x ∈ K, f x = y := by
-  erw [mem_image_iff_bex]; simp
+theorem mem_map {f : G →* N} {K : Subgroup G} {y : N} : y ∈ K.map f ↔ ∃ x ∈ K, f x = y := Iff.rfl
 #align subgroup.mem_map Subgroup.mem_map
 #align add_subgroup.mem_map AddSubgroup.mem_map
 

Mathlib/GroupTheory/Submonoid/Operations.lean

@@ -231,9 +231,7 @@ theorem coe_map (f : F) (S : Submonoid M) : (S.map f : Set N) = f '' S :=
 #align add_submonoid.coe_map AddSubmonoid.coe_map
 
 @[to_additive (attr := simp)]
-theorem mem_map {f : F} {S : Submonoid M} {y : N} : y ∈ S.map f ↔ ∃ x ∈ S, f x = y := by
-  rw [← bex_def]
-  exact mem_image_iff_bex
+theorem mem_map {f : F} {S : Submonoid M} {y : N} : y ∈ S.map f ↔ ∃ x ∈ S, f x = y := Iff.rfl
 #align submonoid.mem_map Submonoid.mem_map
 #align add_submonoid.mem_map AddSubmonoid.mem_map
 

Mathlib/Init/Data/List/Instances.lean

@@ -63,12 +63,12 @@ variable {α : Type u} {p : α → Prop} [DecidablePred p]
 
 -- To work around lean4#2552, we call specific `Decidable` instances and use `match` on them,
 -- as opposed to using `if`.
-instance decidableBex : ∀ (l : List α), Decidable (∃ x ∈ l, p x)
+instance decidableExistsMem : ∀ (l : List α), Decidable (∃ x ∈ l, p x)
   | []    => isFalse (by simp)
   | x::xs =>
     match ‹DecidablePred p› x with
     | isTrue h₁ => isTrue ⟨x, mem_cons_self _ _, h₁⟩
-    | isFalse h₁ => match decidableBex xs with
+    | isFalse h₁ => match decidableExistsMem xs with
       | isTrue h₂  => isTrue <| by
         rcases h₂ with ⟨y, hm, hp⟩
         exact ⟨y, mem_cons_of_mem _ hm, hp⟩
@@ -77,14 +77,14 @@ instance decidableBex : ∀ (l : List α), Decidable (∃ x ∈ l, p x)
         cases mem_cons.1 hm with
         | inl h => rw [h] at hp; contradiction
         | inr h => exact absurd ⟨y, h, hp⟩ h₂
-#align list.decidable_bex List.decidableBex
+#align list.decidable_bex List.decidableExistsMem
 
-instance decidableBall (l : List α) : Decidable (∀ x ∈ l, p x) :=
+instance decidableForallMem (l : List α) : Decidable (∀ x ∈ l, p x) :=
   match (inferInstance : Decidable <| ∃ x ∈ l, ¬ p x) with
   | isFalse h => isTrue fun x hx => match ‹DecidablePred p› x with
     | isTrue h' => h'
     | isFalse h' => False.elim <| h ⟨x, hx, h'⟩
   | isTrue h => isFalse <| let ⟨x, h, np⟩ := h; fun al => np (al x h)
-#align list.decidable_ball List.decidableBall
+#align list.decidable_ball List.decidableForallMem
 
 end List

Mathlib/Init/Data/List/Lemmas.lean

@@ -72,20 +72,17 @@ alias ⟨eq_or_mem_of_mem_cons, _⟩ := mem_cons
 #align list.mem_append_left List.mem_append_left
 #align list.mem_append_right List.mem_append_right
 
-theorem not_bex_nil (p : α → Prop) : ¬∃ x ∈ @nil α, p x := fun ⟨_, hx, _⟩ => List.not_mem_nil _ hx
-#align list.not_bex_nil List.not_bex_nil
+theorem not_exists_mem_nil (p : α → Prop) : ¬∃ x ∈ @nil α, p x :=
+  fun ⟨_, hx, _⟩ => List.not_mem_nil _ hx
+#align list.not_bex_nil List.not_exists_mem_nil
 
 #align list.ball_nil List.forall_mem_nil
 
-theorem bex_cons (p : α → Prop) (a : α) (l : List α) : (∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x :=
-  ⟨fun ⟨x, h, px⟩ => by
-    simp only [find?, mem_cons] at h
-    cases' h with h h
-    · cases h; exact Or.inl px;
-    · exact Or.inr ⟨x, h, px⟩,
-  fun o =>
-    o.elim (fun pa => ⟨a, mem_cons_self _ _, pa⟩) fun ⟨x, h, px⟩ => ⟨x, mem_cons_of_mem _ h, px⟩⟩
-#align list.bex_cons List.bex_cons
+#align list.bex_cons List.exists_mem_cons
+
+-- 2024-03-23
+@[deprecated] alias not_bex_nil := not_exists_mem_nil
+@[deprecated] alias bex_cons := exists_mem_cons
 
 #align list.ball_cons List.forall_mem_consₓ