bump mathlib (#330)

previous version gave errors for some people

Author: fpvandoorn

Carleson/ToMathlib/Misc.lean

@@ -139,8 +139,9 @@ lemma lintegral_Ioc_partition {a b : ℕ} {c : ℝ} {f : ℝ → ℝ≥0∞} (hc
     have li : a * c ≤ b * c := by gcongr
     rw [← Ioc_union_Ioc_eq_Ioc li (by gcongr; omega),
       lintegral_union measurableSet_Ioc (Ioc_disjoint_Ioc_of_le le_rfl),
-      Nat.Ico_succ_right_eq_insert_Ico h, Finset.sum_insert Finset.right_not_mem_Ico,
-      add_comm (lintegral ..), ih]
+      ← Order.succ_eq_add_one, ← Finset.insert_Ico_right_eq_Ico_succ h,
+      Finset.sum_insert Finset.right_not_mem_Ico,
+      add_comm (lintegral ..), ih, Order.succ_eq_add_one]
 
 /-! ## Averaging -/
 
@@ -274,11 +275,7 @@ end eLpNorm
 
 namespace MemLp
 
-variable {f : α → F} {p : ℝ≥0∞}
-theorem enorm (hf : MemLp f p μ) : MemLp (‖f ·‖ₑ) p μ :=
-  ⟨hf.aestronglyMeasurable.enorm.aestronglyMeasurable,
-    by simp_rw [MeasureTheory.eLpNorm_enorm, hf.eLpNorm_lt_top]⟩
-
+variable {p : ℝ≥0∞}
 theorem toReal {f : α → ℝ≥0∞} (hf : MemLp f p μ) : MemLp (f · |>.toReal) p μ :=
   ⟨hf.aestronglyMeasurable.aemeasurable.ennreal_toReal.aestronglyMeasurable,
     eLpNorm_toReal_le.trans_lt hf.eLpNorm_lt_top⟩

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "529c13b5da1ff47aef41dbebd4d004fdf353aaf7",
+   "rev": "a336c585a94229b8ec3b48abfba42bdd4c0caf7c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -45,10 +45,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24f15e3fbeb4df449dacb61f761a136e9c989a94",
+   "rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
@@ -85,17 +85,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "92079574ccbf31af64468cb70f0f9da6c0138997",
+   "rev": "78e1181c4752c7e10874d2ed5a6a15063f4a35b6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "lean-pr-testing-8161",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "aff4176e5c41737a0d73be74ad9feb6a889bfa98",
+   "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.20.0-rc2
+leanprover/lean4:v4.20.0-rc4