bump to nightly-2023-06-04-22

mathlib commit leanprover-community/mathlib@5f25c08
leanprover-community · Jun 4, 2023 · 3d1af1b · 3d1af1b
1 parent 2ecbc73
commit 3d1af1b
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 6 deletions.
diff --git a/Mathbin/Analysis/SpecialFunctions/Sqrt.lean b/Mathbin/Analysis/SpecialFunctions/Sqrt.lean
@@ -28,6 +28,7 @@ open scoped Topology
 
 namespace Real
 
+#print Real.sqLocalHomeomorph /-
 /-- Local homeomorph between `(0, +∞)` and `(0, +∞)` with `to_fun = λ x, x ^ 2` and
 `inv_fun = sqrt`. -/
 noncomputable def sqLocalHomeomorph : LocalHomeomorph ℝ ℝ
@@ -45,6 +46,7 @@ noncomputable def sqLocalHomeomorph : LocalHomeomorph ℝ ℝ
   continuous_toFun := (continuous_pow 2).ContinuousOn
   continuous_invFun := continuousOn_id.sqrt
 #align real.sq_local_homeomorph Real.sqLocalHomeomorph
+-/
 
 theorem deriv_sqrt_aux {x : ℝ} (hx : x ≠ 0) :
     HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ n, ContDiffAt ℝ n sqrt x :=

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "55eb71dd5b20804417231d017bdb6164afdb2184",
+    "rev": "e20fe52db37229493ee4b53649837d895d87c693",
     "name": "lean3port",
-    "inputRev?": "55eb71dd5b20804417231d017bdb6164afdb2184"}},
+    "inputRev?": "e20fe52db37229493ee4b53649837d895d87c693"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "9a28a6c4eca9f619bbd15297e90eff63915de56e",
+    "rev": "04d916cc591ef8675d9a48d20fe2694bfc21ca38",
     "name": "mathlib",
-    "inputRev?": "9a28a6c4eca9f619bbd15297e90eff63915de56e"}},
+    "inputRev?": "04d916cc591ef8675d9a48d20fe2694bfc21ca38"}},
   {"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-06-04-20"
+def tag : String := "nightly-2023-06-04-22"
 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"@"55eb71dd5b20804417231d017bdb6164afdb2184"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e20fe52db37229493ee4b53649837d895d87c693"
 
 @[default_target]
 lean_lib Mathbin where