bump to nightly-2023-06-30-19

mathlib commit leanprover-community/mathlib@9240e8b

Mathbin/Analysis/NormedSpace/Pointwise.lean

@@ -136,16 +136,16 @@ theorem smul_closedBall' {c : 𝕜} (hc : c ≠ 0) (x : E) (r : ℝ) :
 #align smul_closed_ball' smul_closedBall'
 -/
 
-#print Metric.Bounded.smul /-
-theorem Metric.Bounded.smul {s : Set E} (hs : Bounded s) (c : 𝕜) : Bounded (c • s) :=
+#print Metric.Bounded.smul₀ /-
+theorem Metric.Bounded.smul₀ {s : Set E} (hs : Bounded s) (c : 𝕜) : Bounded (c • s) :=
   by
   obtain ⟨R, hR⟩ : ∃ R : ℝ, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le
   refine' bounded_iff_forall_norm_le.2 ⟨‖c‖ * R, fun z hz => _⟩
   obtain ⟨y, ys, rfl⟩ : ∃ y : E, y ∈ s ∧ c • y = z := mem_smul_set.1 hz
   calc
     ‖c • y‖ = ‖c‖ * ‖y‖ := norm_smul _ _
     _ ≤ ‖c‖ * R := mul_le_mul_of_nonneg_left (hR y ys) (norm_nonneg _)
-#align metric.bounded.smul Metric.Bounded.smul
+#align metric.bounded.smul Metric.Bounded.smul₀
 -/
 
 #print eventually_singleton_add_smul_subset /-

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "56a733b82ba0ba62e93d52f90dc97675e3e5b209",
+    "rev": "248dee5c15dd3ce4477ed6c7be239b3f974b0bf3",
     "name": "lean3port",
-    "inputRev?": "56a733b82ba0ba62e93d52f90dc97675e3e5b209"}},
+    "inputRev?": "248dee5c15dd3ce4477ed6c7be239b3f974b0bf3"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "e71da81e8a9278f1dd851419dcd766b30feec966",
+    "rev": "a59175a8a4c6f4ac1e26612891465c0518ce04f3",
     "name": "mathlib",
-    "inputRev?": "e71da81e8a9278f1dd851419dcd766b30feec966"}},
+    "inputRev?": "a59175a8a4c6f4ac1e26612891465c0518ce04f3"}},
   {"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-30-17"
+def tag : String := "nightly-2023-06-30-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"@"56a733b82ba0ba62e93d52f90dc97675e3e5b209"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"248dee5c15dd3ce4477ed6c7be239b3f974b0bf3"
 
 @[default_target]
 lean_lib Mathbin where