chore: bump mathlib (#524)

Author: pitmonticone

Carleson/Classical/Helper.lean

@@ -5,10 +5,6 @@ import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
 
 open MeasureTheory
 
-theorem Real.volume_uIoc {a b : ℝ} : volume (Set.uIoc a b) = ENNReal.ofReal |b - a| := by
-  /- Cf. proof of Real.volume_interval-/
-  rw [Set.uIoc, volume_Ioc, max_sub_min_eq_abs]
-
 lemma intervalIntegral.integral_conj' {μ : Measure ℝ} {𝕜 : Type*} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} :
     ∫ x in a..b, (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ x in a..b, f x ∂μ) := by
   rw [intervalIntegral_eq_integral_uIoc, integral_conj, intervalIntegral_eq_integral_uIoc,

Carleson/Psi.lean

@@ -197,7 +197,7 @@ private lemma endpoint_sub_one (hx : 0 < x) (h : D ^ (-⌈logb D (4 * x)⌉) < 1
   rw [one_add_logb hD hx]
   apply le_antisymm
   · rw [← inv_eq_one_div, zpow_neg, inv_lt_inv₀ (by positivity) (cDx0 hD two_pos hx)] at h
-    rw [Int.floor_le_sub_one_iff, ← rpow_lt_rpow_left_iff hD,
+    rw [Int.le_sub_one_iff, Int.floor_lt, ← rpow_lt_rpow_left_iff hD,
       rpow_logb (D0 hD) (ne_of_gt hD) (cDx0 hD two_pos hx)]
     exact_mod_cast h
   · apply sub_le_iff_le_add.2 ∘ Int.ceil_le.2

Carleson/ToMathlib/MinLayer.lean

@@ -181,7 +181,7 @@ lemma iUnion_lt_minLayer_iff_bounded_series :
 all `LTSeries` in `A` have length at most `n`. -/
 lemma iUnion_minLayer_iff_bounded_series :
     ⋃ (k ≤ n), A.minLayer k = A ↔ ∀ p : LTSeries A, p.length ≤ n := by
-  simp [← lt_succ_iff, iUnion_lt_minLayer_iff_bounded_series]
+  simp_rw [← Nat.lt_succ_iff, iUnion_lt_minLayer_iff_bounded_series]
 
 variable [Fintype α]
 

lake-manifest.json

@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "32d24245c7a12ded17325299fd41d412022cd3fe",
+   "rev": "b66f9a38d12cfb6b0b1e4398f3936c33ecf9e10c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
+   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "19e5f5cc9c21199be466ef99489e3acab370f079",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
+   "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb12f5535c80e40119286d9575c9393562252d21",
+   "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
+   "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
+   "rev": "bc7b7f567dacc39ae904b6f12f6aa7f90e48e45f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",