bump to nightly-2023-03-31-16

mathlib commit leanprover-community/mathlib@ce11c3c

Mathbin/Data/Set/List.lean

@@ -25,6 +25,7 @@ variable {α β : Type _} (l : List α)
 
 namespace Set
 
+#print Set.range_list_map /-
 theorem range_list_map (f : α → β) : range (map f) = { l | ∀ x ∈ l, x ∈ range f } :=
   by
   refine'
@@ -35,27 +36,35 @@ theorem range_list_map (f : α → β) : range (map f) = { l | ∀ x ∈ l, x 
   rcases hl a (mem_cons_self _ _) with ⟨a, rfl⟩
   exact ⟨a :: l, map_cons _ _ _⟩
 #align set.range_list_map Set.range_list_map
+-/
 
+#print Set.range_list_map_coe /-
 theorem range_list_map_coe (s : Set α) : range (map (coe : s → α)) = { l | ∀ x ∈ l, x ∈ s } := by
   rw [range_list_map, Subtype.range_coe]
 #align set.range_list_map_coe Set.range_list_map_coe
+-/
 
+#print Set.range_list_nthLe /-
 @[simp]
 theorem range_list_nthLe : (range fun k : Fin l.length => l.nthLe k k.2) = { x | x ∈ l } :=
   by
   ext x
   rw [mem_set_of_eq, mem_iff_nth_le]
   exact ⟨fun ⟨⟨n, h₁⟩, h₂⟩ => ⟨n, h₁, h₂⟩, fun ⟨n, h₁, h₂⟩ => ⟨⟨n, h₁⟩, h₂⟩⟩
 #align set.range_list_nth_le Set.range_list_nthLe
+-/
 
+#print Set.range_list_get? /-
 theorem range_list_get? : range l.get? = insert none (some '' { x | x ∈ l }) :=
   by
   rw [← range_list_nth_le, ← range_comp]
   refine' (range_subset_iff.2 fun n => _).antisymm (insert_subset.2 ⟨_, _⟩)
   exacts[(le_or_lt l.length n).imp nth_eq_none_iff.2 fun hlt => ⟨⟨_, _⟩, (nth_le_nth hlt).symm⟩,
     ⟨_, nth_eq_none_iff.2 le_rfl⟩, range_subset_iff.2 fun k => ⟨_, nth_le_nth _⟩]
 #align set.range_list_nth Set.range_list_get?
+-/
 
+#print Set.range_list_getD /-
 @[simp]
 theorem range_list_getD (d : α) : (range fun n => l.getD n d) = insert d { x | x ∈ l } :=
   calc
@@ -65,11 +74,14 @@ theorem range_list_getD (d : α) : (range fun n => l.getD n d) = insert d { x |
       simp only [range_list_nth, image_insert_eq, Option.getD, image_image, image_id']
     
 #align set.range_list_nthd Set.range_list_getD
+-/
 
+#print Set.range_list_getI /-
 @[simp]
 theorem range_list_getI [Inhabited α] (l : List α) : range l.getI = insert default { x | x ∈ l } :=
   range_list_getD l default
 #align set.range_list_inth Set.range_list_getI
+-/
 
 end Set
 

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "6766126ec237f5eb6e1b30dc77e2d3a99f24a0d6",
+    "rev": "b0454e2da1c1b36d9a01127da67847cc5c20361b",
     "name": "lean3port",
-    "inputRev?": "6766126ec237f5eb6e1b30dc77e2d3a99f24a0d6"}},
+    "inputRev?": "b0454e2da1c1b36d9a01127da67847cc5c20361b"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "98f40c35a2da7b450c5908784b6dcc20ba32ec3d",
+    "rev": "dcbcc203ad12e36fabe281a0432dee63ee40b8d5",
     "name": "mathlib",
-    "inputRev?": "98f40c35a2da7b450c5908784b6dcc20ba32ec3d"}},
+    "inputRev?": "dcbcc203ad12e36fabe281a0432dee63ee40b8d5"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

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-03-31-14"
+def tag : String := "nightly-2023-03-31-16"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"6766126ec237f5eb6e1b30dc77e2d3a99f24a0d6"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"b0454e2da1c1b36d9a01127da67847cc5c20361b"
 
 @[default_target]
 lean_lib Mathbin where