bump to nightly-2023-10-09-06

mathlib commit leanprover-community/mathlib@ce64cd3

Mathbin/Data/Set/Basic.lean

@@ -1036,25 +1036,29 @@ 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 /-
 @[simp]
-theorem union_eq_left_iff_subset {s t : Set α} : s ∪ t = s ↔ t ⊆ s :=
+theorem union_eq_left {s t : Set α} : s ∪ t = s ↔ t ⊆ s :=
   sup_eq_left
-#align set.union_eq_left_iff_subset Set.union_eq_left_iff_subset
+#align set.union_eq_left_iff_subset Set.union_eq_left
+-/
 
+#print Set.union_eq_right /-
 @[simp]
-theorem union_eq_right_iff_subset {s t : Set α} : s ∪ t = t ↔ s ⊆ t :=
+theorem union_eq_right {s t : Set α} : s ∪ t = t ↔ s ⊆ t :=
   sup_eq_right
-#align set.union_eq_right_iff_subset Set.union_eq_right_iff_subset
+#align set.union_eq_right_iff_subset Set.union_eq_right
+-/
 
 #print Set.union_eq_self_of_subset_left /-
 theorem union_eq_self_of_subset_left {s t : Set α} (h : s ⊆ t) : s ∪ t = t :=
-  union_eq_right_iff_subset.mpr h
+  union_eq_right.mpr h
 #align set.union_eq_self_of_subset_left Set.union_eq_self_of_subset_left
 -/
 
 #print Set.union_eq_self_of_subset_right /-
 theorem union_eq_self_of_subset_right {s t : Set α} (h : t ⊆ s) : s ∪ t = s :=
-  union_eq_left_iff_subset.mpr h
+  union_eq_left.mpr h
 #align set.union_eq_self_of_subset_right Set.union_eq_self_of_subset_right
 -/
 

Mathbin/Data/Set/Semiring.lean

@@ -253,7 +253,7 @@ instance [CommMonoid α] : CanonicallyOrderedCommSemiring (SetSemiring α) :=
   { SetSemiring.idemSemiring, Set.commMonoid,
     SetSemiring.noZeroDivisors with
     add_le_add_left := fun a b => add_le_add_left
-    exists_add_of_le := fun a b ab => ⟨b, (union_eq_right_iff_subset.2 ab).symm⟩
+    exists_add_of_le := fun a b ab => ⟨b, (union_eq_right.2 ab).symm⟩
     le_self_add := subset_union_left }
 
 #print SetSemiring.imageHom /-

lake-manifest.json

@@ -4,18 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "2cd796118b1572a1b0b8b09ddd09f09f3664da30",
+    "rev": "6d3fe7de4958954d8050c9919b504d9c521d428e",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "2cd796118b1572a1b0b8b09ddd09f09f3664da30",
+    "inputRev?": "6d3fe7de4958954d8050c9919b504d9c521d428e",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "fb3884a6050e87d4cd7ed034b459f152d2b432a3",
+    "rev": "81fa8d9e845905d1ca6d742d17f63e2facb0eb88",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "fb3884a6050e87d4cd7ed034b459f152d2b432a3",
+    "inputRev?": "81fa8d9e845905d1ca6d742d17f63e2facb0eb88",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",

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-08-06"
+def tag : String := "nightly-2023-10-09-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"@"2cd796118b1572a1b0b8b09ddd09f09f3664da30"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"6d3fe7de4958954d8050c9919b504d9c521d428e"
 
 @[default_target]
 lean_lib Mathbin where