From 7b7bbd7381c5445de85b93339023d25bf6180931 Mon Sep 17 00:00:00 2001 From: grunweg Date: Mon, 8 Apr 2024 10:17:55 +0000 Subject: [PATCH] chore: remove more `bex` and `ball` from lemma names (#11615) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- Archive/Wiedijk100Theorems/Partition.lean | 2 +- Mathlib/Analysis/Convex/Basic.lean | 6 +- .../Analysis/LocallyConvex/WithSeminorms.lean | 2 +- Mathlib/Analysis/NormedSpace/Banach.lean | 2 +- .../Sites/EqualizerSheafCondition.lean | 6 +- Mathlib/CategoryTheory/Sites/IsSheafFor.lean | 2 +- .../SimpleGraph/Regularity/Increment.lean | 2 +- Mathlib/Data/Analysis/Topology.lean | 2 +- Mathlib/Data/Finset/Basic.lean | 5 +- Mathlib/Data/Finset/Image.lean | 4 +- Mathlib/Data/Finset/Lattice.lean | 2 +- Mathlib/Data/Finset/Prod.lean | 4 +- Mathlib/Data/List/Basic.lean | 2 - Mathlib/Data/List/Pairwise.lean | 2 +- Mathlib/Data/List/Sigma.lean | 2 +- Mathlib/Data/Nat/Squarefree.lean | 2 +- Mathlib/Data/Set/Basic.lean | 17 ++-- Mathlib/Data/Set/Finite.lean | 6 +- Mathlib/Data/Set/Function.lean | 2 +- Mathlib/Data/Set/Image.lean | 1 + Mathlib/Data/Set/Lattice.lean | 2 +- Mathlib/Data/Sigma/Interval.lean | 8 +- Mathlib/GroupTheory/GroupAction/Basic.lean | 2 +- Mathlib/GroupTheory/Subgroup/Basic.lean | 3 +- Mathlib/GroupTheory/Submonoid/Operations.lean | 4 +- Mathlib/Init/Data/List/Instances.lean | 10 +- Mathlib/Init/Data/List/Lemmas.lean | 19 ++-- .../AffineSpace/AffineSubspace.lean | 6 +- Mathlib/Logic/Basic.lean | 96 +++++++++++-------- Mathlib/MeasureTheory/SetSemiring.lean | 2 +- .../CanonicalEmbedding/ConvexBody.lean | 2 +- Mathlib/Order/Bounds/Basic.lean | 2 +- Mathlib/Order/Concept.lean | 2 +- Mathlib/Order/Directed.lean | 2 +- Mathlib/Order/Filter/AtTopBot.lean | 4 +- Mathlib/RingTheory/Ideal/Operations.lean | 2 +- .../NonUnitalSubsemiring/Basic.lean | 5 +- Mathlib/RingTheory/Subring/Basic.lean | 3 +- Mathlib/SetTheory/Ordinal/Arithmetic.lean | 8 +- Mathlib/SetTheory/Ordinal/FixedPoint.lean | 2 +- Mathlib/Topology/Algebra/UniformGroup.lean | 2 +- Mathlib/Topology/Basic.lean | 2 +- Mathlib/Topology/Connected/Basic.lean | 2 +- Mathlib/Topology/Constructions.lean | 4 +- Mathlib/Topology/ContinuousOn.lean | 2 +- Mathlib/Topology/EMetricSpace/Basic.lean | 2 +- Mathlib/Topology/GDelta.lean | 2 +- .../Topology/MetricSpace/MetricSeparated.lean | 2 +- Mathlib/Topology/UniformSpace/Basic.lean | 2 +- Mathlib/Topology/UniformSpace/Cauchy.lean | 4 +- 50 files changed, 147 insertions(+), 134 deletions(-) diff --git a/Archive/Wiedijk100Theorems/Partition.lean b/Archive/Wiedijk100Theorems/Partition.lean index 8eb6d3a404a80..22e19791ddd52 100644 --- a/Archive/Wiedijk100Theorems/Partition.lean +++ b/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 diff --git a/Mathlib/Analysis/Convex/Basic.lean b/Mathlib/Analysis/Convex/Basic.lean index 4d5c878671da4..211de17ebe645 100644 --- a/Mathlib/Analysis/Convex/Basic.lean +++ b/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) : diff --git a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean index 29b2ca36f7361..760ff00a15db3 100644 --- a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean +++ b/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) _ diff --git a/Mathlib/Analysis/NormedSpace/Banach.lean b/Mathlib/Analysis/NormedSpace/Banach.lean index 286d9e69214db..5fdc4fc10bcc4 100644 --- a/Mathlib/Analysis/NormedSpace/Banach.lean +++ b/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⟩ diff --git a/Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean b/Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean index 04ef7a4154186..942f2ce37e64d 100644 --- a/Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Sites/IsSheafFor.lean b/Mathlib/CategoryTheory/Sites/IsSheafFor.lean index 748f292ffc98f..3ccc2360047e8 100644 --- a/Mathlib/CategoryTheory/Sites/IsSheafFor.lean +++ b/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 diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean index 5915d0bb370c3..28847feda0f9b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean +++ b/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 diff --git a/Mathlib/Data/Analysis/Topology.lean b/Mathlib/Data/Analysis/Topology.lean index c9df222430bb1..cef6acc54fc1a 100644 --- a/Mathlib/Data/Analysis/Topology.lean +++ b/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 α} : diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean index 9f8f6b61f3053..fc159f4c66b8b 100644 --- a/Mathlib/Data/Finset/Basic.lean +++ b/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 diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean index 7e33febace88a..6846118b8b7fe 100644 --- a/Mathlib/Data/Finset/Image.lean +++ b/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 diff --git a/Mathlib/Data/Finset/Lattice.lean b/Mathlib/Data/Finset/Lattice.lean index 86dddac24ffb7..ce4d3f048b4ad 100644 --- a/Mathlib/Data/Finset/Lattice.lean +++ b/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] diff --git a/Mathlib/Data/Finset/Prod.lean b/Mathlib/Data/Finset/Prod.lean index 57dc5dbd25a1a..d7b3564b900ae 100644 --- a/Mathlib/Data/Finset/Prod.lean +++ b/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 (α × β)} : diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 332373951521f..4efff37627297 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/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 diff --git a/Mathlib/Data/List/Pairwise.lean b/Mathlib/Data/List/Pairwise.lean index 2446643894963..acf6eb71b6f0a 100644 --- a/Mathlib/Data/List/Pairwise.lean +++ b/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 _ _ diff --git a/Mathlib/Data/List/Sigma.lean b/Mathlib/Data/List/Sigma.lean index 35de455bb58da..be04d046c7395 100644 --- a/Mathlib/Data/List/Sigma.lean +++ b/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 diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean index e865d057235c2..26c1ced838014 100644 --- a/Mathlib/Data/Nat/Squarefree.lean +++ b/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 diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index cff07b75cf691..75f0196029d24 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/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 -/ diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean index d86767691c034..2d6c950c46ca3 100644 --- a/Mathlib/Data/Set/Finite.lean +++ b/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 := diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean index bef68f0704b13..eaa0fd3c93205 100644 --- a/Mathlib/Data/Set/Function.lean +++ b/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₂) := diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean index a73f680264f62..fec32f149642a 100644 --- a/Mathlib/Data/Set/Image.lean +++ b/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 diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean index 09827a0d9e010..2af73770cc644 100644 --- a/Mathlib/Data/Set/Lattice.lean +++ b/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 diff --git a/Mathlib/Data/Sigma/Interval.lean b/Mathlib/Data/Sigma/Interval.lean index 4bee080d4cffa..fdf8bf1575b69 100644 --- a/Mathlib/Data/Sigma/Interval.lean +++ b/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 diff --git a/Mathlib/GroupTheory/GroupAction/Basic.lean b/Mathlib/GroupTheory/GroupAction/Basic.lean index f31eeb8db2e9e..b1e5ba703f347 100644 --- a/Mathlib/GroupTheory/GroupAction/Basic.lean +++ b/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₁ diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean index 88e03142592aa..acb206fa558db 100644 --- a/Mathlib/GroupTheory/Subgroup/Basic.lean +++ b/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 diff --git a/Mathlib/GroupTheory/Submonoid/Operations.lean b/Mathlib/GroupTheory/Submonoid/Operations.lean index b882556e9b0e5..c8c92e231e2ae 100644 --- a/Mathlib/GroupTheory/Submonoid/Operations.lean +++ b/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 diff --git a/Mathlib/Init/Data/List/Instances.lean b/Mathlib/Init/Data/List/Instances.lean index 48ee9adfc54b4..49b8476a5c350 100644 --- a/Mathlib/Init/Data/List/Instances.lean +++ b/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 diff --git a/Mathlib/Init/Data/List/Lemmas.lean b/Mathlib/Init/Data/List/Lemmas.lean index 2b7f40d7ca428..70b50f0e6b51a 100644 --- a/Mathlib/Init/Data/List/Lemmas.lean +++ b/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ₓ diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean index 51b6a640f9a0d..93d805f1e8eff 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean @@ -296,7 +296,7 @@ theorem coe_direction_eq_vsub_set_left {s : AffineSubspace k P} {p : P} (hp : p (s.direction : Set V) = (p -ᵥ ·) '' s := by ext v rw [SetLike.mem_coe, ← Submodule.neg_mem_iff, ← SetLike.mem_coe, - coe_direction_eq_vsub_set_right hp, Set.mem_image_iff_bex, Set.mem_image_iff_bex] + coe_direction_eq_vsub_set_right hp, Set.mem_image, Set.mem_image] conv_lhs => congr ext @@ -1547,8 +1547,8 @@ theorem coe_map (s : AffineSubspace k P₁) : (s.map f : Set P₂) = f '' s := @[simp] theorem mem_map {f : P₁ →ᵃ[k] P₂} {x : P₂} {s : AffineSubspace k P₁} : - x ∈ s.map f ↔ ∃ y ∈ s, f y = x := by - simpa only [bex_def] using mem_image_iff_bex + x ∈ s.map f ↔ ∃ y ∈ s, f y = x := + Iff.rfl #align affine_subspace.mem_map AffineSubspace.mem_map theorem mem_map_of_mem {x : P₁} {s : AffineSubspace k P₁} (h : x ∈ s) : f x ∈ s.map f := diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index 8d548b900d932..eb97b4a40e665 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -517,15 +517,19 @@ alias Membership.mem.ne_of_not_mem' := ne_of_mem_of_not_mem' section Equality -- todo: change name -theorem ball_cond_comm {α} {s : α → Prop} {p : α → α → Prop} : +theorem forall_cond_comm {α} {s : α → Prop} {p : α → α → Prop} : (∀ a, s a → ∀ b, s b → p a b) ↔ ∀ a b, s a → s b → p a b := ⟨fun h a b ha hb ↦ h a ha b hb, fun h a ha b hb ↦ h a b ha hb⟩ -#align ball_cond_comm ball_cond_comm +#align ball_cond_comm forall_cond_comm -theorem ball_mem_comm {α β} [Membership α β] {s : β} {p : α → α → Prop} : +theorem forall_mem_comm {α β} [Membership α β] {s : β} {p : α → α → Prop} : (∀ a (_ : a ∈ s) b (_ : b ∈ s), p a b) ↔ ∀ a b, a ∈ s → b ∈ s → p a b := - ball_cond_comm -#align ball_mem_comm ball_mem_comm + forall_cond_comm +#align ball_mem_comm forall_mem_comm + +-- 2024-03-23 +@[deprecated] alias ball_cond_comm := forall_cond_comm +@[deprecated] alias ball_mem_comm := forall_mem_comm #align ne_of_apply_ne ne_of_apply_ne @@ -1052,18 +1056,18 @@ theorem BEx.intro (a : α) (h₁ : p a) (h₂ : P a h₁) : ∃ (x : _) (h : p x ⟨a, h₁, h₂⟩ #align bex.intro BEx.intro -theorem ball_congr (H : ∀ x h, P x h ↔ Q x h) : (∀ x h, P x h) ↔ ∀ x h, Q x h := - forall_congr' fun x ↦ forall_congr' (H x) -#align ball_congr ball_congr - -theorem bex_congr (H : ∀ x h, P x h ↔ Q x h) : (∃ x h, P x h) ↔ ∃ x h, Q x h := - exists_congr fun x ↦ exists_congr (H x) -#align bex_congr bex_congr +#align ball_congr forall₂_congr +#align bex_congr exists₂_congr +@[deprecated exists_eq_left] -- 2024-04-06 theorem bex_eq_left {a : α} : (∃ (x : _) (_ : x = a), p x) ↔ p a := by simp only [exists_prop, exists_eq_left] #align bex_eq_left bex_eq_left +-- 2024-04-06 +@[deprecated] alias ball_congr := forall₂_congr +@[deprecated] alias bex_congr := exists₂_congr + theorem BAll.imp_right (H : ∀ x h, P x h → Q x h) (h₁ : ∀ x h, P x h) (x h) : Q x h := H _ _ <| h₁ _ _ #align ball.imp_right BAll.imp_right @@ -1080,61 +1084,77 @@ theorem BEx.imp_left (H : ∀ x, p x → q x) : (∃ (x : _) (_ : p x), r x) → | ⟨x, hp, hr⟩ => ⟨x, H _ hp, hr⟩ #align bex.imp_left BEx.imp_left +@[deprecated id] -- 2024-03-23 theorem ball_of_forall (h : ∀ x, p x) (x) : p x := h x #align ball_of_forall ball_of_forall +@[deprecated forall_imp] -- 2024-03-23 theorem forall_of_ball (H : ∀ x, p x) (h : ∀ x, p x → q x) (x) : q x := h x <| H x #align forall_of_ball forall_of_ball -theorem bex_of_exists (H : ∀ x, p x) : (∃ x, q x) → ∃ (x : _) (_ : p x), q x +theorem exists_mem_of_exists (H : ∀ x, p x) : (∃ x, q x) → ∃ (x : _) (_ : p x), q x | ⟨x, hq⟩ => ⟨x, H x, hq⟩ -#align bex_of_exists bex_of_exists +#align bex_of_exists exists_mem_of_exists -theorem exists_of_bex : (∃ (x : _) (_ : p x), q x) → ∃ x, q x +theorem exists_of_exists_mem : (∃ (x : _) (_ : p x), q x) → ∃ x, q x | ⟨x, _, hq⟩ => ⟨x, hq⟩ -#align exists_of_bex exists_of_bex +#align exists_of_bex exists_of_exists_mem + +theorem exists₂_imp : (∃ x h, P x h) → b ↔ ∀ x h, P x h → b := by simp +#align bex_imp_distrib exists₂_imp -theorem bex_imp : (∃ x h, P x h) → b ↔ ∀ x h, P x h → b := by simp -#align bex_imp_distrib bex_imp +-- 2024-03-23 +@[deprecated] alias bex_of_exists := exists_mem_of_exists +@[deprecated] alias exists_of_bex := exists_of_exists_mem +@[deprecated] alias bex_imp := exists₂_imp -theorem not_bex : (¬∃ x h, P x h) ↔ ∀ x h, ¬P x h := bex_imp -#align not_bex not_bex +theorem not_exists_mem : (¬∃ x h, P x h) ↔ ∀ x h, ¬P x h := exists₂_imp +#align not_bex not_exists_mem -theorem not_ball_of_bex_not : (∃ x h, ¬P x h) → ¬∀ x h, P x h +theorem not_forall₂_of_exists₂_not : (∃ x h, ¬P x h) → ¬∀ x h, P x h | ⟨x, h, hp⟩, al => hp <| al x h -#align not_ball_of_bex_not not_ball_of_bex_not +#align not_ball_of_bex_not not_forall₂_of_exists₂_not -- See Note [decidable namespace] -protected theorem Decidable.not_ball [Decidable (∃ x h, ¬P x h)] [∀ x h, Decidable (P x h)] : +protected theorem Decidable.not_forall₂ [Decidable (∃ x h, ¬P x h)] [∀ x h, Decidable (P x h)] : (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h := ⟨Not.decidable_imp_symm fun nx x h ↦ nx.decidable_imp_symm - fun h' ↦ ⟨x, h, h'⟩, not_ball_of_bex_not⟩ -#align decidable.not_ball Decidable.not_ball + fun h' ↦ ⟨x, h, h'⟩, not_forall₂_of_exists₂_not⟩ +#align decidable.not_ball Decidable.not_forall₂ -theorem not_ball : (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h := Decidable.not_ball -#align not_ball not_ball +theorem not_forall₂ : (¬∀ x h, P x h) ↔ ∃ x h, ¬P x h := Decidable.not_forall₂ +#align not_ball not_forall₂ -theorem ball_true_iff (p : α → Prop) : (∀ x, p x → True) ↔ True := - iff_true_intro fun _ _ ↦ trivial -#align ball_true_iff ball_true_iff +#align ball_true_iff forall₂_true_iff -theorem ball_and : (∀ x h, P x h ∧ Q x h) ↔ (∀ x h, P x h) ∧ ∀ x h, Q x h := +theorem forall₂_and : (∀ x h, P x h ∧ Q x h) ↔ (∀ x h, P x h) ∧ ∀ x h, Q x h := Iff.trans (forall_congr' fun _ ↦ forall_and) forall_and -#align ball_and_distrib ball_and +#align ball_and_distrib forall₂_and -theorem bex_or : (∃ x h, P x h ∨ Q x h) ↔ (∃ x h, P x h) ∨ ∃ x h, Q x h := +theorem exists_mem_or : (∃ x h, P x h ∨ Q x h) ↔ (∃ x h, P x h) ∨ ∃ x h, Q x h := Iff.trans (exists_congr fun _ ↦ exists_or) exists_or -#align bex_or_distrib bex_or +#align bex_or_distrib exists_mem_or -theorem ball_or_left : (∀ x, p x ∨ q x → r x) ↔ (∀ x, p x → r x) ∧ ∀ x, q x → r x := +theorem forall₂_or_left : (∀ x, p x ∨ q x → r x) ↔ (∀ x, p x → r x) ∧ ∀ x, q x → r x := Iff.trans (forall_congr' fun _ ↦ or_imp) forall_and -#align ball_or_left_distrib ball_or_left +#align ball_or_left_distrib forall₂_or_left -theorem bex_or_left : +theorem exists_mem_or_left : (∃ (x : _) (_ : p x ∨ q x), r x) ↔ (∃ (x : _) (_ : p x), r x) ∨ ∃ (x : _) (_ : q x), r x := by simp only [exists_prop] exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or -#align bex_or_left_distrib bex_or_left +#align bex_or_left_distrib exists_mem_or_left + +-- 2023-03-23 +@[deprecated] alias not_ball_of_bex_not := not_forall₂_of_exists₂_not +@[deprecated] alias Decidable.not_ball := Decidable.not_forall₂ +@[deprecated] alias not_ball := not_forall₂ +@[deprecated] alias ball_true_iff := forall₂_true_iff +@[deprecated] alias ball_and := forall₂_and +@[deprecated] alias not_bex := not_exists_mem +@[deprecated] alias bex_or := exists_mem_or +@[deprecated] alias ball_or_left := forall₂_or_left +@[deprecated] alias bex_or_left := exists_mem_or_left end BoundedQuantifiers diff --git a/Mathlib/MeasureTheory/SetSemiring.lean b/Mathlib/MeasureTheory/SetSemiring.lean index 59d2d642e0e35..dfc753141b9a8 100644 --- a/Mathlib/MeasureTheory/SetSemiring.lean +++ b/Mathlib/MeasureTheory/SetSemiring.lean @@ -166,7 +166,7 @@ lemma exists_disjoint_finset_diff_eq (hC : IsSetSemiring C) (hs : s ∈ C) (hI : have hJ'_subset : ↑J' ⊆ C := by intro u simp only [J' ,Subtype.coe_mk, univ_eq_attach, coe_biUnion, mem_coe, mem_attach, iUnion_true, - mem_iUnion, Finset.exists_coe, bex_imp] + mem_iUnion, Finset.exists_coe, exists₂_imp] intro v hv huvt exact hJu_subset v (h_ss hv) huvt refine ⟨J', hJ'_subset, ?_, ?_⟩ diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean index a968f18f47ce9..9c69982747ade 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean @@ -64,7 +64,7 @@ theorem convexBodyLT_mem {x : K} : mixedEmbedding K x ∈ (convexBodyLT K f) ↔ ∀ w : InfinitePlace K, w x < f w := by simp_rw [mixedEmbedding, RingHom.prod_apply, Set.mem_prod, Set.mem_pi, Set.mem_univ, forall_true_left, mem_ball_zero_iff, Pi.ringHom_apply, ← Complex.norm_real, - embedding_of_isReal_apply, Subtype.forall, ← ball_or_left, ← not_isReal_iff_isComplex, em, + embedding_of_isReal_apply, Subtype.forall, ← forall₂_or_left, ← not_isReal_iff_isComplex, em, forall_true_left, norm_embedding_eq] theorem convexBodyLT_neg_mem (x : E K) (hx : x ∈ (convexBodyLT K f)) : diff --git a/Mathlib/Order/Bounds/Basic.lean b/Mathlib/Order/Bounds/Basic.lean index ec0714987aa83..9fea202ce07cc 100644 --- a/Mathlib/Order/Bounds/Basic.lean +++ b/Mathlib/Order/Bounds/Basic.lean @@ -868,7 +868,7 @@ theorem not_bddBelow_univ [NoMinOrder α] : ¬BddBelow (univ : Set α) := @[simp] theorem upperBounds_empty : upperBounds (∅ : Set α) = univ := by - simp only [upperBounds, eq_univ_iff_forall, mem_setOf_eq, ball_empty_iff, forall_true_iff] + simp only [upperBounds, eq_univ_iff_forall, mem_setOf_eq, forall_mem_empty, forall_true_iff] #align upper_bounds_empty upperBounds_empty @[simp] diff --git a/Mathlib/Order/Concept.lean b/Mathlib/Order/Concept.lean index 7fd2f26810c9b..bcfec875d9dfd 100644 --- a/Mathlib/Order/Concept.lean +++ b/Mathlib/Order/Concept.lean @@ -92,7 +92,7 @@ theorem extentClosure_empty : extentClosure r ∅ = univ := @[simp] theorem intentClosure_union (s₁ s₂ : Set α) : intentClosure r (s₁ ∪ s₂) = intentClosure r s₁ ∩ intentClosure r s₂ := - Set.ext fun _ => ball_or_left + Set.ext fun _ => forall₂_or_left #align intent_closure_union intentClosure_union @[simp] diff --git a/Mathlib/Order/Directed.lean b/Mathlib/Order/Directed.lean index 2fb710dc7c26a..0799554dee2c8 100644 --- a/Mathlib/Order/Directed.lean +++ b/Mathlib/Order/Directed.lean @@ -57,7 +57,7 @@ variable {r r'} theorem directedOn_iff_directed {s} : @DirectedOn α r s ↔ Directed r (Subtype.val : s → α) := by simp only [DirectedOn, Directed, Subtype.exists, exists_and_left, exists_prop, Subtype.forall] - exact ball_congr fun x _ => by simp [And.comm, and_assoc] + exact forall₂_congr fun x _ => by simp [And.comm, and_assoc] #align directed_on_iff_directed directedOn_iff_directed alias ⟨DirectedOn.directed_val, _⟩ := directedOn_iff_directed diff --git a/Mathlib/Order/Filter/AtTopBot.lean b/Mathlib/Order/Filter/AtTopBot.lean index 4cfb3cbf7c692..691212150f8f2 100644 --- a/Mathlib/Order/Filter/AtTopBot.lean +++ b/Mathlib/Order/Filter/AtTopBot.lean @@ -1571,12 +1571,12 @@ theorem eventually_atTop_prod_self [SemilatticeSup α] [Nonempty α] {p : α × theorem eventually_atBot_prod_self' [SemilatticeInf α] [Nonempty α] {p : α × α → Prop} : (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l) := by - simp only [eventually_atBot_prod_self, ball_cond_comm] + simp only [eventually_atBot_prod_self, forall_cond_comm] #align filter.eventually_at_bot_prod_self' Filter.eventually_atBot_prod_self' theorem eventually_atTop_prod_self' [SemilatticeSup α] [Nonempty α] {p : α × α → Prop} : (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l) := by - simp only [eventually_atTop_prod_self, ball_cond_comm] + simp only [eventually_atTop_prod_self, forall_cond_comm] #align filter.eventually_at_top_prod_self' Filter.eventually_atTop_prod_self' theorem eventually_atTop_curry [SemilatticeSup α] [SemilatticeSup β] {p : α × β → Prop} diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index 2b5511a16cf53..ee62fe64fd46d 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -1340,7 +1340,7 @@ theorem subset_union_prime {R : Type u} [CommRing R] {s : Finset ι} {f : ι → rw [Finset.coe_empty, Set.biUnion_empty, Set.subset_empty_iff] at h have : (I : Set R) ≠ ∅ := Set.Nonempty.ne_empty (Set.nonempty_of_mem I.zero_mem) exact absurd h this - · cases' hsne.bex with i his + · cases' hsne with i his obtain ⟨t, _, rfl⟩ : ∃ t, i ∉ t ∧ insert i t = s := ⟨s.erase i, Finset.not_mem_erase i s, Finset.insert_erase his⟩ have hp' : ∀ j ∈ t, IsPrime (f j) := by diff --git a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean index 442a388b4319d..cac04ecbb1a4b 100644 --- a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean +++ b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean @@ -303,9 +303,8 @@ theorem coe_map (f : F) (s : NonUnitalSubsemiring R) : (s.map f : Set S) = f '' #align non_unital_subsemiring.coe_map NonUnitalSubsemiring.coe_map @[simp] -theorem mem_map {f : F} {s : NonUnitalSubsemiring R} {y : S} : y ∈ s.map f ↔ ∃ x ∈ s, f x = y := by - convert Set.mem_image_iff_bex - simp +theorem mem_map {f : F} {s : NonUnitalSubsemiring R} {y : S} : y ∈ s.map f ↔ ∃ x ∈ s, f x = y := + Iff.rfl #align non_unital_subsemiring.mem_map NonUnitalSubsemiring.mem_map @[simp] diff --git a/Mathlib/RingTheory/Subring/Basic.lean b/Mathlib/RingTheory/Subring/Basic.lean index 860ec86deac32..b01b3577a5c87 100644 --- a/Mathlib/RingTheory/Subring/Basic.lean +++ b/Mathlib/RingTheory/Subring/Basic.lean @@ -548,8 +548,7 @@ theorem coe_map (f : R →+* S) (s : Subring R) : (s.map f : Set S) = f '' s := #align subring.coe_map Subring.coe_map @[simp] -theorem mem_map {f : R →+* S} {s : Subring R} {y : S} : y ∈ s.map f ↔ ∃ x ∈ s, f x = y := - Set.mem_image_iff_bex.trans <| by simp +theorem mem_map {f : R →+* S} {s : Subring R} {y : S} : y ∈ s.map f ↔ ∃ x ∈ s, f x = y := Iff.rfl #align subring.mem_map Subring.mem_map @[simp] diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean index b871a697cb68a..a13c89cc1caee 100644 --- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean @@ -271,7 +271,7 @@ theorem limit_le {o} (h : IsLimit o) {a} : o ≤ a ↔ ∀ x < o, x ≤ a := theorem lt_limit {o} (h : IsLimit o) {a} : a < o ↔ ∃ x < o, a < x := by -- Porting note: `bex_def` is required. - simpa only [not_ball, not_le, bex_def] using not_congr (@limit_le _ h a) + simpa only [not_forall₂, not_le, bex_def] using not_congr (@limit_le _ h a) #align ordinal.lt_limit Ordinal.lt_limit @[simp] @@ -454,11 +454,11 @@ theorem IsNormal.le_set {f o} (H : IsNormal f) (p : Set Ordinal) (p0 : p.Nonempt rw [this] at px exact h _ px | H₂ S _ => - rcases not_ball.1 (mt (H₂ S).2 <| (lt_succ S).not_le) with ⟨a, h₁, h₂⟩ + rcases not_forall₂.1 (mt (H₂ S).2 <| (lt_succ S).not_le) with ⟨a, h₁, h₂⟩ exact (H.le_iff.2 <| succ_le_of_lt <| not_le.1 h₂).trans (h _ h₁) | H₃ S L _ => refine' (H.2 _ L _).2 fun a h' => _ - rcases not_ball.1 (mt (H₂ a).2 h'.not_le) with ⟨b, h₁, h₂⟩ + rcases not_forall₂.1 (mt (H₂ a).2 h'.not_le) with ⟨b, h₁, h₂⟩ exact (H.le_iff.2 <| (not_le.1 h₂).le).trans (h _ h₁)⟩ #align ordinal.is_normal.le_set Ordinal.IsNormal.le_set @@ -813,7 +813,7 @@ theorem mul_isNormal {a : Ordinal} (h : 0 < a) : IsNormal (a * ·) := theorem lt_mul_of_limit {a b c : Ordinal} (h : IsLimit c) : a < b * c ↔ ∃ c' < c, a < b * c' := by -- Porting note: `bex_def` is required. - simpa only [not_ball, not_le, bex_def] using not_congr (@mul_le_of_limit b c a h) + simpa only [not_forall₂, not_le, bex_def] using not_congr (@mul_le_of_limit b c a h) #align ordinal.lt_mul_of_limit Ordinal.lt_mul_of_limit theorem mul_lt_mul_iff_left {a b c : Ordinal} (a0 : 0 < a) : a * b < a * c ↔ b < c := diff --git a/Mathlib/SetTheory/Ordinal/FixedPoint.lean b/Mathlib/SetTheory/Ordinal/FixedPoint.lean index d0087b85c50a3..f5512154ab021 100644 --- a/Mathlib/SetTheory/Ordinal/FixedPoint.lean +++ b/Mathlib/SetTheory/Ordinal/FixedPoint.lean @@ -213,7 +213,7 @@ theorem le_iff_derivFamily (H : ∀ i, IsNormal (f i)) {a} : · intro h₁ cases' eq_or_lt_of_le h₁ with h h · exact ⟨_, h.symm⟩ - rw [derivFamily_limit _ l, ← not_le, bsup_le_iff, not_ball] at h + rw [derivFamily_limit _ l, ← not_le, bsup_le_iff, not_forall₂] at h exact let ⟨o', h, hl⟩ := h IH o' h (le_of_not_le hl), diff --git a/Mathlib/Topology/Algebra/UniformGroup.lean b/Mathlib/Topology/Algebra/UniformGroup.lean index 8ed68be455726..b3f11ee83ea88 100644 --- a/Mathlib/Topology/Algebra/UniformGroup.lean +++ b/Mathlib/Topology/Algebra/UniformGroup.lean @@ -768,7 +768,7 @@ private theorem extend_Z_bilin_aux (x₀ : α) (y₁ : δ) : ∃ U₂ ∈ comap simpa using hφ.tendsto (0, y₁) have lim := lim2.comp lim1 rw [tendsto_prod_self_iff] at lim - simp_rw [ball_mem_comm] + simp_rw [forall_mem_comm] exact lim W' W'_nhd #noalign dense_inducing.extend_Z_bilin_aux diff --git a/Mathlib/Topology/Basic.lean b/Mathlib/Topology/Basic.lean index 144584cbbb8ac..ebe1fb565ca4e 100644 --- a/Mathlib/Topology/Basic.lean +++ b/Mathlib/Topology/Basic.lean @@ -130,7 +130,7 @@ lemma isOpen_iff_of_cover {f : α → Set X} (ho : ∀ i, IsOpen (f i)) (hU : ( theorem Set.Finite.isOpen_sInter {s : Set (Set X)} (hs : s.Finite) : (∀ t ∈ s, IsOpen t) → IsOpen (⋂₀ s) := Finite.induction_on hs (fun _ => by rw [sInter_empty]; exact isOpen_univ) fun _ _ ih h => by - simp only [sInter_insert, ball_insert_iff] at h ⊢ + simp only [sInter_insert, forall_mem_insert] at h ⊢ exact h.1.inter (ih h.2) #align is_open_sInter Set.Finite.isOpen_sInter diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index 0636626335e95..75ac97ddcd97c 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -1057,7 +1057,7 @@ theorem isConnected_iff_sUnion_disjoint_open {s : Set α} : · induction U using Finset.induction_on with | empty => exact absurd (by simpa using hsU) hne.not_subset_empty | @insert u U uU IH => - simp only [← ball_cond_comm, Finset.forall_mem_insert, Finset.exists_mem_insert, + simp only [← forall_cond_comm, Finset.forall_mem_insert, Finset.exists_mem_insert, Finset.coe_insert, sUnion_insert, implies_true, true_and] at * refine (h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_ · refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_ diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index 033eb2b958204..a18ba36a9c1f8 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -1420,7 +1420,7 @@ theorem isOpen_pi_iff {s : Set (∀ a, π a)} : (∀ a, a ∈ I → IsOpen (u a) ∧ f a ∈ u a) ∧ (I : Set ι).pi u ⊆ s := by rw [isOpen_iff_nhds] simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff] - refine ball_congr fun a _ => ⟨?_, ?_⟩ + refine forall₂_congr fun a _ => ⟨?_, ?_⟩ · rintro ⟨I, t, ⟨h1, h2⟩⟩ refine ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩ · simp_rw [Set.eval_image_pi (Finset.mem_coe.mpr hi) @@ -1447,7 +1447,7 @@ theorem isOpen_pi_iff' [Finite ι] {s : Set (∀ a, π a)} : cases nonempty_fintype ι rw [isOpen_iff_nhds] simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff] - refine ball_congr fun a _ => ⟨?_, ?_⟩ + refine forall₂_congr fun a _ => ⟨?_, ?_⟩ · rintro ⟨I, t, ⟨h1, h2⟩⟩ refine ⟨fun i => (h1 i).choose, diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index b98b1ddf1c274..bee579457cdf3 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/Mathlib/Topology/ContinuousOn.lean @@ -908,7 +908,7 @@ theorem ContinuousWithinAt.continuousAt {f : α → β} {s : Set α} {x : α} theorem IsOpen.continuousOn_iff {f : α → β} {s : Set α} (hs : IsOpen s) : ContinuousOn f s ↔ ∀ ⦃a⦄, a ∈ s → ContinuousAt f a := - ball_congr fun _ => continuousWithinAt_iff_continuousAt ∘ hs.mem_nhds + forall₂_congr fun _ => continuousWithinAt_iff_continuousAt ∘ hs.mem_nhds #align is_open.continuous_on_iff IsOpen.continuousOn_iff theorem ContinuousOn.continuousAt {f : α → β} {s : Set α} {x : α} (h : ContinuousOn f s) diff --git a/Mathlib/Topology/EMetricSpace/Basic.lean b/Mathlib/Topology/EMetricSpace/Basic.lean index 5d38a7551daac..72329f8e56176 100644 --- a/Mathlib/Topology/EMetricSpace/Basic.lean +++ b/Mathlib/Topology/EMetricSpace/Basic.lean @@ -951,7 +951,7 @@ theorem diam_iUnion_mem_option {ι : Type*} (o : Option ι) (s : ι → Set α) theorem diam_insert : diam (insert x s) = max (⨆ y ∈ s, edist x y) (diam s) := eq_of_forall_ge_iff fun d => by - simp only [diam_le_iff, ball_insert_iff, edist_self, edist_comm x, max_le_iff, iSup_le_iff, + simp only [diam_le_iff, forall_mem_insert, edist_self, edist_comm x, max_le_iff, iSup_le_iff, zero_le, true_and_iff, forall_and, and_self_iff, ← and_assoc] #align emetric.diam_insert EMetric.diam_insert diff --git a/Mathlib/Topology/GDelta.lean b/Mathlib/Topology/GDelta.lean index d21788fff17fe..fac61c1c2eb4b 100644 --- a/Mathlib/Topology/GDelta.lean +++ b/Mathlib/Topology/GDelta.lean @@ -154,7 +154,7 @@ theorem IsGδ.sUnion {S : Set (Set X)} (hS : S.Finite) (h : ∀ s ∈ S, IsGδ s induction S, hS using Set.Finite.dinduction_on with | H0 => simp | H1 _ _ ih => - simp only [ball_insert_iff, sUnion_insert] at * + simp only [forall_mem_insert, sUnion_insert] at * exact h.1.union (ih h.2) /-- The union of finitely many Gδ sets is a Gδ set, bounded indexed union version. -/ diff --git a/Mathlib/Topology/MetricSpace/MetricSeparated.lean b/Mathlib/Topology/MetricSpace/MetricSeparated.lean index c67a11afb99e8..d2fc7268cf23e 100644 --- a/Mathlib/Topology/MetricSpace/MetricSeparated.lean +++ b/Mathlib/Topology/MetricSpace/MetricSeparated.lean @@ -106,7 +106,7 @@ theorem union_right_iff {t'} : theorem finite_iUnion_left_iff {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set X} {t : Set X} : IsMetricSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, IsMetricSeparated (s i) t := by refine' Finite.induction_on hI (by simp) @fun i I _ _ hI => _ - rw [biUnion_insert, ball_insert_iff, union_left_iff, hI] + rw [biUnion_insert, forall_mem_insert, union_left_iff, hI] #align is_metric_separated.finite_Union_left_iff IsMetricSeparated.finite_iUnion_left_iff alias ⟨_, finite_iUnion_left⟩ := finite_iUnion_left_iff diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean index 24c8d9199c49c..eafadc79a3aac 100644 --- a/Mathlib/Topology/UniformSpace/Basic.lean +++ b/Mathlib/Topology/UniformSpace/Basic.lean @@ -1131,7 +1131,7 @@ theorem Filter.HasBasis.uniformContinuousOn_iff {ι'} [UniformSpace β] {p : ι UniformContinuousOn f S ↔ ∀ i, q i → ∃ j, p j ∧ ∀ x, x ∈ S → ∀ y, y ∈ S → (x, y) ∈ s j → (f x, f y) ∈ t i := ((ha.inf_principal (S ×ˢ S)).tendsto_iff hb).trans <| by - simp_rw [Prod.forall, Set.inter_comm (s _), ball_mem_comm, mem_inter_iff, mem_prod, and_imp] + simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp] #align filter.has_basis.uniform_continuous_on_iff Filter.HasBasis.uniformContinuousOn_iff end UniformSpace diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean index 59613efb4e4af..c657f579a2043 100644 --- a/Mathlib/Topology/UniformSpace/Cauchy.lean +++ b/Mathlib/Topology/UniformSpace/Cauchy.lean @@ -43,7 +43,7 @@ theorem Filter.HasBasis.cauchy_iff {ι} {p : ι → Prop} {s : ι → Set (α × Cauchy f ↔ NeBot f ∧ ∀ i, p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i := and_congr Iff.rfl <| (f.basis_sets.prod_self.le_basis_iff h).trans <| by - simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, ball_mem_comm] + simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm] #align filter.has_basis.cauchy_iff Filter.HasBasis.cauchy_iff theorem cauchy_iff' {f : Filter α} : @@ -53,7 +53,7 @@ theorem cauchy_iff' {f : Filter α} : theorem cauchy_iff {f : Filter α} : Cauchy f ↔ NeBot f ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s := cauchy_iff'.trans <| by - simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, ball_mem_comm] + simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm] #align cauchy_iff cauchy_iff lemma cauchy_iff_le {l : Filter α} [hl : l.NeBot] :