diff --git a/Carleson/Carleson.lean b/Carleson/Carleson.lean
index 63c1ad35..d7ba3f11 100644
--- a/Carleson/Carleson.lean
+++ b/Carleson/Carleson.lean
@@ -65,7 +65,7 @@ lemma mem_nonzeroS_iff {i : ℤ} {x : ℝ} (hx : 0 < x) (hD : 1 < D) :
   rw [← lt_div_iff hx, mul_comm D⁻¹, ← div_lt_div_iff hx (by positivity)]
   rw [← Real.logb_inv, ← Real.logb_inv]
   rw [div_inv_eq_mul, ← zpow_add_one₀ (by positivity)]
-  simp_rw [← Real.rpow_int_cast]
+  simp_rw [← Real.rpow_intCast]
   rw [Real.lt_logb_iff_rpow_lt hD (by positivity), Real.logb_lt_iff_lt_rpow hD (by positivity)]
   simp [div_eq_mul_inv, mul_comm]
 
diff --git a/Carleson/CoverByBalls.lean b/Carleson/CoverByBalls.lean
index ca8763a2..b604b1f3 100644
--- a/Carleson/CoverByBalls.lean
+++ b/Carleson/CoverByBalls.lean
@@ -58,9 +58,7 @@ lemma CoveredByBalls.zero_right : CoveredByBalls s n 0 ↔ s = ∅ := by
   have h1 : CoveredByBalls s n 0 → s =∅ := by
     intro hcovered
     cases hcovered
-    case mk b hn hs
-    have h11 : ∀ x ∈b, ball x 0 = ∅ := by
-      exact fun x a ↦ ball_zero
+    case mk b hn hs =>
     simp at hs
     exact Set.subset_eq_empty hs rfl
   have h2 : s = ∅ → CoveredByBalls s n 0 := by
@@ -108,9 +106,7 @@ lemma BallsCoverBalls.pow_mul {a : ℝ} {k : ℕ} (h : ∀ r, BallsCoverBalls X
   case succ m h2 =>
     specialize h (r * a^m)
     rw[<- mul_assoc, mul_comm, <- mul_assoc] at h
-    norm_cast
-    ring_nf
-    rw[Nat.succ_eq_add_one, Nat.pow_add, pow_add, pow_one, pow_one, mul_comm (n^m) n]
+    rw[pow_succ, pow_succ, mul_comm (n^m) n]
     rw[mul_comm] at h2
     norm_cast at h2
     exact BallsCoverBalls.trans h h2
diff --git a/Carleson/HomogeneousType.lean b/Carleson/HomogeneousType.lean
index 43896875..840d052c 100644
--- a/Carleson/HomogeneousType.lean
+++ b/Carleson/HomogeneousType.lean
@@ -13,7 +13,8 @@ noncomputable section
 /-- A space of homogeneous type, or doubling measure metric space
 Note(F): I added `ProperSpace` to the definition (which I think doesn't follow from the rest?)
 and removed `SigmaFinite` (which follows from the rest).
-Should we assume `volume ≠ 0` / `IsOpenPosMeasure`? -/
+Should we assume `volume ≠ 0` / `IsOpenPosMeasure`?
+Remark: `IsUnifLocDoublingMeasure` which is a weaker notion in Mathlib. -/
 class IsSpaceOfHomogeneousType (X : Type*) (A : outParam ℝ) [PseudoMetricSpace X] extends
   MeasureSpace X, ProperSpace X, BorelSpace X,
   Regular (volume : Measure X), IsOpenPosMeasure (volume : Measure X) where
@@ -62,7 +63,8 @@ lemma volume_ball_le_same (x : X) {r s r': ℝ} (hsp : s > 0) (hs : r' ≤ s * r
         _ = volume.real (ball x (2 * 2 ^ m * r)) := by ring_nf
         _ ≤ A * volume.real (ball x (2 ^ m * r)) := by rw[mul_assoc]; norm_cast; apply volume_ball_two_le_same
         _ ≤ A * (↑(A ^ m) * volume.real (ball x r)) := by gcongr
-        _ = A^(Nat.succ m) * volume.real (ball x r) := by rw[<- mul_assoc]; norm_cast
+        _ = A^(m+1) * volume.real (ball x r) := by
+          rw[← mul_assoc, pow_succ, mul_comm _ A]
 
   /-Show inclusion in larger ball-/
   have haux : s * r ≤ 2 ^ ⌈Real.log s / Real.log 2⌉₊ * r := by
@@ -84,9 +86,6 @@ def Ad (A : ℝ) (s d : ℝ) : ℝ :=
 lemma ball_subset_ball_of_le {x x' : X} {r r' : ℝ}
   (hr : dist x x' + r' ≤ r) : ball x' r' ⊆ ball x r := by
     intro y h
-    have hA : 0 < A := by
-      calc 0 < 1 := by apply zero_lt_one
-        _ ≤ A := by exact hA
     have h1 : dist x y < r := by
       calc dist x y ≤ dist x x' + dist x' y := by apply dist_triangle
           _ < dist x x' + r' := by gcongr; apply mem_ball'.mp h
diff --git a/Carleson/ToMathlib/Finiteness.lean b/Carleson/ToMathlib/Finiteness.lean
index 22a6832a..0765cf25 100644
--- a/Carleson/ToMathlib/Finiteness.lean
+++ b/Carleson/ToMathlib/Finiteness.lean
@@ -24,7 +24,7 @@ open ENNReal
 /-! ## Lemmas -/
 
 theorem ENNReal.ofNat_ne_top (n : ℕ) [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) ≠ ∞ :=
-  ENNReal.nat_ne_top n
+  ENNReal.natCast_ne_top n
 
 theorem ENNReal.inv_ne_top' {a} (h : a ≠ 0) : a⁻¹ ≠ ∞ := ENNReal.inv_ne_top.2 h
 
@@ -39,7 +39,7 @@ attribute [aesop (rule_sets := [Finiteness]) unsafe 20%] ne_top_of_lt
 
 attribute [aesop (rule_sets := [Finiteness]) safe apply]
   Ne.lt_top
-  ENNReal.ofReal_ne_top ENNReal.coe_ne_top ENNReal.nat_ne_top
+  ENNReal.ofReal_ne_top ENNReal.coe_ne_top ENNReal.natCast_ne_top
   ENNReal.zero_ne_top ENNReal.one_ne_top ENNReal.ofNat_ne_top
   ENNReal.mul_ne_top ENNReal.add_ne_top' ENNReal.sub_ne_top ENNReal.inv_ne_top'
   MeasureTheory.measure_ne_top
diff --git a/lake-manifest.json b/lake-manifest.json
index 33c850e4..638a900e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,11 +1,11 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "e5306c3b0edefe722370b7387ee9bcd4631d6c17",
-   "name": "std",
+   "rev": "56d2e4ee226603eb6b90b05f6b944bde42672cd5",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
+   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,25 +22,25 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "8be30c25e3caa06937feeb62f7ca898370f80ee9",
+   "rev": "2225b0e4a3528da20499e2304b521e0c4c2a4563",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.36",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,56 +49,20 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "rev": "c46d22bbe4f8363c0829ce0eb48a95012cdc0d79",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "496f2278b1142e4c6dc5f73dd0a5d10700be4895",
+   "rev": "994f298c6c02a897c98574d2e11f3ba7b78d0578",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/xubaiw/CMark.lean",
-   "type": "git",
-   "subDir": null,
-   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
-   "name": "CMark",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "rev": "5b096942260d7805cc90bacf4ea4a0f8e9700ccb",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
-   "type": "git",
-   "subDir": null,
-   "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
-   "name": "leanInk",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "rev": "780bbec107cba79d18ec55ac2be3907a77f27f98",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "carleson",
  "lakeDir": ".lake"}
diff --git a/lean-toolchain b/lean-toolchain
index e35881ce..d8a6d7ef 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0-rc2
+leanprover/lean4:v4.8.0-rc1