bump mathlib

fpvandoorn · Sep 9, 2024 · 9750bee · 9750bee
1 parent 75b3951
commit 9750bee
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/Carleson.lean b/Carleson.lean
@@ -24,13 +24,16 @@ import Carleson.HardyLittlewood
 import Carleson.HolderVanDerCorput
 import Carleson.LinearizedMetricCarleson
 import Carleson.MetricCarleson
+import Carleson.MinLayerTiles
 import Carleson.Psi
 import Carleson.RealInterpolation
 import Carleson.TileExistence
 import Carleson.TileStructure
 import Carleson.ToMathlib.Finiteness
 import Carleson.ToMathlib.Finiteness.Attr
+import Carleson.ToMathlib.Height
 import Carleson.ToMathlib.MeasureReal
+import Carleson.ToMathlib.MinLayer
 import Carleson.ToMathlib.Misc
 import Carleson.TwoSidedMetricCarleson
 import Carleson.WeakType
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8feac540abb781cb1349688c816dc02fae66b49c",
+   "rev": "d11566f4c8ca80dbe87630b606c608274c7380fd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8c811c94af285516e8c76a63165c87027f18ccd0",
+   "rev": "d9a27f6094744c840dc41eee71fb4b606a61ddb7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",