bump to nightly-2023-10-03-06

mathlib commit leanprover-community/mathlib@ce64cd3

Mathbin/AlgebraicGeometry/AffineScheme.lean

@@ -406,7 +406,7 @@ theorem IsAffineOpen.basicOpenIsAffine {X : Scheme} {U : Opens X.carrier} (hU :
     hU.from_Spec.val.base '' (hU.from_Spec.val.base ⁻¹' (X.basic_open f : Set X.carrier)) =
       (X.basic_open f : Set X.carrier) :=
     by
-    rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset, hU.from_Spec_range]
+    rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left, hU.from_Spec_range]
     exact Scheme.basic_open_le _ _
   rw [Scheme.hom.opens_range_coe, Scheme.comp_val_base, ← this, coe_comp, Set.range_comp]
   congr 1
@@ -797,7 +797,7 @@ theorem IsAffineOpen.basicOpen_union_eq_self_iff {X : Scheme} {U : Opens X.carri
     apply_fun Set.image hU.from_Spec.1.base at h 
     rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.from_Spec_range] at
       h 
-    simp only [Set.inter_self, opens.carrier_eq_coe, Set.inter_eq_right_iff_subset] at h 
+    simp only [Set.inter_self, opens.carrier_eq_coe, Set.inter_eq_right] at h 
     ext1
     refine' Set.Subset.antisymm _ h
     simp only [Set.iUnion_subset_iff, SetCoe.forall, opens.coe_supr]

Mathbin/AlgebraicGeometry/OpenImmersion/Scheme.lean

@@ -760,7 +760,7 @@ theorem image_basicOpen {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersionCat f]
   rw [← e]
   ext1
   refine' set.image_preimage_eq_inter_range.trans _
-  erw [Set.inter_eq_left_iff_subset]
+  erw [Set.inter_eq_left]
   refine' Set.Subset.trans (Scheme.basic_open_le _ _) (Set.image_subset_range _ _)
   refine' le_trans (Scheme.basic_open_le _ _) (le_of_eq _)
   ext1
@@ -1234,7 +1234,7 @@ def morphismRestrictRestrictBasicOpen {X Y : Scheme} (f : X ⟶ Y) (U : Opens Y.
   rw [eq_to_hom_op, eq_to_hom_op, eq_to_hom_map, eq_to_hom_trans]
   erw [← e]
   ext1; dsimp [opens.map, opens.inclusion]
-  rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset, Subtype.range_coe]
+  rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left, Subtype.range_coe]
   exact Y.basic_open_le r
 #align algebraic_geometry.morphism_restrict_restrict_basic_open AlgebraicGeometry.morphismRestrictRestrictBasicOpen
 -/

Mathbin/Computability/TmToPartrec.lean

@@ -1887,8 +1887,7 @@ theorem codeSupp_comp (f g k) :
       trStmts₁ (trNormal (Code.comp f g) k) ∪ codeSupp g (Cont'.comp f k) :=
   by
   simp [code_supp, code_supp', cont_supp, Finset.union_assoc]
-  rw [← Finset.union_assoc _ _ (cont_supp k),
-    Finset.union_eq_right_iff_subset.2 (code_supp'_self _ _)]
+  rw [← Finset.union_assoc _ _ (cont_supp k), Finset.union_eq_right.2 (code_supp'_self _ _)]
 #align turing.partrec_to_TM2.code_supp_comp Turing.PartrecToTM2.codeSupp_comp
 -/
 

Mathbin/Data/Finset/Basic.lean

@@ -1944,32 +1944,32 @@ theorem insert_union_distrib (a : α) (s t : Finset α) :
 #align finset.insert_union_distrib Finset.insert_union_distrib
 -/
 
-#print Finset.union_eq_left_iff_subset /-
+#print Finset.union_eq_left /-
 @[simp]
-theorem union_eq_left_iff_subset {s t : Finset α} : s ∪ t = s ↔ t ⊆ s :=
+theorem union_eq_left {s t : Finset α} : s ∪ t = s ↔ t ⊆ s :=
   sup_eq_left
-#align finset.union_eq_left_iff_subset Finset.union_eq_left_iff_subset
+#align finset.union_eq_left_iff_subset Finset.union_eq_left
 -/
 
-#print Finset.left_eq_union_iff_subset /-
+#print Finset.left_eq_union /-
 @[simp]
-theorem left_eq_union_iff_subset {s t : Finset α} : s = s ∪ t ↔ t ⊆ s := by
+theorem left_eq_union {s t : Finset α} : s = s ∪ t ↔ t ⊆ s := by
   rw [← union_eq_left_iff_subset, eq_comm]
-#align finset.left_eq_union_iff_subset Finset.left_eq_union_iff_subset
+#align finset.left_eq_union_iff_subset Finset.left_eq_union
 -/
 
-#print Finset.union_eq_right_iff_subset /-
+#print Finset.union_eq_right /-
 @[simp]
-theorem union_eq_right_iff_subset {s t : Finset α} : s ∪ t = t ↔ s ⊆ t :=
+theorem union_eq_right {s t : Finset α} : s ∪ t = t ↔ s ⊆ t :=
   sup_eq_right
-#align finset.union_eq_right_iff_subset Finset.union_eq_right_iff_subset
+#align finset.union_eq_right_iff_subset Finset.union_eq_right
 -/
 
-#print Finset.right_eq_union_iff_subset /-
+#print Finset.right_eq_union /-
 @[simp]
-theorem right_eq_union_iff_subset {s t : Finset α} : s = t ∪ s ↔ t ⊆ s := by
+theorem right_eq_union {s t : Finset α} : s = t ∪ s ↔ t ⊆ s := by
   rw [← union_eq_right_iff_subset, eq_comm]
-#align finset.right_eq_union_iff_subset Finset.right_eq_union_iff_subset
+#align finset.right_eq_union_iff_subset Finset.right_eq_union
 -/
 
 #print Finset.union_congr_left /-
@@ -2384,10 +2384,10 @@ theorem inter_inter_inter_comm (s t u v : Finset α) : s ∩ t ∩ (u ∩ v) = s
 #align finset.inter_inter_inter_comm Finset.inter_inter_inter_comm
 -/
 
-#print Finset.union_eq_empty_iff /-
-theorem union_eq_empty_iff (A B : Finset α) : A ∪ B = ∅ ↔ A = ∅ ∧ B = ∅ :=
+#print Finset.union_eq_empty /-
+theorem union_eq_empty (A B : Finset α) : A ∪ B = ∅ ↔ A = ∅ ∧ B = ∅ :=
   sup_eq_bot_iff
-#align finset.union_eq_empty_iff Finset.union_eq_empty_iff
+#align finset.union_eq_empty_iff Finset.union_eq_empty
 -/
 
 #print Finset.union_subset_iff /-
@@ -2402,18 +2402,16 @@ theorem subset_inter_iff : s ⊆ t ∩ u ↔ s ⊆ t ∧ s ⊆ u :=
 #align finset.subset_inter_iff Finset.subset_inter_iff
 -/
 
-#print Finset.inter_eq_left_iff_subset /-
 @[simp]
 theorem inter_eq_left_iff_subset (s t : Finset α) : s ∩ t = s ↔ s ⊆ t :=
   inf_eq_left
 #align finset.inter_eq_left_iff_subset Finset.inter_eq_left_iff_subset
--/
 
-#print Finset.inter_eq_right_iff_subset /-
+#print Finset.inter_eq_right /-
 @[simp]
-theorem inter_eq_right_iff_subset (s t : Finset α) : t ∩ s = s ↔ s ⊆ t :=
+theorem inter_eq_right (s t : Finset α) : t ∩ s = s ↔ s ⊆ t :=
   inf_eq_right
-#align finset.inter_eq_right_iff_subset Finset.inter_eq_right_iff_subset
+#align finset.inter_eq_right_iff_subset Finset.inter_eq_right
 -/
 
 #print Finset.inter_congr_left /-

Mathbin/Data/Set/Basic.lean

@@ -1036,19 +1036,15 @@ theorem union_right_comm (s₁ s₂ s₃ : Set α) : s₁ ∪ s₂ ∪ s₃ = s
 #align set.union_right_comm Set.union_right_comm
 -/
 
-#print Set.union_eq_left_iff_subset /-
 @[simp]
 theorem union_eq_left_iff_subset {s t : Set α} : s ∪ t = s ↔ t ⊆ s :=
   sup_eq_left
 #align set.union_eq_left_iff_subset Set.union_eq_left_iff_subset
--/
 
-#print Set.union_eq_right_iff_subset /-
 @[simp]
 theorem union_eq_right_iff_subset {s t : Set α} : s ∪ t = t ↔ s ⊆ t :=
   sup_eq_right
 #align set.union_eq_right_iff_subset Set.union_eq_right_iff_subset
--/
 
 #print Set.union_eq_self_of_subset_left /-
 theorem union_eq_self_of_subset_left {s t : Set α} (h : s ⊆ t) : s ∪ t = t :=
@@ -1278,29 +1274,29 @@ theorem subset_inter_iff {s t r : Set α} : r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆
 #align set.subset_inter_iff Set.subset_inter_iff
 -/
 
-#print Set.inter_eq_left_iff_subset /-
+#print Set.inter_eq_left /-
 @[simp]
-theorem inter_eq_left_iff_subset {s t : Set α} : s ∩ t = s ↔ s ⊆ t :=
+theorem inter_eq_left {s t : Set α} : s ∩ t = s ↔ s ⊆ t :=
   inf_eq_left
-#align set.inter_eq_left_iff_subset Set.inter_eq_left_iff_subset
+#align set.inter_eq_left_iff_subset Set.inter_eq_left
 -/
 
-#print Set.inter_eq_right_iff_subset /-
+#print Set.inter_eq_right /-
 @[simp]
-theorem inter_eq_right_iff_subset {s t : Set α} : s ∩ t = t ↔ t ⊆ s :=
+theorem inter_eq_right {s t : Set α} : s ∩ t = t ↔ t ⊆ s :=
   inf_eq_right
-#align set.inter_eq_right_iff_subset Set.inter_eq_right_iff_subset
+#align set.inter_eq_right_iff_subset Set.inter_eq_right
 -/
 
 #print Set.inter_eq_self_of_subset_left /-
 theorem inter_eq_self_of_subset_left {s t : Set α} : s ⊆ t → s ∩ t = s :=
-  inter_eq_left_iff_subset.mpr
+  inter_eq_left.mpr
 #align set.inter_eq_self_of_subset_left Set.inter_eq_self_of_subset_left
 -/
 
 #print Set.inter_eq_self_of_subset_right /-
 theorem inter_eq_self_of_subset_right {s t : Set α} : t ⊆ s → s ∩ t = t :=
-  inter_eq_right_iff_subset.mpr
+  inter_eq_right.mpr
 #align set.inter_eq_self_of_subset_right Set.inter_eq_self_of_subset_right
 -/
 

Mathbin/LinearAlgebra/Multilinear/Basic.lean

@@ -628,7 +628,7 @@ theorem map_sum_finset_aux [DecidableEq ι] [Fintype ι] {n : ℕ} (h : ∑ i, (
         by
         simp only [B, C, Function.update_same, Finset.sdiff_union_self_eq_union]
         symm
-        simp only [hj₂, Finset.singleton_subset_iff, Finset.union_eq_left_iff_subset]
+        simp only [hj₂, Finset.singleton_subset_iff, Finset.union_eq_left]
       rw [this]
       apply Finset.sum_union
       apply Finset.disjoint_right.2 fun j hj => _

Mathbin/Probability/Process/HittingTime.lean

@@ -117,7 +117,7 @@ theorem hitting_of_le {m : ι} (hmn : m ≤ n) : hitting u s n m ω = m :=
   · simp only [hitting, Set.Icc_self, ite_eq_right_iff, Set.mem_Icc, exists_prop,
       forall_exists_index, and_imp]
     intro i hi₁ hi₂ hi
-    rw [Set.inter_eq_left_iff_subset.2, csInf_singleton]
+    rw [Set.inter_eq_left.2, csInf_singleton]
     exact Set.singleton_subset_iff.2 (le_antisymm hi₂ hi₁ ▸ hi)
   · exact hitting_of_lt h
 #align measure_theory.hitting_of_le MeasureTheory.hitting_of_le

Mathbin/Topology/MetricSpace/Basic.lean

@@ -2870,7 +2870,7 @@ theorem sphere_pi (x : ∀ b, π b) {r : ℝ} (h : 0 < r ∨ Nonempty β) :
   by
   obtain hr | rfl | hr := lt_trichotomy r 0
   · simp [hr]
-  · rw [closed_ball_eq_sphere_of_nonpos le_rfl, eq_comm, Set.inter_eq_right_iff_subset]
+  · rw [closed_ball_eq_sphere_of_nonpos le_rfl, eq_comm, Set.inter_eq_right]
     letI := h.resolve_left (lt_irrefl _)
     inhabit β
     refine' subset_Union_of_subset default _

Mathbin/Topology/QuasiSeparated.lean

@@ -80,17 +80,17 @@ theorem IsQuasiSeparated.image_of_embedding {s : Set α} (H : IsQuasiSeparated s
   convert
     (H (f ⁻¹' U) (f ⁻¹' V) _ (h.continuous.1 _ hU') _ _ (h.continuous.1 _ hV') _).image h.continuous
   · symm
-    rw [← Set.preimage_inter, Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset]
+    rw [← Set.preimage_inter, Set.image_preimage_eq_inter_range, Set.inter_eq_left]
     exact (Set.inter_subset_left _ _).trans (hU.trans (Set.image_subset_range _ _))
   · intro x hx; rw [← (h.inj.inj_on _).mem_image_iff (Set.subset_univ _) trivial]; exact hU hx
   · rw [h.is_compact_iff_is_compact_image]
     convert hU''
-    rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset]
+    rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
     exact hU.trans (Set.image_subset_range _ _)
   · intro x hx; rw [← (h.inj.inj_on _).mem_image_iff (Set.subset_univ _) trivial]; exact hV hx
   · rw [h.is_compact_iff_is_compact_image]
     convert hV''
-    rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left_iff_subset]
+    rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left]
     exact hV.trans (Set.image_subset_range _ _)
 #align is_quasi_separated.image_of_embedding IsQuasiSeparated.image_of_embedding
 -/

lake-manifest.json

@@ -4,18 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "baca076e572e7a3c8d372b043d83cf6a97582db9",
+    "rev": "9d9eac092a21d7187de7bf6bdb1f9a833c4b2089",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "baca076e572e7a3c8d372b043d83cf6a97582db9",
+    "inputRev?": "9d9eac092a21d7187de7bf6bdb1f9a833c4b2089",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "86831e868a1fc76bfa49a25cb554ff97cd8db284",
+    "rev": "2372c7a7b72bfd454fb451b676778b5e81b55db1",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "86831e868a1fc76bfa49a25cb554ff97cd8db284",
+    "inputRev?": "2372c7a7b72bfd454fb451b676778b5e81b55db1",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/gebner/quote4",

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-10-02-06"
+def tag : String := "nightly-2023-10-03-06"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"baca076e572e7a3c8d372b043d83cf6a97582db9"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"9d9eac092a21d7187de7bf6bdb1f9a833c4b2089"
 
 @[default_target]
 lean_lib Mathbin where