bump to nightly-2023-07-07-13

mathlib commit leanprover-community/mathlib@8905e5e
leanprover-community · Jul 7, 2023 · 569666a · 569666a
1 parent a151962
commit 569666a
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 6 deletions.
diff --git a/Mathbin/Data/Set/Function.lean b/Mathbin/Data/Set/Function.lean
@@ -238,9 +238,11 @@ theorem eqOn_empty (f₁ f₂ : α → β) : EqOn f₁ f₂ ∅ := fun x => Fals
 #align set.eq_on_empty Set.eqOn_empty
 -/
 
+#print Set.eqOn_singleton /-
 @[simp]
 theorem eqOn_singleton : EqOn f₁ f₂ {a} ↔ f₁ a = f₂ a := by simp [Set.EqOn]
 #align set.eq_on_singleton Set.eqOn_singleton
+-/
 
 #print Set.restrict_eq_restrict_iff /-
 @[simp]

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "5322b74b49567ceb15695e69d05014312190ad05",
+    "rev": "5676d39ca647849ac60e2d8cac0c292e76728cb3",
     "name": "lean3port",
-    "inputRev?": "5322b74b49567ceb15695e69d05014312190ad05"}},
+    "inputRev?": "5676d39ca647849ac60e2d8cac0c292e76728cb3"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "caec9984838902721a2dbc9ab3e885ee00731653",
+    "rev": "c4bb14cbd48da428ec1f6432e5fcd700a36ed07f",
     "name": "mathlib",
-    "inputRev?": "caec9984838902721a2dbc9ab3e885ee00731653"}},
+    "inputRev?": "c4bb14cbd48da428ec1f6432e5fcd700a36ed07f"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

diff --git a/lakefile.lean b/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-07-07-11"
+def tag : String := "nightly-2023-07-07-13"
 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"@"5322b74b49567ceb15695e69d05014312190ad05"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"5676d39ca647849ac60e2d8cac0c292e76728cb3"
 
 @[default_target]
 lean_lib Mathbin where