From 5894b593ab4473d3e95c8d7b5d93a99cbfd0e2b7 Mon Sep 17 00:00:00 2001
From: grunweg <rothgang@math.uni-bonn.de>
Date: Mon, 10 Feb 2025 21:24:01 +0100
Subject: [PATCH] chore: bump to current mathlib (#230)

~~and a few other misc changes as I was playing with this branch, which
I'll remove from this PR soon~~ landed in #232
---
 Carleson/ToMathlib/RealInterpolation.lean |  4 ++--
 docbuild/lakefile.toml                    |  2 +-
 lake-manifest.json                        | 24 +++++++++++------------
 lean-toolchain                            |  2 +-
 4 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/Carleson/ToMathlib/RealInterpolation.lean b/Carleson/ToMathlib/RealInterpolation.lean
index 26179899..e9826049 100644
--- a/Carleson/ToMathlib/RealInterpolation.lean
+++ b/Carleson/ToMathlib/RealInterpolation.lean
@@ -2714,11 +2714,11 @@ lemma estimate_trnc₁ {spf : ScaledPowerFunction} {j : Bool}
       ((sel j p₀ p₁).toReal ⁻¹ * (sel j q₀ q₁).toReal) := by
     congr
     rw [← one_div]
-    refine (eLpNorm_eq_lintegral_rpow_enorm ?_ ?_).symm
+    refine (eLpNorm_eq_lintegral_rpow_enorm (ε := E₁) ?_ ?_).symm
     · exact (interpolated_pos' hp₀ hp₁ hp).ne'
     · exact interp_exp_ne_top hp₀p₁.ne ht hp
 
--- TODO: move this to Weaktype.lean?
+-- TODO: move this to WeakType.lean?
 lemma wnorm_eq_zero_iff {f : α → E₁} {p : ℝ≥0∞} [NormedAddCommGroup E₁] (hp : p ≠ 0) :
     wnorm f p μ = 0 ↔ f =ᵐ[μ] 0 := by
   unfold wnorm
diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml
index 647fce7c..c7f4ba7a 100644
--- a/docbuild/lakefile.toml
+++ b/docbuild/lakefile.toml
@@ -12,4 +12,4 @@ scope = "leanprover"
 name = "doc-gen4"
 # If you are developing against a release candidate or a stable version `v4.x`, replace `main` below by `v4.x`.
 # If you do not use `main` keep in mind to update this field as you update your Lean version.
-rev = "v4.16.0"
\ No newline at end of file
+rev = "main"
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
index b41bc9b9..9ad18b09 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a6276f4c6097675b1cf5ebd49b1146b735f38c02",
+   "rev": "ebbd72bd24186186016706e3716518fbc7aba085",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
+   "rev": "59a8514bb0ee5bae2689d8be717b5272c9b3dc1c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1a6613663c3eb08c401ce0fd1a408412f2c2321e",
+   "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,37 +55,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
+   "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.50",
+   "inputRev": "v0.0.52-pre",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
+   "rev": "ba9a63be53f16b3b6e4043641c6bad4883e650b4",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
+   "rev": "7b3b0c8327b3c0214ac49ca6d6922edbb81ab8c9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01006c9e86bf9e397c026fef4190478dd1fd897e",
+   "rev": "24cbb071689802fd6d3ff42198b19b125004c4e3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 8b4f470c..3ca992cf 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0
\ No newline at end of file
+leanprover/lean4:v4.17.0-rc1