From 3c21b209b5bf2927a35ced44c4e0fb1972656383 Mon Sep 17 00:00:00 2001 From: Peter Nelson <71660771+apnelson1@users.noreply.github.com> Date: Wed, 28 Jun 2023 00:29:19 +0000 Subject: [PATCH] feat(Data.Set.Basic/Data.Finset.Basic): rename insert_subset (#5450) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Currently, (for both `Set` and `Finset`) `insert_subset` is an `iff` lemma stating that `insert a s ⊆ t` if and only if `a ∈ t` and `s ⊆ t`. For both types, this PR renames this lemma to `insert_subset_iff`, and adds an `insert_subset` lemma that gives the implication just in the reverse direction : namely `theorem insert_subset (ha : a ∈ t) (hs : s ⊆ t) : insert a s ⊆ t` . This both aligns the naming with `union_subset` and `union_subset_iff`, and removes the need for the awkward `insert_subset.mpr ⟨_,_⟩` idiom. It touches a lot of files (too many to list), but in a trivial way. --- Mathlib/Algebra/BigOperators/Basic.lean | 2 +- Mathlib/Algebra/BigOperators/Order.lean | 2 +- .../Analysis/BoxIntegral/Partition/Split.lean | 2 +- Mathlib/Analysis/Convex/Between.lean | 2 +- Mathlib/Analysis/Convex/Hull.lean | 2 +- Mathlib/Analysis/Convex/Segment.lean | 4 +-- Mathlib/Analysis/Convex/StoneSeparation.lean | 2 +- Mathlib/Analysis/Convex/Topology.lean | 2 +- .../Combinatorics/Additive/RuzsaCovering.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Basic.lean | 2 +- Mathlib/Computability/TMToPartrec.lean | 4 +-- Mathlib/Data/Finset/Basic.lean | 16 +++++---- Mathlib/Data/Finset/NAry.lean | 4 +-- Mathlib/Data/Polynomial/Coeff.lean | 4 +-- Mathlib/Data/Set/Basic.lean | 15 +++++---- Mathlib/Data/Set/Finite.lean | 2 +- Mathlib/Data/Set/Intervals/Basic.lean | 2 +- Mathlib/Data/Set/Intervals/OrdConnected.lean | 2 +- Mathlib/Data/Set/List.lean | 2 +- Mathlib/FieldTheory/Adjoin.lean | 2 +- Mathlib/Geometry/Euclidean/Angle/Sphere.lean | 6 ++-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean | 2 +- Mathlib/GroupTheory/Perm/Cycle/Basic.lean | 2 +- Mathlib/GroupTheory/Perm/Cycle/Type.lean | 2 +- .../AffineSpace/AffineSubspace.lean | 2 +- .../AffineSpace/FiniteDimensional.lean | 2 +- Mathlib/LinearAlgebra/Lagrange.lean | 8 ++--- Mathlib/LinearAlgebra/LinearIndependent.lean | 4 +-- Mathlib/LinearAlgebra/Span.lean | 4 +-- Mathlib/MeasureTheory/Covering/Vitali.lean | 2 +- Mathlib/ModelTheory/Types.lean | 2 +- Mathlib/Order/CompactlyGenerated.lean | 4 +-- Mathlib/Order/Cover.lean | 2 +- Mathlib/Order/Filter/CountableInter.lean | 2 +- Mathlib/Order/SupIndep.lean | 2 +- Mathlib/RingTheory/Adjoin/Basic.lean | 4 +-- Mathlib/RingTheory/Finiteness.lean | 2 +- Mathlib/RingTheory/IntegralClosure.lean | 9 +++-- .../Polynomial/Cyclotomic/Roots.lean | 2 +- Mathlib/SetTheory/Ordinal/Topology.lean | 2 +- Mathlib/Topology/Algebra/Order/Compact.lean | 2 +- Mathlib/Topology/Connected.lean | 33 ++++++++++++------- Mathlib/Topology/Order/Basic.lean | 2 +- 43 files changed, 99 insertions(+), 78 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index 5bd20e923b36a..1ecc4252b4641 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Basic.lean @@ -812,7 +812,7 @@ theorem prod_eq_mul_of_mem {s : Finset α} {f : α → β} (a b : α) (ha : a (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) : (∏ x in s, f x) = f a * f b := by haveI := Classical.decEq α; let s' := ({a, b} : Finset α) have hu : s' ⊆ s := by - refine' insert_subset.mpr _ + refine' insert_subset_iff.mpr _ apply And.intro ha apply singleton_subset_iff.mpr hb have hf : ∀ c ∈ s, c ∉ s' → f c = 1 := by diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean index f4e8cfed410e4..eb671dbb18058 100644 --- a/Mathlib/Algebra/BigOperators/Order.lean +++ b/Mathlib/Algebra/BigOperators/Order.lean @@ -486,7 +486,7 @@ theorem prod_lt_prod_of_subset' (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i exact lt_mul_of_one_lt_left' (∏ j in s, f j) hlt _ ≤ ∏ j in t, f j := by apply prod_le_prod_of_subset_of_one_le' - · simp [Finset.insert_subset, h, ht] + · simp [Finset.insert_subset_iff, h, ht] · intro x hx h'x simp only [mem_insert, not_or] at h'x exact hle x hx h'x.2 diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean index 6c4a7334ff130..db7a922a51e0c 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean @@ -285,7 +285,7 @@ a box `I` into subboxes. Let `Js` be one of them. If `J` and `Js` have nonempty theorem not_disjoint_imp_le_of_subset_of_mem_splitMany {I J Js : Box ι} {s : Finset (ι × ℝ)} (H : ∀ i, {(i, J.lower i), (i, J.upper i)} ⊆ s) (HJs : Js ∈ splitMany I s) (Hn : ¬Disjoint (J : WithBot (Box ι)) Js) : Js ≤ J := by - simp only [Finset.insert_subset, Finset.singleton_subset_iff] at H + simp only [Finset.insert_subset_iff, Finset.singleton_subset_iff] at H rcases Box.not_disjoint_coe_iff_nonempty_inter.mp Hn with ⟨x, hx, hxs⟩ refine' fun y hy i => ⟨_, _⟩ · rcases splitMany_le_split I (H i).1 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.lower i), Hle⟩ diff --git a/Mathlib/Analysis/Convex/Between.lean b/Mathlib/Analysis/Convex/Between.lean index 6a1da53269c10..92dc428d0ee96 100644 --- a/Mathlib/Analysis/Convex/Between.lean +++ b/Mathlib/Analysis/Convex/Between.lean @@ -617,7 +617,7 @@ theorem sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair [NoZeroSMulDivisors R V] refine' affineSpan_pair_le_of_mem_of_mem (mem_affineSpan R (Set.mem_range_self _)) _ have hle : line[R, t.points i₂, t.points i₃] ≤ affineSpan R (Set.range t.points) := by refine' affineSpan_mono R _ - simp [Set.insert_subset] + simp [Set.insert_subset_iff] rw [AffineSubspace.le_def'] at hle exact hle _ h₁.wbtw.mem_affineSpan rw [AffineSubspace.le_def'] at hle diff --git a/Mathlib/Analysis/Convex/Hull.lean b/Mathlib/Analysis/Convex/Hull.lean index 8af57e25481c4..2bd98e0ccd1c7 100644 --- a/Mathlib/Analysis/Convex/Hull.lean +++ b/Mathlib/Analysis/Convex/Hull.lean @@ -135,7 +135,7 @@ theorem convexHull_singleton (x : E) : convexHull 𝕜 ({x} : Set E) = {x} := theorem convexHull_pair (x y : E) : convexHull 𝕜 {x, y} = segment 𝕜 x y := by refine (convexHull_min ?_ <| convex_segment _ _).antisymm (segment_subset_convexHull (mem_insert _ _) <| subset_insert _ _ <| mem_singleton _) - rw [insert_subset, singleton_subset_iff] + rw [insert_subset_iff, singleton_subset_iff] exact ⟨left_mem_segment _ _ _, right_mem_segment _ _ _⟩ #align convex_hull_pair convexHull_pair diff --git a/Mathlib/Analysis/Convex/Segment.lean b/Mathlib/Analysis/Convex/Segment.lean index 832c5844e2e11..f39c97a087895 100644 --- a/Mathlib/Analysis/Convex/Segment.lean +++ b/Mathlib/Analysis/Convex/Segment.lean @@ -139,7 +139,7 @@ theorem segment_same (x : E) : [x -[𝕜] x] = {x} := theorem insert_endpoints_openSegment (x y : E) : insert x (insert y (openSegment 𝕜 x y)) = [x -[𝕜] y] := by - simp only [subset_antisymm_iff, insert_subset, left_mem_segment, right_mem_segment, + simp only [subset_antisymm_iff, insert_subset_iff, left_mem_segment, right_mem_segment, openSegment_subset_segment, true_and_iff] rintro z ⟨a, b, ha, hb, hab, rfl⟩ refine' hb.eq_or_gt.imp _ fun hb' => ha.eq_or_gt.imp _ fun ha' => _ @@ -160,7 +160,7 @@ theorem mem_openSegment_of_ne_left_right (hx : x ≠ z) (hy : y ≠ z) (hz : z theorem openSegment_subset_iff_segment_subset (hx : x ∈ s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s := by - simp only [← insert_endpoints_openSegment, insert_subset, *, true_and_iff] + simp only [← insert_endpoints_openSegment, insert_subset_iff, *, true_and_iff] #align open_segment_subset_iff_segment_subset openSegment_subset_iff_segment_subset end Module diff --git a/Mathlib/Analysis/Convex/StoneSeparation.lean b/Mathlib/Analysis/Convex/StoneSeparation.lean index bf646bb4d3e52..8e14a07a86792 100644 --- a/Mathlib/Analysis/Convex/StoneSeparation.lean +++ b/Mathlib/Analysis/Convex/StoneSeparation.lean @@ -102,7 +102,7 @@ theorem exists_convex_convex_compl_subset (hs : Convex 𝕜 s) (ht : Convex 𝕜 refine' not_disjoint_segment_convexHull_triple hz hu hv (hC.2.symm.mono (ht.segment_subset hut hvt) <| convexHull_min _ hC.1) - simpa [insert_subset, hp, hq, singleton_subset_iff.2 hzC] + simpa [insert_subset_iff, hp, hq, singleton_subset_iff.2 hzC] rintro c hc by_contra' h suffices h : Disjoint (convexHull 𝕜 (insert c C)) t diff --git a/Mathlib/Analysis/Convex/Topology.lean b/Mathlib/Analysis/Convex/Topology.lean index 3a7a491a868da..1de24f2d77a1d 100644 --- a/Mathlib/Analysis/Convex/Topology.lean +++ b/Mathlib/Analysis/Convex/Topology.lean @@ -259,7 +259,7 @@ protected theorem Convex.strictConvex' {s : Set E} (hs : Convex 𝕜 s) by_cases hy' : y ∈ interior s · exact hs.openSegment_self_interior_subset_interior hx hy' rcases h ⟨hx, hx'⟩ ⟨hy, hy'⟩ hne with ⟨c, hc⟩ - refine' (openSegment_subset_union x y ⟨c, rfl⟩).trans (insert_subset.2 ⟨hc, union_subset _ _⟩) + refine' (openSegment_subset_union x y ⟨c, rfl⟩).trans (insert_subset_iff.2 ⟨hc, union_subset _ _⟩) exacts [hs.openSegment_self_interior_subset_interior hx hc, hs.openSegment_interior_self_subset_interior hc hy] #align convex.strict_convex' Convex.strictConvex' diff --git a/Mathlib/Combinatorics/Additive/RuzsaCovering.lean b/Mathlib/Combinatorics/Additive/RuzsaCovering.lean index 452acf505e73c..400a4095a96c4 100644 --- a/Mathlib/Combinatorics/Additive/RuzsaCovering.lean +++ b/Mathlib/Combinatorics/Additive/RuzsaCovering.lean @@ -46,7 +46,7 @@ theorem exists_subset_mul_div (ht : t.Nonempty) : · exact subset_mul_left _ ht.one_mem_div hau by_cases H : ∀ b ∈ u, Disjoint (a • t) (b • t) · refine' (hCmax _ _ <| ssubset_insert hau).elim - rw [mem_filter, mem_powerset, insert_subset, coe_insert] + rw [mem_filter, mem_powerset, insert_subset_iff, coe_insert] exact ⟨⟨ha, hu.1⟩, hu.2.insert fun _ hb _ ↦ H _ hb⟩ push_neg at H simp_rw [not_disjoint_iff, ← inv_smul_mem_iff] at H diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index 92c4dec377798..657fdfa111e69 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -1620,7 +1620,7 @@ theorem Adj.card_commonNeighbors_lt_degree {G : SimpleGraph V} [DecidableRel G.A rw [Finset.ssubset_iff] use w constructor - · rw [Finset.insert_subset] + · rw [Finset.insert_subset_iff] constructor · simpa · rw [neighborFinset, Set.toFinset_subset_toFinset] diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index 376f4cff4315e..e24b1f8c24d84 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -1956,7 +1956,7 @@ theorem trStmts₁_supports {S q} (H₁ : (q : Λ').Supports S) (HS₁ : trStmts induction' q with _ _ _ q q_ih _ _ q q_ih q q_ih _ _ q q_ih q q_ih q q_ih q₁ q₂ q₁_ih q₂_ih _ <;> simp [trStmts₁, -Finset.singleton_subset_iff] at HS₁ ⊢ any_goals - cases' Finset.insert_subset.1 HS₁ with h₁ h₂ + cases' Finset.insert_subset_iff.1 HS₁ with h₁ h₂ first | have h₃ := h₂ W | try simp [Finset.subset_iff] at h₂ · exact supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩ -- move · exact supports_insert.2 ⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩ -- clear @@ -2033,7 +2033,7 @@ theorem codeSupp'_supports {S c k} (H : codeSupp c k ⊆ S) : Supports (codeSupp refine' supports_union.2 ⟨IHf H'.2, _⟩ refine' trStmts₁_supports' (trNormal_supports _) (Finset.union_subset_right h) fun _ => _ · simp only [codeSupp', codeSupp, Finset.union_subset_iff, contSupp, trStmts₁, - Finset.insert_subset] at h H ⊢ + Finset.insert_subset_iff] at h H ⊢ exact ⟨h.1, ⟨H.1.1, h⟩, H.2⟩ exact supports_singleton.2 (ret_supports <| Finset.union_subset_right H) #align turing.partrec_to_TM2.code_supp'_supports Turing.PartrecToTM2.codeSupp'_supports diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean index 28804da921cf1..765f5dcafbf89 100644 --- a/Mathlib/Data/Finset/Basic.lean +++ b/Mathlib/Data/Finset/Basic.lean @@ -810,7 +810,8 @@ theorem eq_singleton_or_nontrivial (ha : a ∈ s) : s = {a} ∨ (s : Set α).Non theorem Nonempty.exists_eq_singleton_or_nontrivial : s.Nonempty → (∃ a, s = {a}) ∨ (s : Set α).Nontrivial := fun ⟨a, ha⟩ => (eq_singleton_or_nontrivial ha).imp_left <| Exists.intro a -#align finset.nonempty.exists_eq_singleton_or_nontrivial Finset.Nonempty.exists_eq_singleton_or_nontrivial +#align finset.nonempty.exists_eq_singleton_or_nontrivial + Finset.Nonempty.exists_eq_singleton_or_nontrivial instance [Nonempty α] : Nontrivial (Finset α) := ‹Nonempty α›.elim fun a => ⟨⟨{a}, ∅, singleton_ne_empty _⟩⟩ @@ -1163,15 +1164,18 @@ theorem ne_insert_of_not_mem (s t : Finset α) {a : α} (h : a ∉ s) : s ≠ in simp [h] #align finset.ne_insert_of_not_mem Finset.ne_insert_of_not_mem -theorem insert_subset : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by +theorem insert_subset_iff : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by simp only [subset_iff, mem_insert, forall_eq, or_imp, forall_and] -#align finset.insert_subset Finset.insert_subset +#align finset.insert_subset Finset.insert_subset_iff + +theorem insert_subset (ha : a ∈ t) (hs : s ⊆ t) : insert a s ⊆ t := + insert_subset_iff.mpr ⟨ha,hs⟩ theorem subset_insert (a : α) (s : Finset α) : s ⊆ insert a s := fun _b => mem_insert_of_mem #align finset.subset_insert Finset.subset_insert theorem insert_subset_insert (a : α) {s t : Finset α} (h : s ⊆ t) : insert a s ⊆ insert a t := - insert_subset.2 ⟨mem_insert_self _ _, Subset.trans h (subset_insert _ _)⟩ + insert_subset_iff.2 ⟨mem_insert_self _ _, Subset.trans h (subset_insert _ _)⟩ #align finset.insert_subset_insert Finset.insert_subset_insert theorem insert_inj (ha : a ∉ s) : insert a s = insert b s ↔ a = b := @@ -1236,7 +1240,7 @@ theorem induction_on' {α : Type _} {p : Finset α → Prop} [DecidableEq α] (S (h₂ : ∀ {a s}, a ∈ S → s ⊆ S → a ∉ s → p s → p (insert a s)) : p S := @Finset.induction_on α (fun T => T ⊆ S → p T) _ S (fun _ => h₁) (fun _ _ has hqs hs => - let ⟨hS, sS⟩ := Finset.insert_subset.1 hs + let ⟨hS, sS⟩ := Finset.insert_subset_iff.1 hs h₂ hS sS has (hqs sS)) (Finset.Subset.refl S) #align finset.induction_on' Finset.induction_on' @@ -1545,7 +1549,7 @@ theorem _root_.Directed.exists_mem_subset_of_finset_subset_biUnion {α ι : Type obtain ⟨j, hbj⟩ : ∃ j, b ∈ f j := by simpa [Set.mem_iUnion₂] using hbtc (t.mem_insert_self b) rcases h j i with ⟨k, hk, hk'⟩ use k - rw [coe_insert, Set.insert_subset] + rw [coe_insert, Set.insert_subset_iff] exact ⟨hk hbj, _root_.trans hti hk'⟩ #align directed.exists_mem_subset_of_finset_subset_bUnion Directed.exists_mem_subset_of_finset_subset_biUnion diff --git a/Mathlib/Data/Finset/NAry.lean b/Mathlib/Data/Finset/NAry.lean index d4cb13446b2ad..e6a4eb5a0ac12 100644 --- a/Mathlib/Data/Finset/NAry.lean +++ b/Mathlib/Data/Finset/NAry.lean @@ -244,10 +244,10 @@ theorem subset_image₂ {s : Set α} {t : Set β} (hu : ↑u ⊆ image2 f s t) : haveI := Classical.decEq α haveI := Classical.decEq β refine' ⟨insert x s', insert y t', _⟩ - simp_rw [coe_insert, Set.insert_subset] + simp_rw [coe_insert, Set.insert_subset_iff] exact ⟨⟨hx, hs⟩, ⟨hy, hs'⟩, - insert_subset.2 + insert_subset_iff.2 ⟨mem_image₂.2 ⟨x, y, mem_insert_self _ _, mem_insert_self _ _, ha⟩, h.trans <| image₂_subset (subset_insert _ _) <| subset_insert _ _⟩⟩ #align finset.subset_image₂ Finset.subset_image₂ diff --git a/Mathlib/Data/Polynomial/Coeff.lean b/Mathlib/Data/Polynomial/Coeff.lean index b2048a435ca9b..a8956abadc27d 100644 --- a/Mathlib/Data/Polynomial/Coeff.lean +++ b/Mathlib/Data/Polynomial/Coeff.lean @@ -197,7 +197,7 @@ open Finset theorem support_binomial {k m : ℕ} (hkm : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) : support (C x * X ^ k + C y * X ^ m) = {k, m} := by apply subset_antisymm (support_binomial' k m x y) - simp_rw [insert_subset, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, + simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add, add_zero, Ne.def, hx, hy] #align polynomial.support_binomial Polynomial.support_binomial @@ -206,7 +206,7 @@ theorem support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hy : y ≠ 0) (hz : z ≠ 0) : support (C x * X ^ k + C y * X ^ m + C z * X ^ n) = {k, m, n} := by apply subset_antisymm (support_trinomial' k m n x y z) - simp_rw [insert_subset, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, + simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne, if_neg hmn.ne', if_neg (hkm.trans hmn).ne, if_neg (hkm.trans hmn).ne', mul_zero, add_zero, zero_add, Ne.def, hx, hy, hz] diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 6a38c2155c213..67d93cf93a5d2 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -1153,9 +1153,12 @@ theorem insert_ne_self : insert a s ≠ s ↔ a ∉ s := insert_eq_self.not #align set.insert_ne_self Set.insert_ne_self -theorem insert_subset : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by +theorem insert_subset_iff : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by simp only [subset_def, mem_insert_iff, or_imp, forall_and, forall_eq] -#align set.insert_subset Set.insert_subset +#align set.insert_subset Set.insert_subset_iff + +theorem insert_subset (ha : a ∈ t) (hs : s ⊆ t) : insert a s ⊆ t := + insert_subset_iff.mpr ⟨ha, hs⟩ theorem insert_subset_insert (h : s ⊆ t) : insert a s ⊆ insert a t := fun _ => Or.imp_right (@h _) #align set.insert_subset_insert Set.insert_subset_insert @@ -1171,7 +1174,7 @@ theorem subset_insert_iff_of_not_mem (ha : a ∉ s) : s ⊆ insert a t ↔ s ⊆ #align set.subset_insert_iff_of_not_mem Set.subset_insert_iff_of_not_mem theorem ssubset_iff_insert {s t : Set α} : s ⊂ t ↔ ∃ (a : α) (_ : a ∉ s), insert a s ⊆ t := by - simp only [insert_subset, exists_and_right, ssubset_def, not_subset] + simp only [insert_subset_iff, exists_and_right, ssubset_def, not_subset] simp only [exists_prop, and_comm] #align set.ssubset_iff_insert Set.ssubset_iff_insert @@ -1390,8 +1393,8 @@ theorem pair_comm (a b : α) : ({a, b} : Set α) = {b, a} := -- Porting note: first branch after `constructor` used to be by `tauto!`. theorem pair_eq_pair_iff {x y z w : α} : ({x, y} : Set α) = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z := by - simp only [Set.Subset.antisymm_iff, Set.insert_subset, Set.mem_insert_iff, Set.mem_singleton_iff, - Set.singleton_subset_iff] + simp only [Set.Subset.antisymm_iff, Set.insert_subset_iff, Set.mem_insert_iff, + Set.mem_singleton_iff, Set.singleton_subset_iff] constructor · rintro ⟨⟨rfl | rfl, rfl | rfl⟩, ⟨h₁, h₂⟩⟩ <;> simp [h₁, h₂] at * <;> simp [h₁, h₂] · rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> simp @@ -2474,7 +2477,7 @@ theorem nontrivial_of_pair_subset {x y} (hxy : x ≠ y) (h : {x, y} ⊆ s) : s.N theorem Nontrivial.pair_subset (hs : s.Nontrivial) : ∃ (x y : _) (_ : x ≠ y), {x, y} ⊆ s := let ⟨x, hx, y, hy, hxy⟩ := hs - ⟨x, y, hxy, insert_subset.2 ⟨hx, singleton_subset_iff.2 hy⟩⟩ + ⟨x, y, hxy, insert_subset_iff.2 ⟨hx, singleton_subset_iff.2 hy⟩⟩ #align set.nontrivial.pair_subset Set.Nontrivial.pair_subset theorem nontrivial_iff_pair_subset : s.Nontrivial ↔ ∃ (x y : _) (_ : x ≠ y), {x, y} ⊆ s := diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean index aea7664a78e24..c5c6b89e85fe1 100644 --- a/Mathlib/Data/Set/Finite.lean +++ b/Mathlib/Data/Set/Finite.lean @@ -1162,7 +1162,7 @@ theorem Finite.induction_on' {C : Set α → Prop} {S : Set α} (h : S.Finite) ( (H1 : ∀ {a s}, a ∈ S → s ⊆ S → a ∉ s → C s → C (insert a s)) : C S := by refine' @Set.Finite.induction_on α (fun s => s ⊆ S → C s) S h (fun _ => H0) _ Subset.rfl intro a s has _ hCs haS - rw [insert_subset] at haS + rw [insert_subset_iff] at haS exact H1 haS.1 haS.2 has (hCs haS.2) #align set.finite.induction_on' Set.Finite.induction_on' diff --git a/Mathlib/Data/Set/Intervals/Basic.lean b/Mathlib/Data/Set/Intervals/Basic.lean index f926c8c60b75c..75e07d3a43c80 100644 --- a/Mathlib/Data/Set/Intervals/Basic.lean +++ b/Mathlib/Data/Set/Intervals/Basic.lean @@ -829,7 +829,7 @@ theorem Icc_diff_Ioc_same (h : a ≤ b) : Icc a b \ Ioc a b = {a} := by @[simp] theorem Icc_diff_Ioo_same (h : a ≤ b) : Icc a b \ Ioo a b = {a, b} := by rw [← Icc_diff_both, diff_diff_cancel_left] - simp [insert_subset, h] + simp [insert_subset_iff, h] #align set.Icc_diff_Ioo_same Set.Icc_diff_Ioo_same @[simp] diff --git a/Mathlib/Data/Set/Intervals/OrdConnected.lean b/Mathlib/Data/Set/Intervals/OrdConnected.lean index 8f067160eb6ac..aab57501f323d 100644 --- a/Mathlib/Data/Set/Intervals/OrdConnected.lean +++ b/Mathlib/Data/Set/Intervals/OrdConnected.lean @@ -63,7 +63,7 @@ theorem ordConnected_of_Ioo {α : Type _} [PartialOrder α] {s : Set α} intro x hx y hy hxy rcases eq_or_lt_of_le hxy with (rfl | hxy'); · simpa rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy'] - exact insert_subset.2 ⟨hx, insert_subset.2 ⟨hy, hs x hx y hy hxy'⟩⟩ + exact insert_subset_iff.2 ⟨hx, insert_subset_iff.2 ⟨hy, hs x hx y hy hxy'⟩⟩ #align set.ord_connected_of_Ioo Set.ordConnected_of_Ioo theorem OrdConnected.preimage_mono {f : β → α} (hs : OrdConnected s) (hf : Monotone f) : diff --git a/Mathlib/Data/Set/List.lean b/Mathlib/Data/Set/List.lean index 89fb65f511ff8..b1cf7f9531138 100644 --- a/Mathlib/Data/Set/List.lean +++ b/Mathlib/Data/Set/List.lean @@ -48,7 +48,7 @@ theorem range_list_nthLe : (range fun k : Fin l.length => l.nthLe k k.2) = { x | theorem range_list_get? : range l.get? = insert none (some '' { x | x ∈ l }) := by rw [← range_list_nthLe, ← range_comp] - refine' (range_subset_iff.2 fun n => _).antisymm (insert_subset.2 ⟨_, _⟩) + refine' (range_subset_iff.2 fun n => _).antisymm (insert_subset_iff.2 ⟨_, _⟩) exacts [(le_or_lt l.length n).imp get?_eq_none.2 (fun hlt => ⟨⟨_, hlt⟩, (get?_eq_get hlt).symm⟩), ⟨_, get?_eq_none.2 le_rfl⟩, range_subset_iff.2 <| fun k => ⟨_, get?_eq_get _⟩] #align set.range_list_nth Set.range_list_get? diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean index 8045ea4e03979..518d56883dd69 100644 --- a/Mathlib/FieldTheory/Adjoin.lean +++ b/Mathlib/FieldTheory/Adjoin.lean @@ -397,7 +397,7 @@ theorem adjoin_insert_adjoin (x : E) : adjoin F (insert x (adjoin F S : Set E)) = adjoin F (insert x S) := le_antisymm (adjoin_le_iff.mpr - (Set.insert_subset.mpr + (Set.insert_subset_iff.mpr ⟨subset_adjoin _ _ (Set.mem_insert _ _), adjoin_le_iff.mpr (subset_adjoin_of_subset_right _ _ (Set.subset_insert _ _))⟩)) (adjoin.mono _ _ _ (Set.insert_subset_insert (subset_adjoin _ _))) diff --git a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean index 5c3440cd35dd2..0c99fdd49409a 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean @@ -113,7 +113,7 @@ theorem Cospherical.two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ : P} (h : Cospherical ({p₁, p₂, p₃, p₄} : Set P)) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₄ : p₂ ≠ p₄) (hp₃p₁ : p₃ ≠ p₁) (hp₃p₄ : p₃ ≠ p₄) : (2 : ℤ) • ∡ p₁ p₂ p₄ = (2 : ℤ) • ∡ p₁ p₃ p₄ := by obtain ⟨s, hs⟩ := cospherical_iff_exists_sphere.1 h - simp_rw [Set.insert_subset, Set.singleton_subset_iff, Sphere.mem_coe] at hs + simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff, Sphere.mem_coe] at hs exact Sphere.two_zsmul_oangle_eq hs.1 hs.2.1 hs.2.2.1 hs.2.2.2 hp₂p₁ hp₂p₄ hp₃p₁ hp₃p₄ #align euclidean_geometry.cospherical.two_zsmul_oangle_eq EuclideanGeometry.Cospherical.two_zsmul_oangle_eq @@ -374,7 +374,7 @@ theorem cospherical_of_two_zsmul_oangle_eq_of_not_collinear {p₁ p₂ p₃ p₄ let t₂ : Affine.Triangle ℝ P := ⟨![p₁, p₃, p₄], affineIndependent_iff_not_collinear_set.2 hn'⟩ rw [cospherical_iff_exists_sphere] refine' ⟨t₂.circumsphere, _⟩ - simp_rw [Set.insert_subset, Set.singleton_subset_iff] + simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff] refine' ⟨t₂.mem_circumsphere 0, _, t₂.mem_circumsphere 1, t₂.mem_circumsphere 2⟩ rw [Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq (by decide : (0 : Fin 3) ≠ 1) (by decide : (0 : Fin 3) ≠ 2) (by decide) @@ -404,7 +404,7 @@ theorem cospherical_or_collinear_of_two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ : P let t : Affine.Triangle ℝ P := ⟨![p₂, p₃, p₄], affineIndependent_iff_not_collinear_set.2 hl⟩ rw [cospherical_iff_exists_sphere] refine' ⟨t.circumsphere, _⟩ - simp_rw [Set.insert_subset, Set.singleton_subset_iff] + simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff] exact ⟨t.mem_circumsphere 0, t.mem_circumsphere 1, t.mem_circumsphere 2⟩ have hc' : Collinear ℝ ({p₁, p₃, p₄} : Set P) := by rwa [← collinear_iff_of_two_zsmul_oangle_eq h] diff --git a/Mathlib/Geometry/Euclidean/Sphere/Basic.lean b/Mathlib/Geometry/Euclidean/Sphere/Basic.lean index 7a7f93113bf02..1b5146f409cf0 100644 --- a/Mathlib/Geometry/Euclidean/Sphere/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Sphere/Basic.lean @@ -281,7 +281,7 @@ theorem Cospherical.affineIndependent_of_mem_of_ne {s : Set P} (hs : Cospherical (h₁ : p₁ ∈ s) (h₂ : p₂ ∈ s) (h₃ : p₃ ∈ s) (h₁₂ : p₁ ≠ p₂) (h₁₃ : p₁ ≠ p₃) (h₂₃ : p₂ ≠ p₃) : AffineIndependent ℝ ![p₁, p₂, p₃] := by refine' hs.affineIndependent _ _ - · simp [h₁, h₂, h₃, Set.insert_subset] + · simp [h₁, h₂, h₃, Set.insert_subset_iff] · erw [Fin.cons_injective_iff, Fin.cons_injective_iff] simp [h₁₂, h₁₃, h₂₃, Function.Injective] #align euclidean_geometry.cospherical.affine_independent_of_mem_of_ne EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean index 8131a54110964..e8d8b12923b4f 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean @@ -1672,7 +1672,7 @@ theorem closure_cycle_coprime_swap {n : ℕ} {σ : Perm α} (h0 : Nat.coprime n have h1' : IsCycle ((σ ^ n) ^ (m : ℤ)) := by rwa [← hm] at h1 replace h1' : IsCycle (σ ^ n) := h1'.of_pow (le_trans (support_pow_le σ n) (ge_of_eq (congr_arg support hm))) - rw [eq_top_iff, ← closure_cycle_adjacent_swap h1' h2' x, closure_le, Set.insert_subset] + rw [eq_top_iff, ← closure_cycle_adjacent_swap h1' h2' x, closure_le, Set.insert_subset_iff] exact ⟨Subgroup.pow_mem (closure _) (subset_closure (Set.mem_insert σ _)) n, Set.singleton_subset_iff.mpr (subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _)))⟩ diff --git a/Mathlib/GroupTheory/Perm/Cycle/Type.lean b/Mathlib/GroupTheory/Perm/Cycle/Type.lean index 143cba514ff90..79f478b4f4ee1 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Type.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Type.lean @@ -507,7 +507,7 @@ theorem subgroup_eq_top_of_swap_mem [DecidableEq α] {H : Subgroup (Perm α)} have hσ3 : (σ : Perm α).support = ⊤ := Finset.eq_univ_of_card (σ : Perm α).support (hσ2.orderOf.symm.trans hσ1) have hσ4 : Subgroup.closure {↑σ, τ} = ⊤ := closure_prime_cycle_swap h0 hσ2 hσ3 h3 - rw [eq_top_iff, ← hσ4, Subgroup.closure_le, Set.insert_subset, Set.singleton_subset_iff] + rw [eq_top_iff, ← hσ4, Subgroup.closure_le, Set.insert_subset_iff, Set.singleton_subset_iff] exact ⟨Subtype.mem σ, h2⟩ #align equiv.perm.subgroup_eq_top_of_swap_mem Equiv.Perm.subgroup_eq_top_of_swap_mem diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean index 5e53c276c2b93..9860a5f40c6ff 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean @@ -1352,7 +1352,7 @@ theorem vadd_right_mem_affineSpan_pair {p₁ p₂ : P} {v : V} : /-- The span of two points that lie in an affine subspace is contained in that subspace. -/ theorem affineSpan_pair_le_of_mem_of_mem {p₁ p₂ : P} {s : AffineSubspace k P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) : line[k, p₁, p₂] ≤ s := by - rw [affineSpan_le, Set.insert_subset, Set.singleton_subset_iff] + rw [affineSpan_le, Set.insert_subset_iff, Set.singleton_subset_iff] exact ⟨hp₁, hp₂⟩ #align affine_span_pair_le_of_mem_of_mem affineSpan_pair_le_of_mem_of_mem diff --git a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean index 3d83a73f3b946..b829c352ff011 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean @@ -529,7 +529,7 @@ theorem Collinear.mem_affineSpan_of_mem_of_ne {s : Set P} (h : Collinear k s) {p span of the whole set. -/ theorem Collinear.affineSpan_eq_of_ne {s : Set P} (h : Collinear k s) {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₁p₂ : p₁ ≠ p₂) : line[k, p₁, p₂] = affineSpan k s := - le_antisymm (affineSpan_mono _ (Set.insert_subset.2 ⟨hp₁, Set.singleton_subset_iff.2 hp₂⟩)) + le_antisymm (affineSpan_mono _ (Set.insert_subset_iff.2 ⟨hp₁, Set.singleton_subset_iff.2 hp₂⟩)) (affineSpan_le.2 fun _ hp => h.mem_affineSpan_of_mem_of_ne hp₁ hp₂ hp hp₁p₂) #align collinear.affine_span_eq_of_ne Collinear.affineSpan_eq_of_ne diff --git a/Mathlib/LinearAlgebra/Lagrange.lean b/Mathlib/LinearAlgebra/Lagrange.lean index 4860353696034..31eadc60331b8 100644 --- a/Mathlib/LinearAlgebra/Lagrange.lean +++ b/Mathlib/LinearAlgebra/Lagrange.lean @@ -432,13 +432,13 @@ theorem interpolate_eq_sum_interpolate_insert_sdiff (hvt : Set.InjOn v t) (hs : rw [degree_basis (Set.InjOn.mono hst hvt) hi, H, WithBot.coe_add, Nat.cast_withBot, WithBot.add_lt_add_iff_right (@WithBot.coe_ne_bot _ (s.card - 1))] convert degree_interpolate_lt _ - (hvt.mono (coe_subset.mpr (insert_subset.mpr ⟨hst hi, sdiff_subset _ _⟩))) + (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hst hi, sdiff_subset _ _⟩))) rw [card_insert_of_not_mem (not_mem_sdiff_of_mem_right hi), card_sdiff hst, add_comm] · simp_rw [eval_finset_sum, eval_mul] by_cases hi' : i ∈ s · rw [← add_sum_erase _ _ hi', eval_basis_self (hvt.mono hst) hi', eval_interpolate_at_node _ - (hvt.mono (coe_subset.mpr (insert_subset.mpr ⟨hi, sdiff_subset _ _⟩))) + (hvt.mono (coe_subset.mpr (insert_subset_iff.mpr ⟨hi, sdiff_subset _ _⟩))) (mem_insert_self _ _), mul_one, add_right_eq_self] refine' sum_eq_zero fun j hj => _ @@ -450,7 +450,7 @@ theorem interpolate_eq_sum_interpolate_insert_sdiff (hvt : Set.InjOn v t) (hs : refine' sum_congr rfl fun j hj => _ congr exact - eval_interpolate_at_node _ (hvt.mono (insert_subset.mpr ⟨hst hj, sdiff_subset _ _⟩)) + eval_interpolate_at_node _ (hvt.mono (insert_subset_iff.mpr ⟨hst hj, sdiff_subset _ _⟩)) (mem_insert.mpr (Or.inr (mem_sdiff.mpr ⟨hi, hi'⟩))) #align lagrange.interpolate_eq_sum_interpolate_insert_sdiff Lagrange.interpolate_eq_sum_interpolate_insert_sdiff @@ -465,7 +465,7 @@ theorem interpolate_eq_add_interpolate_erase (hvs : Set.InjOn v s) (hi : i ∈ s sdiff_singleton_eq_erase, pair_comm, sdiff_insert_insert_of_mem_of_not_mem hj (not_mem_singleton.mpr hij.symm), sdiff_singleton_eq_erase] - · exact insert_subset.mpr ⟨hi, singleton_subset_iff.mpr hj⟩ + · exact insert_subset_iff.mpr ⟨hi, singleton_subset_iff.mpr hj⟩ #align lagrange.interpolate_eq_add_interpolate_erase Lagrange.interpolate_eq_add_interpolate_erase end Interpolate diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean index 7fd367b45ac9f..77d1ea9d2d43a 100644 --- a/Mathlib/LinearAlgebra/LinearIndependent.lean +++ b/Mathlib/LinearAlgebra/LinearIndependent.lean @@ -1285,7 +1285,7 @@ theorem exists_linearIndependent_extension (hs : LinearIndependent K ((↑) : s · refine' ⟨b, bt, sb, fun x xt => _, bi⟩ by_contra hn apply hn - rw [← h _ ⟨insert_subset.2 ⟨xt, bt⟩, bi.insert hn⟩ (subset_insert _ _)] + rw [← h _ ⟨insert_subset_iff.2 ⟨xt, bt⟩, bi.insert hn⟩ (subset_insert _ _)] exact subset_span (mem_insert _ _) #align exists_linear_independent_extension exists_linearIndependent_extension @@ -1383,7 +1383,7 @@ theorem exists_of_linearIndependent_of_finite_span {t : Finset V} have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) := by exact mem_span_insert_exchange (this hb₂s) hb₂t rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃ - let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset, hb₂s, hs']) hst this + let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset_iff, hb₂s, hs']) hst this -- Porting note: `hb₂t'` → `Finset.card_insert_of_not_mem hb₂t'` ⟨u, Subset.trans hust <| union_subset_union (Subset.refl _) (by simp [subset_insert]), hsu, by simp [eq, Finset.card_insert_of_not_mem hb₂t', hb₁t, hb₁s']⟩ diff --git a/Mathlib/LinearAlgebra/Span.lean b/Mathlib/LinearAlgebra/Span.lean index 703bcffe5edd9..6dea36914cf5a 100644 --- a/Mathlib/LinearAlgebra/Span.lean +++ b/Mathlib/LinearAlgebra/Span.lean @@ -117,7 +117,7 @@ alias Submodule.map_span_le ← _root_.LinearMap.map_span_le @[simp] theorem span_insert_zero : span R (insert (0 : M) s) = span R s := by refine' le_antisymm _ (Submodule.span_mono (Set.subset_insert 0 s)) - rw [span_le, Set.insert_subset] + rw [span_le, Set.insert_subset_iff] exact ⟨by simp only [SetLike.mem_coe, Submodule.zero_mem], Submodule.subset_span⟩ #align submodule.span_insert_zero Submodule.span_insert_zero @@ -492,7 +492,7 @@ theorem span_insert (x) (s : Set M) : span R (insert x s) = span R ({x} : Set M) #align submodule.span_insert Submodule.span_insert theorem span_insert_eq_span (h : x ∈ span R s) : span R (insert x s) = span R s := - span_eq_of_le _ (Set.insert_subset.mpr ⟨h, subset_span⟩) (span_mono <| subset_insert _ _) + span_eq_of_le _ (Set.insert_subset_iff.mpr ⟨h, subset_span⟩) (span_mono <| subset_insert _ _) #align submodule.span_insert_eq_span Submodule.span_insert_eq_span theorem span_span : span R (span R s : Set M) = span R s := diff --git a/Mathlib/MeasureTheory/Covering/Vitali.lean b/Mathlib/MeasureTheory/Covering/Vitali.lean index 311c74a971d6f..8e5e82bd76ca5 100644 --- a/Mathlib/MeasureTheory/Covering/Vitali.lean +++ b/Mathlib/MeasureTheory/Covering/Vitali.lean @@ -128,7 +128,7 @@ theorem exists_disjoint_subfamily_covering_enlargment (B : ι → Set α) (t : S -- we claim that `u ∪ {a'}` still belongs to `T`, contradicting the maximality of `u`. refine' ⟨insert a' u, ⟨_, _, _⟩, subset_insert _ _, (ne_insert_of_not_mem _ a'_ne_u).symm⟩ · -- check that `u ∪ {a'}` is made of elements of `t`. - rw [insert_subset] + rw [insert_subset_iff] exact ⟨a'A.1, uT.1⟩ · -- Check that `u ∪ {a'}` is a disjoint family. This follows from the fact that `a'` does not -- intersect `u`. diff --git a/Mathlib/ModelTheory/Types.lean b/Mathlib/ModelTheory/Types.lean index f8a8404dc16d7..738cb38d3841e 100644 --- a/Mathlib/ModelTheory/Types.lean +++ b/Mathlib/ModelTheory/Types.lean @@ -104,7 +104,7 @@ theorem not_mem_iff (p : T.CompleteType α) (φ : L[[α]].Sentence) : φ.not ∈ simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h exact h.2 h.1 refine' h (p.isMaximal.1.mono _) - rw [insert_subset, singleton_subset_iff] + rw [insert_subset_iff, singleton_subset_iff] exact ⟨ht, hf⟩, (p.mem_or_not_mem φ).resolve_left⟩ #align first_order.language.Theory.complete_type.not_mem_iff FirstOrder.Language.Theory.CompleteType.not_mem_iff diff --git a/Mathlib/Order/CompactlyGenerated.lean b/Mathlib/Order/CompactlyGenerated.lean index bd2d4aea5e8b6..0a4d9cf22117e 100644 --- a/Mathlib/Order/CompactlyGenerated.lean +++ b/Mathlib/Order/CompactlyGenerated.lean @@ -207,7 +207,7 @@ theorem WellFounded.isSupFiniteCompact (h : WellFounded ((· > ·) : α → α refine' ⟨t, ht₁, (sSup_le _ _ fun y hy => _).antisymm _⟩ · classical rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y)) - (hm _ ⟨insert y t, by simp [Set.insert_subset, hy, ht₁]⟩)] + (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)] simp · rw [Finset.sup_id_eq_sSup] exact sSup_le_sSup ht₁ @@ -436,7 +436,7 @@ theorem CompleteLattice.setIndependent_iff_finite {s : Set α} : have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot · rwa [Finset.coe_insert, Set.insert_diff_self_of_not_mem] at h' exact fun con => ((Set.mem_diff a).1 (ht con)).2 (Set.mem_singleton a) - · rw [Finset.coe_insert, Set.insert_subset] + · rw [Finset.coe_insert, Set.insert_subset_iff] exact ⟨ha, Set.Subset.trans ht (Set.diff_subset _ _)⟩⟩ #align complete_lattice.set_independent_iff_finite CompleteLattice.setIndependent_iff_finite diff --git a/Mathlib/Order/Cover.lean b/Mathlib/Order/Cover.lean index dc268221a3902..1d743048fe6c8 100644 --- a/Mathlib/Order/Cover.lean +++ b/Mathlib/Order/Cover.lean @@ -473,7 +473,7 @@ namespace Set theorem wcovby_insert (x : α) (s : Set α) : s ⩿ insert x s := by refine' wcovby_of_eq_or_eq (subset_insert x s) fun t hst h2t => _ by_cases h : x ∈ t - · exact Or.inr (subset_antisymm h2t <| insert_subset.mpr ⟨h, hst⟩) + · exact Or.inr (subset_antisymm h2t <| insert_subset_iff.mpr ⟨h, hst⟩) · refine' Or.inl (subset_antisymm _ hst) rwa [← diff_singleton_eq_self h, diff_singleton_subset_iff] #align set.wcovby_insert Set.wcovby_insert diff --git a/Mathlib/Order/Filter/CountableInter.lean b/Mathlib/Order/Filter/CountableInter.lean index 8d7d04507aca5..8b71fbbeda1e0 100644 --- a/Mathlib/Order/Filter/CountableInter.lean +++ b/Mathlib/Order/Filter/CountableInter.lean @@ -136,7 +136,7 @@ def Filter.ofCountableInter (l : Set (Set α)) univ_sets := @sInter_empty α ▸ hp _ countable_empty (empty_subset _) sets_of_superset := h_mono _ _ inter_sets {s t} hs ht := sInter_pair s t ▸ - hp _ ((countable_singleton _).insert _) (insert_subset.2 ⟨hs, singleton_subset_iff.2 ht⟩) + hp _ ((countable_singleton _).insert _) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩) #align filter.of_countable_Inter Filter.ofCountableInter instance Filter.countable_Inter_ofCountableInter (l : Set (Set α)) diff --git a/Mathlib/Order/SupIndep.lean b/Mathlib/Order/SupIndep.lean index e9e67246e3855..2f2fbeec3e187 100644 --- a/Mathlib/Order/SupIndep.lean +++ b/Mathlib/Order/SupIndep.lean @@ -325,7 +325,7 @@ theorem setIndependent_pair {a b : α} (hab : a ≠ b) : subset of the rest. -/ theorem SetIndependent.disjoint_sSup {x : α} {y : Set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) : Disjoint x (sSup y) := by - have := (hs.mono <| insert_subset.mpr ⟨hx, hy⟩) (mem_insert x _) + have := (hs.mono <| insert_subset_iff.mpr ⟨hx, hy⟩) (mem_insert x _) rw [insert_diff_of_mem _ (mem_singleton _), diff_singleton_eq_self hxy] at this exact this #align complete_lattice.set_independent.disjoint_Sup CompleteLattice.SetIndependent.disjoint_sSup diff --git a/Mathlib/RingTheory/Adjoin/Basic.lean b/Mathlib/RingTheory/Adjoin/Basic.lean index 9b830d327d6bd..8380fd0480330 100644 --- a/Mathlib/RingTheory/Adjoin/Basic.lean +++ b/Mathlib/RingTheory/Adjoin/Basic.lean @@ -226,7 +226,7 @@ theorem adjoin_image (f : A →ₐ[R] B) (s : Set A) : adjoin R (f '' s) = (adjo theorem adjoin_insert_adjoin (x : A) : adjoin R (insert x ↑(adjoin R s)) = adjoin R (insert x s) := le_antisymm (adjoin_le - (Set.insert_subset.mpr + (Set.insert_subset_iff.mpr ⟨subset_adjoin (Set.mem_insert _ _), adjoin_mono (Set.subset_insert _ _)⟩)) (Algebra.adjoin_mono (Set.insert_subset_insert Algebra.subset_adjoin)) #align algebra.adjoin_insert_adjoin Algebra.adjoin_insert_adjoin @@ -255,7 +255,7 @@ theorem adjoin_inl_union_inr_eq_prod (s) (t) : (adjoin R s).prod (adjoin R t) := by apply le_antisymm · - simp only [adjoin_le_iff, Set.insert_subset, Subalgebra.zero_mem, Subalgebra.one_mem, + simp only [adjoin_le_iff, Set.insert_subset_iff, Subalgebra.zero_mem, Subalgebra.one_mem, subset_adjoin,-- the rest comes from `squeeze_simp` Set.union_subset_iff, LinearMap.coe_inl, Set.mk_preimage_prod_right, Set.image_subset_iff, SetLike.mem_coe, diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean index 50bd841242f5b..d77e60e821fe4 100644 --- a/Mathlib/RingTheory/Finiteness.lean +++ b/Mathlib/RingTheory/Finiteness.lean @@ -107,7 +107,7 @@ theorem exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type _} [CommR apply ih rcases H with ⟨r, hr1, hrn, hs⟩ rw [← Set.singleton_union, span_union, smul_sup] at hrn - rw [Set.insert_subset] at hs + rw [Set.insert_subset_iff] at hs have : ∃ c : R, c - 1 ∈ I ∧ c • i ∈ I • span R s := by specialize hrn hs.1 rw [mem_comap, mem_sup] at hrn diff --git a/Mathlib/RingTheory/IntegralClosure.lean b/Mathlib/RingTheory/IntegralClosure.lean index 7c5ee4514f3f7..578093a8951d7 100644 --- a/Mathlib/RingTheory/IntegralClosure.lean +++ b/Mathlib/RingTheory/IntegralClosure.lean @@ -321,7 +321,8 @@ theorem isIntegral_of_mem_of_FG (S : Subalgebra R A) (HS : S.toSubmodule.FG) (x constructor <;> intro hz · exact (span_le.2 - (Set.insert_subset.2 ⟨(Algebra.adjoin S₀ (y : Set A)).one_mem, Algebra.subset_adjoin⟩)) hz + (Set.insert_subset_iff.2 + ⟨(Algebra.adjoin S₀ (y : Set A)).one_mem, Algebra.subset_adjoin⟩)) hz · rw [Subalgebra.mem_toSubmodule, Algebra.mem_adjoin_iff] at hz suffices Subring.closure (Set.range (algebraMap (↥S₀) A) ∪ ↑y) ≤ S₁ by exact this hz refine' Subring.closure_le.2 (Set.union_subset _ fun t ht => subset_span <| Or.inr ht) @@ -719,7 +720,8 @@ theorem normalizeScaleRoots_coeff_mul_leadingCoeff_pow (i : ℕ) (hp : 1 ≤ nat apply Nat.le_pred_of_lt rw [lt_iff_le_and_ne] exact ⟨le_natDegree_of_ne_zero h₁, h₂⟩ -#align normalize_scale_roots_coeff_mul_leading_coeff_pow normalizeScaleRoots_coeff_mul_leadingCoeff_pow +#align normalize_scale_roots_coeff_mul_leading_coeff_pow + normalizeScaleRoots_coeff_mul_leadingCoeff_pow theorem leadingCoeff_smul_normalizeScaleRoots (p : R[X]) : p.leadingCoeff • normalizeScaleRoots p = scaleRoots p p.leadingCoeff := by @@ -1063,7 +1065,8 @@ theorem RingHom.isIntegralElem_of_isIntegralElem_comp {x : T} (h : (g.comp f).Is g.IsIntegralElem x := let ⟨p, ⟨hp, hp'⟩⟩ := h ⟨p.map f, hp.map f, by rwa [← eval₂_map] at hp'⟩ -#align ring_hom.is_integral_elem_of_is_integral_elem_comp RingHom.isIntegralElem_of_isIntegralElem_comp +#align ring_hom.is_integral_elem_of_is_integral_elem_comp + RingHom.isIntegralElem_of_isIntegralElem_comp theorem RingHom.isIntegral_tower_top_of_isIntegral (h : (g.comp f).IsIntegral) : g.IsIntegral := fun x => RingHom.isIntegralElem_of_isIntegralElem_comp f g (h x) diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean index c2e2ff6947d09..ca672003fcba3 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean @@ -94,7 +94,7 @@ private theorem isRoot_cyclotomic_iff' {n : ℕ} {K : Type _} [Field K] {μ : K} have key : i < n := (Nat.le_of_dvd ho hio).trans_lt ((Nat.le_of_dvd hnpos hμn).lt_of_ne hnμ) have key' : i ∣ n := hio.trans hμn rw [← Polynomial.dvd_iff_isRoot] at hμ hiμ - have hni : {i, n} ⊆ n.divisors := by simpa [Finset.insert_subset, key'] using hnpos.ne' + have hni : {i, n} ⊆ n.divisors := by simpa [Finset.insert_subset_iff, key'] using hnpos.ne' obtain ⟨k, hk⟩ := hiμ obtain ⟨j, hj⟩ := hμ have := prod_cyclotomic_eq_X_pow_sub_one hnpos K diff --git a/Mathlib/SetTheory/Ordinal/Topology.lean b/Mathlib/SetTheory/Ordinal/Topology.lean index 5020b96d2e9bb..0ca4d245a26ec 100644 --- a/Mathlib/SetTheory/Ordinal/Topology.lean +++ b/Mathlib/SetTheory/Ordinal/Topology.lean @@ -81,7 +81,7 @@ theorem isOpen_iff : IsOpen s ↔ ∀ o ∈ s, IsLimit o → ∃ a < o, Set.Ioo by_cases ho' : IsLimit o · simp only [(nhdsBasis_Ioc ho'.1).mem_iff, ho', true_implies] refine exists_congr fun a => and_congr_right fun ha => ?_ - simp only [← Set.Ioo_insert_right ha, Set.insert_subset, ho, true_and] + simp only [← Set.Ioo_insert_right ha, Set.insert_subset_iff, ho, true_and] · simp [nhds_eq_pure.2 ho', ho, ho'] #align ordinal.is_open_iff Ordinal.isOpen_iff diff --git a/Mathlib/Topology/Algebra/Order/Compact.lean b/Mathlib/Topology/Algebra/Order/Compact.lean index a9979053f84f6..435aafd46b63e 100644 --- a/Mathlib/Topology/Algebra/Order/Compact.lean +++ b/Mathlib/Topology/Algebra/Order/Compact.lean @@ -227,7 +227,7 @@ theorem ContinuousOn.exists_isMinOn' {s : Set β} {f : β → α} (hf : Continuo (hsc : IsClosed s) {x₀ : β} (h₀ : x₀ ∈ s) (hc : ∀ᶠ x in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x) : ∃ x ∈ s, IsMinOn f s x := by rcases (hasBasis_cocompact.inf_principal _).eventually_iff.1 hc with ⟨K, hK, hKf⟩ - have hsub : insert x₀ (K ∩ s) ⊆ s := insert_subset.2 ⟨h₀, inter_subset_right _ _⟩ + have hsub : insert x₀ (K ∩ s) ⊆ s := insert_subset_iff.2 ⟨h₀, inter_subset_right _ _⟩ obtain ⟨x, hx, hxf⟩ : ∃ x ∈ insert x₀ (K ∩ s), ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y := ((hK.inter_right hsc).insert x₀).exists_forall_le (insert_nonempty _ _) (hf.mono hsub) refine' ⟨x, hsub hx, fun y hy => _⟩ diff --git a/Mathlib/Topology/Connected.lean b/Mathlib/Topology/Connected.lean index 2ee4a71856d73..388c418e625fa 100644 --- a/Mathlib/Topology/Connected.lean +++ b/Mathlib/Topology/Connected.lean @@ -186,7 +186,8 @@ theorem IsPreconnected.biUnion_of_reflTransGen {ι : Type _} {t : Set ι} {s : exact H i hi case tail j k _ hjk ih => obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2 - refine ⟨insert k p, insert_subset.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip, mem_insert k p, ?_⟩ + refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip, + mem_insert k p, ?_⟩ rw [biUnion_insert] refine (H k hj).union' (hjk.1.mono ?_) hp rw [inter_comm] @@ -720,7 +721,8 @@ theorem Continuous.mapsTo_connectedComponent [TopologicalSpace β] {f : α → theorem irreducibleComponent_subset_connectedComponent {x : α} : irreducibleComponent x ⊆ connectedComponent x := isIrreducible_irreducibleComponent.isConnected.subset_connectedComponent mem_irreducibleComponent -#align irreducible_component_subset_connected_component irreducibleComponent_subset_connectedComponent +#align irreducible_component_subset_connected_component + irreducibleComponent_subset_connectedComponent @[mono] theorem connectedComponentIn_mono (x : α) {F G : Set α} (h : F ⊆ G) : @@ -984,7 +986,8 @@ theorem isPreconnected_iff_subset_of_fully_disjoint_closed {s : Set α} (hs : Is · rw [← inter_distrib_right] exact subset_inter hss Subset.rfl · rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm] -#align is_preconnected_iff_subset_of_fully_disjoint_closed isPreconnected_iff_subset_of_fully_disjoint_closed +#align is_preconnected_iff_subset_of_fully_disjoint_closed + isPreconnected_iff_subset_of_fully_disjoint_closed theorem IsClopen.connectedComponent_subset {x} (hs : IsClopen s) (hx : x ∈ s) : connectedComponent x ⊆ s := @@ -1115,7 +1118,8 @@ theorem locallyConnectedSpace_iff_open_connected_basis : LocallyConnectedSpace α ↔ ∀ x, (𝓝 x).HasBasis (fun s : Set α => IsOpen s ∧ x ∈ s ∧ IsConnected s) id := ⟨@LocallyConnectedSpace.open_connected_basis _ _, LocallyConnectedSpace.mk⟩ -#align locally_connected_space_iff_open_connected_basis locallyConnectedSpace_iff_open_connected_basis +#align locally_connected_space_iff_open_connected_basis + locallyConnectedSpace_iff_open_connected_basis theorem locallyConnectedSpace_iff_open_connected_subsets : LocallyConnectedSpace α ↔ @@ -1129,7 +1133,8 @@ theorem locallyConnectedSpace_iff_open_connected_subsets : · exact fun h => ⟨fun U => ⟨fun hU => let ⟨V, hVU, hV⟩ := h U hU ⟨V, hV, hVU⟩, fun ⟨V, ⟨hV, hxV, _⟩, hVU⟩ => mem_nhds_iff.mpr ⟨V, hVU, hV, hxV⟩⟩⟩ -#align locally_connected_space_iff_open_connected_subsets locallyConnectedSpace_iff_open_connected_subsets +#align locally_connected_space_iff_open_connected_subsets + locallyConnectedSpace_iff_open_connected_subsets /-- A space with discrete topology is a locally connected space. -/ instance (priority := 100) DiscreteTopology.toLocallyConnectedSpace (α) [TopologicalSpace α] @@ -1178,7 +1183,8 @@ theorem locallyConnectedSpace_iff_connectedComponentIn_open : (connectedComponentIn_subset _ _).trans interior_subset, h _ isOpen_interior x _, mem_connectedComponentIn _, isConnected_connectedComponentIn_iff.mpr _⟩ <;> exact mem_interior_iff_mem_nhds.mpr hU -#align locally_connected_space_iff_connected_component_in_open locallyConnectedSpace_iff_connectedComponentIn_open +#align locally_connected_space_iff_connected_component_in_open + locallyConnectedSpace_iff_connectedComponentIn_open theorem locallyConnectedSpace_iff_connected_subsets : LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U := by @@ -1304,7 +1310,8 @@ theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton : rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩) · exact subsingleton_empty · exact (h x).anti (hs.subset_connectedComponent x_in) -#align totally_disconnected_space_iff_connected_component_subsingleton totallyDisconnectedSpace_iff_connectedComponent_subsingleton +#align totally_disconnected_space_iff_connected_component_subsingleton + totallyDisconnectedSpace_iff_connectedComponent_subsingleton /-- A space is totally disconnected iff its connected components are singletons. -/ theorem totallyDisconnectedSpace_iff_connectedComponent_singleton : @@ -1313,7 +1320,8 @@ theorem totallyDisconnectedSpace_iff_connectedComponent_singleton : refine forall_congr' fun x => ?_ rw [subsingleton_iff_singleton] exact mem_connectedComponent -#align totally_disconnected_space_iff_connected_component_singleton totallyDisconnectedSpace_iff_connectedComponent_singleton +#align totally_disconnected_space_iff_connected_component_singleton + totallyDisconnectedSpace_iff_connectedComponent_singleton @[simp] theorem connectedComponent_eq_singleton [TotallyDisconnectedSpace α] (x : α) : connectedComponent x = {x} := @@ -1327,12 +1335,14 @@ theorem Continuous.image_connectedComponent_eq_singleton {β : Type _} [Topologi f '' connectedComponent a = {f a} := (Set.subsingleton_iff_singleton <| mem_image_of_mem f mem_connectedComponent).mp (isPreconnected_connectedComponent.image f h.continuousOn).subsingleton -#align continuous.image_connected_component_eq_singleton Continuous.image_connectedComponent_eq_singleton +#align continuous.image_connected_component_eq_singleton + Continuous.image_connectedComponent_eq_singleton theorem isTotallyDisconnected_of_totallyDisconnectedSpace [TotallyDisconnectedSpace α] (s : Set α) : IsTotallyDisconnected s := fun t _ ht => TotallyDisconnectedSpace.isTotallyDisconnected_univ _ t.subset_univ ht -#align is_totally_disconnected_of_totally_disconnected_space isTotallyDisconnected_of_totallyDisconnectedSpace +#align is_totally_disconnected_of_totally_disconnected_space + isTotallyDisconnected_of_totallyDisconnectedSpace theorem isTotallyDisconnected_of_image [TopologicalSpace β] {f : α → β} (hf : ContinuousOn f s) (hf' : Injective f) (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s := @@ -1398,7 +1408,8 @@ class TotallySeparatedSpace (α : Type u) [TopologicalSpace α] : Prop where instance (priority := 100) TotallySeparatedSpace.totallyDisconnectedSpace (α : Type u) [TopologicalSpace α] [TotallySeparatedSpace α] : TotallyDisconnectedSpace α := ⟨TotallySeparatedSpace.isTotallySeparated_univ.isTotallyDisconnected⟩ -#align totally_separated_space.totally_disconnected_space TotallySeparatedSpace.totallyDisconnectedSpace +#align totally_separated_space.totally_disconnected_space + TotallySeparatedSpace.totallyDisconnectedSpace -- see Note [lower instance priority] instance (priority := 100) TotallySeparatedSpace.of_discrete (α : Type _) [TopologicalSpace α] diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean index c61ea286e1f1c..d07aba3a871e0 100644 --- a/Mathlib/Topology/Order/Basic.lean +++ b/Mathlib/Topology/Order/Basic.lean @@ -2206,7 +2206,7 @@ theorem closure_Ioo {a b : α} (hab : a ≠ b) : closure (Ioo a b) = Icc a b := · cases' hab.lt_or_lt with hab hab · rw [← diff_subset_closure_iff, Icc_diff_Ioo_same hab.le] have hab' : (Ioo a b).Nonempty := nonempty_Ioo.2 hab - simp only [insert_subset, singleton_subset_iff] + simp only [insert_subset_iff, singleton_subset_iff] exact ⟨(isGLB_Ioo hab).mem_closure hab', (isLUB_Ioo hab).mem_closure hab'⟩ · rw [Icc_eq_empty_of_lt hab] exact empty_subset _