bump to nightly-2023-06-12-19

mathlib commit leanprover-community/mathlib@ccdbfb6

Mathbin/Analysis/Calculus/Darboux.lean

@@ -80,6 +80,7 @@ theorem exists_hasDerivWithinAt_eq_of_lt_of_gt (hab : a ≤ b)
   ⟨c, cmem, neg_injective hc⟩
 #align exists_has_deriv_within_at_eq_of_lt_of_gt exists_hasDerivWithinAt_eq_of_lt_of_gt
 
+#print Set.OrdConnected.image_hasDerivWithinAt /-
 /-- **Darboux's theorem**: the image of an `ord_connected` set under `f'` is an `ord_connected`
 set, `has_deriv_within_at` version. -/
 theorem Set.OrdConnected.image_hasDerivWithinAt {s : Set ℝ} (hs : OrdConnected s)
@@ -99,20 +100,25 @@ theorem Set.OrdConnected.image_hasDerivWithinAt {s : Set ℝ} (hs : OrdConnected
       ⟨c, cmem, hc⟩
     exact ⟨c, this <| Ioo_subset_Icc_self cmem, hc⟩
 #align set.ord_connected.image_has_deriv_within_at Set.OrdConnected.image_hasDerivWithinAt
+-/
 
+#print Set.OrdConnected.image_derivWithin /-
 /-- **Darboux's theorem**: the image of an `ord_connected` set under `f'` is an `ord_connected`
 set, `deriv_within` version. -/
 theorem Set.OrdConnected.image_derivWithin {s : Set ℝ} (hs : OrdConnected s)
     (hf : DifferentiableOn ℝ f s) : OrdConnected (derivWithin f s '' s) :=
   hs.image_hasDerivWithinAt fun x hx => (hf x hx).HasDerivWithinAt
 #align set.ord_connected.image_deriv_within Set.OrdConnected.image_derivWithin
+-/
 
+#print Set.OrdConnected.image_deriv /-
 /-- **Darboux's theorem**: the image of an `ord_connected` set under `f'` is an `ord_connected`
 set, `deriv` version. -/
 theorem Set.OrdConnected.image_deriv {s : Set ℝ} (hs : OrdConnected s)
     (hf : ∀ x ∈ s, DifferentiableAt ℝ f x) : OrdConnected (deriv f '' s) :=
   hs.image_hasDerivWithinAt fun x hx => (hf x hx).HasDerivAt.HasDerivWithinAt
 #align set.ord_connected.image_deriv Set.OrdConnected.image_deriv
+-/
 
 /-- **Darboux's theorem**: the image of a convex set under `f'` is a convex set,
 `has_deriv_within_at` version. -/

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "bd859914b929536d98022af748b18980e9352dac",
+    "rev": "3e3ca24aa2e8d9d70ac7f22efbdecb344c466808",
     "name": "lean3port",
-    "inputRev?": "bd859914b929536d98022af748b18980e9352dac"}},
+    "inputRev?": "3e3ca24aa2e8d9d70ac7f22efbdecb344c466808"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "9d9686a1a7f20dc343cba1a83401e30cbfea9f97",
+    "rev": "021caebae2e1d4a57add2ed679feedc649eab0ca",
     "name": "mathlib",
-    "inputRev?": "9d9686a1a7f20dc343cba1a83401e30cbfea9f97"}},
+    "inputRev?": "021caebae2e1d4a57add2ed679feedc649eab0ca"}},
   {"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-06-12-17"
+def tag : String := "nightly-2023-06-12-19"
 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"@"bd859914b929536d98022af748b18980e9352dac"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"3e3ca24aa2e8d9d70ac7f22efbdecb344c466808"
 
 @[default_target]
 lean_lib Mathbin where