bump to nightly-2023-04-13-14

mathlib commit leanprover-community/mathlib@347636a
leanprover-community · Apr 13, 2023 · 7a1b67c · 7a1b67c
1 parent 51949a4
commit 7a1b67c
Show file tree

Hide file tree

Showing 8 changed files with 830 additions and 18 deletions.
diff --git a/Mathbin/Algebra/Category/Module/EpiMono.lean b/Mathbin/Algebra/Category/Module/EpiMono.lean
diff --git a/Mathbin/Analysis/Asymptotics/Theta.lean b/Mathbin/Analysis/Asymptotics/Theta.lean
diff --git a/Mathbin/Analysis/LocallyConvex/BalancedCoreHull.lean b/Mathbin/Analysis/LocallyConvex/BalancedCoreHull.lean
diff --git a/Mathbin/Analysis/Seminorm.lean b/Mathbin/Analysis/Seminorm.lean
@@ -1246,5 +1246,5 @@ theorem balanced_ball_zero : Balanced 𝕜 (Metric.ball (0 : E) r) :=
 end normSeminorm
 
 -- Guard against import creep.
-assert_not_exists balanced_core
+assert_not_exists balancedCore
 
diff --git a/Mathbin/Analysis/SpecialFunctions/Pow.lean b/Mathbin/Analysis/SpecialFunctions/Pow.lean
@@ -565,7 +565,7 @@ theorem isTheta_cpow_rpow (hl_im : IsBoundedUnder (· ≤ ·) l fun x => |(g x).
     (fun x => f x ^ g x) =Θ[l] fun x => abs (f x) ^ (g x).re :=
   calc
     (fun x => f x ^ g x) =Θ[l] fun x => abs (f x) ^ (g x).re / Real.exp (arg (f x) * im (g x)) :=
-      isTheta_of_norm_eventually_eq' <| hl.mono fun x => abs_cpow_of_imp
+      isTheta_of_norm_eventuallyEq' <| hl.mono fun x => abs_cpow_of_imp
     _ =Θ[l] fun x => abs (f x) ^ (g x).re / (1 : ℝ) :=
       ((isTheta_refl _ _).div (isTheta_exp_arg_mul_im hl_im))
     _ =ᶠ[l] fun x => abs (f x) ^ (g x).re := by simp only [of_real_one, div_one]

diff --git a/Mathbin/CategoryTheory/Sites/Sheafification.lean b/Mathbin/CategoryTheory/Sites/Sheafification.lean
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": "2863b2711ed6d4f96dee6f513825f52d5db4667a",
+    "rev": "924c93445ea760290567df9b739c360ea02802dc",
     "name": "lean3port",
-    "inputRev?": "2863b2711ed6d4f96dee6f513825f52d5db4667a"}},
+    "inputRev?": "924c93445ea760290567df9b739c360ea02802dc"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "4372f6e7d70e9c24feb09ae088b28ddc027b8f49",
+    "rev": "1f7abb829f7f8aa9fd5bcd2400945f18015006a3",
     "name": "mathlib",
-    "inputRev?": "4372f6e7d70e9c24feb09ae088b28ddc027b8f49"}},
+    "inputRev?": "1f7abb829f7f8aa9fd5bcd2400945f18015006a3"}},
   {"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-04-13-12"
+def tag : String := "nightly-2023-04-13-14"
 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"@"2863b2711ed6d4f96dee6f513825f52d5db4667a"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"924c93445ea760290567df9b739c360ea02802dc"
 
 @[default_target]
 lean_lib Mathbin where