bump to nightly-2023-06-28-03

mathlib commit leanprover-community/mathlib@8b98191

Archive/Imo/Imo2019Q2.lean

@@ -458,7 +458,7 @@ theorem not_collinear_QPA₂ : ¬Collinear ℝ ({cfg.q, cfg.P, cfg.a₂} : Set P
   have h : cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) :=
     by
     refine' cfg.triangle_ABC.circumsphere.cospherical.subset _
-    simp [Set.insert_subset, cfg.A_mem_circumsphere, cfg.B_mem_circumsphere,
+    simp [Set.insert_subset_iff, cfg.A_mem_circumsphere, cfg.B_mem_circumsphere,
       cfg.A₂_mem_circumsphere]
   exact h.affine_independent_of_ne cfg.A_ne_B.symm cfg.A₂_ne_B.symm cfg.A₂_ne_A.symm
 #align imo2019_q2.imo2019q2_cfg.not_collinear_QPA₂ Imo2019Q2.Imo2019q2Cfg.not_collinear_QPA₂
@@ -656,7 +656,7 @@ theorem result : Concyclic ({cfg.P, cfg.q, cfg.p₁, cfg.q₁} : Set Pt) :=
   refine' ⟨_, coplanar_of_fact_finrank_eq_two _⟩
   rw [cospherical_iff_exists_sphere]
   refine' ⟨cfg.ω, _⟩
-  simp only [Set.insert_subset, Set.singleton_subset_iff]
+  simp only [Set.insert_subset_iff, Set.singleton_subset_iff]
   exact ⟨cfg.P_mem_ω, cfg.Q_mem_ω, cfg.P₁_mem_ω, cfg.Q₁_mem_ω⟩
 #align imo2019_q2.imo2019q2_cfg.result Imo2019Q2.Imo2019q2Cfg.result
 

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -154,7 +154,7 @@ theorem real_roots_Phi_ge (hab : b < a) : 2 ≤ Fintype.card ((Φ ℚ a b).rootS
   have q_ne_zero : Φ ℚ a b ≠ 0 := (monic_Phi a b).NeZero
   obtain ⟨x, y, hxy, hx, hy⟩ := real_roots_Phi_ge_aux a b hab
   have key : ↑({x, y} : Finset ℝ) ⊆ (Φ ℚ a b).rootSet ℝ := by
-    simp [Set.insert_subset, mem_root_set_of_ne q_ne_zero, hx, hy]
+    simp [Set.insert_subset_iff, mem_root_set_of_ne q_ne_zero, hx, hy]
   convert Fintype.card_le_of_embedding (Set.embeddingOfSubset _ _ key)
   simp only [Finset.coe_sort_coe, Fintype.card_coe, Finset.card_singleton,
     Finset.card_insert_of_not_mem (mt finset.mem_singleton.mp hxy)]

Mathbin/Algebra/BigOperators/Order.lean

@@ -542,7 +542,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

Mathbin/Analysis/BoxIntegral/Partition/Split.lean

@@ -356,7 +356,7 @@ theorem not_disjoint_imp_le_of_subset_of_mem_splitMany {I J Js : Box ι} {s : Fi
     (H : ∀ i, {(i, J 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 split_many_le_split I (H i).1 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.lower i), Hle⟩

Mathbin/Analysis/Convex/Between.lean

@@ -782,7 +782,7 @@ theorem sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair [NoZeroSMulDivisors R V]
       by
       refine' affineSpan_pair_le_of_mem_of_mem (mem_affineSpan _ (Set.mem_range_self _)) _
       have hle : line[R, t.points i₂, t.points i₃] ≤ affineSpan R (Set.range t.points) := by
-        refine' affineSpan_mono _ _; simp [Set.insert_subset]
+        refine' affineSpan_mono _ _; simp [Set.insert_subset_iff]
       rw [AffineSubspace.le_def'] at hle 
       exact hle _ h₁.wbtw.mem_affine_span
     rw [AffineSubspace.le_def'] at hle 

Mathbin/Combinatorics/SimpleGraph/Basic.lean

@@ -1960,7 +1960,7 @@ theorem Adj.card_commonNeighbors_lt_degree {G : SimpleGraph V} [DecidableRel G.A
   constructor
   · rw [Set.mem_toFinset]
     apply not_mem_common_neighbors_right
-  · rw [Finset.insert_subset]
+  · rw [Finset.insert_subset_iff]
     constructor
     · simpa
     · rw [neighbor_finset, Set.toFinset_subset_toFinset]

Mathbin/Computability/TmToPartrec.lean

@@ -2037,7 +2037,7 @@ theorem trStmts₁_supports {S q} (H₁ : (q : Λ').Supports S) (HS₁ : trStmts
   have W := fun {q} => tr_stmts₁_self q
   induction q <;> simp [tr_stmts₁] 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₂ 
@@ -2131,7 +2131,7 @@ theorem codeSupp'_supports {S c k} (H : codeSupp c k ⊆ S) : Supports (codeSupp
     refine' supports_union.2 ⟨IHf H'.2, _⟩
     refine' tr_stmts₁_supports' (tr_normal_supports _) (Finset.union_subset_right h) fun h => _
     · simp only [code_supp', code_supp, Finset.union_subset_iff, cont_supp, tr_stmts₁,
-        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

Mathbin/Data/Finset/Basic.lean

@@ -1504,10 +1504,10 @@ theorem ne_insert_of_not_mem (s t : Finset α) {a : α} (h : a ∉ s) : s ≠ in
 #align finset.ne_insert_of_not_mem Finset.ne_insert_of_not_mem
 -/
 
-#print Finset.insert_subset /-
-theorem insert_subset : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by
+#print Finset.insert_subset_iff /-
+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
 -/
 
 #print Finset.subset_insert /-
@@ -1517,7 +1517,7 @@ theorem subset_insert (a : α) (s : Finset α) : s ⊆ insert a s := fun b => me
 
 #print Finset.insert_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
 -/
 
@@ -1601,7 +1601,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 a s 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'
@@ -2007,7 +2007,7 @@ theorem Directed.exists_mem_subset_of_finset_subset_biUnion {α ι : Type _} [hn
     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, trans hti hk'⟩
 #align directed.exists_mem_subset_of_finset_subset_bUnion Directed.exists_mem_subset_of_finset_subset_biUnion
 -/

Mathbin/Data/Finset/NAry.lean

@@ -305,7 +305,7 @@ 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

Mathbin/Data/Set/Basic.lean

@@ -1556,10 +1556,10 @@ theorem insert_ne_self : insert a s ≠ s ↔ a ∉ s :=
 #align set.insert_ne_self Set.insert_ne_self
 -/
 
-#print Set.insert_subset /-
-theorem insert_subset : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by
+#print Set.insert_subset_iff /-
+theorem insert_subset_iff : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by
   simp only [subset_def, or_imp, forall_and, forall_eq, mem_insert_iff]
-#align set.insert_subset Set.insert_subset
+#align set.insert_subset Set.insert_subset_iff
 -/
 
 #print Set.insert_subset_insert /-
@@ -1883,8 +1883,8 @@ theorem pair_comm (a b : α) : ({a, b} : Set α) = {b, a} :=
 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
   · tauto
   · rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> simp
@@ -3432,7 +3432,7 @@ theorem nontrivial_of_pair_subset {x y} (hxy : x ≠ y) (h : {x, y} ⊆ s) : s.N
 #print Set.Nontrivial.pair_subset /-
 theorem Nontrivial.pair_subset (hs : s.Nontrivial) : ∃ (x y : _) (hab : 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
 -/
 

Mathbin/FieldTheory/Adjoin.lean

@@ -487,7 +487,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 _ _)))

Mathbin/Geometry/Euclidean/Angle/Sphere.lean

@@ -131,7 +131,7 @@ theorem Cospherical.two_zsmul_oangle_eq {p₁ p₂ 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
 -/
@@ -456,7 +456,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)
@@ -492,7 +492,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]

Mathbin/Geometry/Euclidean/MongePoint.lean

@@ -569,7 +569,7 @@ theorem affineSpan_orthocenter_point_le_altitude (t : Triangle ℝ P) (i : Fin 3
     line[ℝ, t.orthocenter, t.points i] ≤ t.altitude i :=
   by
   refine' span_points_subset_coe_of_subset_coe _
-  rw [Set.insert_subset, Set.singleton_subset_iff]
+  rw [Set.insert_subset_iff, Set.singleton_subset_iff]
   exact ⟨t.orthocenter_mem_altitude, t.mem_altitude i⟩
 #align affine.triangle.affine_span_orthocenter_point_le_altitude Affine.Triangle.affineSpan_orthocenter_point_le_altitude
 
@@ -596,7 +596,7 @@ theorem altitude_replace_orthocenter_eq_affineSpan {t₁ t₂ : Triangle ℝ P}
     · have hu : (Finset.univ : Finset (Fin 3)) = {j₁, j₂, j₃} := by clear h₁ h₂ h₃; decide!
       rw [← Set.image_univ, ← Finset.coe_univ, hu, Finset.coe_insert, Finset.coe_insert,
         Finset.coe_singleton, Set.image_insert_eq, Set.image_insert_eq, Set.image_singleton, h₁, h₂,
-        h₃, Set.insert_subset, Set.insert_subset, Set.singleton_subset_iff]
+        h₃, Set.insert_subset_iff, Set.insert_subset_iff, Set.singleton_subset_iff]
       exact
         ⟨t₁.orthocenter_mem_affine_span, mem_affineSpan ℝ (Set.mem_range_self _),
           mem_affineSpan ℝ (Set.mem_range_self _)⟩

Mathbin/Geometry/Euclidean/Sphere/Basic.lean

@@ -348,7 +348,7 @@ theorem Cospherical.affineIndependent_of_mem_of_ne {s : Set P} (hs : Cospherical
     AffineIndependent ℝ ![p₁, p₂, p₃] :=
   by
   refine' hs.affine_independent _ _
-  · 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

Mathbin/GroupTheory/Perm/Cycle/Basic.lean

@@ -1994,7 +1994,7 @@ theorem closure_cycle_coprime_swap {n : ℕ} {σ : Perm α} (h0 : Nat.coprime n
   have h1' : is_cycle ((σ ^ n) ^ (m : ℤ)) := by rwa [← hm] at h1 
   replace h1' : is_cycle (σ ^ 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 _)))⟩

Mathbin/GroupTheory/Perm/Cycle/Type.lean

@@ -665,7 +665,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.order_of.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
 -/

Mathbin/LinearAlgebra/AffineSpace/AffineSubspace.lean

@@ -1721,7 +1721,7 @@ theorem vadd_right_mem_affineSpan_pair {p₁ p₂ : P} {v : V} :
 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
 -/

Mathbin/LinearAlgebra/AffineSpace/FiniteDimensional.lean

@@ -638,7 +638,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 p 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
 -/

Mathbin/LinearAlgebra/Span.lean

@@ -146,7 +146,7 @@ alias Submodule.map_span_le ← _root_.linear_map.map_span_le
 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
 -/
@@ -627,7 +627,7 @@ theorem span_insert (x) (s : Set M) : span R (insert x s) = span R ({x} : Set M)
 
 #print Submodule.span_insert_eq_span /-
 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
 -/
 

Mathbin/Order/CompactlyGenerated.lean

@@ -235,7 +235,7 @@ theorem WellFounded.isSupFiniteCompact (h : WellFounded ((· > ·) : α → α 
   ·
     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₁
@@ -499,7 +499,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
 -/

Mathbin/Order/Filter/CountableInter.lean

@@ -172,7 +172,7 @@ def Filter.ofCountableInter (l : Set (Set α))
   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
 -/
 

Mathbin/RingTheory/Adjoin/Basic.lean

@@ -268,7 +268,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
@@ -307,7 +307,7 @@ theorem adjoin_inl_union_inr_eq_prod (s) (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,

Mathbin/RingTheory/Finiteness.lean

@@ -114,7 +114,7 @@ theorem exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type _} [CommR
     rwa [mem_comap, span_empty, smul_bot, mem_bot] at hrn 
   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 

Mathbin/RingTheory/IntegralClosure.lean

@@ -371,7 +371,9 @@ 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).one_mem, Algebra.subset_adjoin⟩)) hz
+        (span_le.2
+            (Set.insert_subset_iff.2 ⟨(Algebra.adjoin S₀ ↑y).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)