diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index aeda2b9413..2414881d10 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -6,9 +6,7 @@ import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Basic
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
 import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Mathlib.Data.Real.ConjExponents
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
@@ -35,7 +33,6 @@ import LeanAPAP.Prereqs.Convolution.Order
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.Convolution.WithConv
 import LeanAPAP.Prereqs.Energy
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.FourierTransform.Discrete
diff --git a/LeanAPAP/Mathlib/Data/Complex/Basic.lean b/LeanAPAP/Mathlib/Data/Complex/Basic.lean
deleted file mode 100644
index 62b10cd0ff..0000000000
--- a/LeanAPAP/Mathlib/Data/Complex/Basic.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import Mathlib.Data.Complex.Basic
-
-namespace Complex
-
-@[simp] lemma coe_comp_sub {α : Type*} (f g : α → ℝ) :
-    ofReal' ∘ (f - g) = ofReal' ∘ f - ofReal' ∘ g := map_comp_sub ofReal _ _
-
-end Complex
diff --git a/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean b/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean
deleted file mode 100644
index 3f2942ae9b..0000000000
--- a/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-import Mathlib.Data.ENNReal.Operations
-
-namespace ENNReal
-variable {a b c : ℝ≥0∞}
-
-protected lemma sub_eq_of_eq_add' (ha : a ≠ ∞) (h : a = c + b) : a - b = c :=
-  ENNReal.sub_eq_of_eq_add (mt (by rintro rfl; simpa using h) ha) h
-
-protected lemma eq_sub_of_add_eq' (hb : b ≠ ∞) (h : a + c = b) : a = b - c :=
-  ENNReal.eq_sub_of_add_eq (mt (by rintro rfl; simpa [eq_comm] using h) hb) h
-
-protected lemma sub_eq_of_eq_add_rev' (ha : a ≠ ∞) (h : a = b + c) : a - b = c :=
-  ENNReal.sub_eq_of_eq_add_rev (mt (by rintro rfl; simpa using h) ha) h
-
-end ENNReal
diff --git a/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean b/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean
index c34b1cba25..3cea583d55 100644
--- a/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean
+++ b/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean
@@ -1,6 +1,5 @@
 import Mathlib.Data.ENNReal.Inv
 import Mathlib.Data.Real.ConjExponents
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
 
 open scoped NNReal
 
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index 2e37f02717..2e0e59fa84 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -3,7 +3,6 @@ import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 
diff --git a/LeanAPAP/Prereqs/Balance/Complex.lean b/LeanAPAP/Prereqs/Balance/Complex.lean
index 18bab88079..8aeda4b99c 100644
--- a/LeanAPAP/Prereqs/Balance/Complex.lean
+++ b/LeanAPAP/Prereqs/Balance/Complex.lean
@@ -1,5 +1,6 @@
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Data.Complex.BigOperators
 import LeanAPAP.Prereqs.Balance.Defs
-import LeanAPAP.Prereqs.Expect.Complex
 
 open Finset
 open scoped BigOperators NNReal
@@ -28,4 +29,3 @@ lemma coe_balance : (↑(balance f a) : 𝕜) = balance ((↑) ∘ f) a := map_b
   simp [balance]
 
 end RCLike
-
diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean
index a2f6bcd7f0..1dd94ee45e 100644
--- a/LeanAPAP/Prereqs/Convolution/Compact.lean
+++ b/LeanAPAP/Prereqs/Convolution/Compact.lean
@@ -1,6 +1,5 @@
 import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 
 /-!
@@ -393,11 +392,11 @@ end Field
 namespace RCLike
 variable {𝕜 : Type} [RCLike 𝕜] (f g : G → ℝ) (a : G)
 
-@[simp, norm_cast]
-lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) a := map_cconv (algebraMap ℝ 𝕜) _ _ _
+@[simp, norm_cast] lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) a :=
+  map_cconv (algebraMap ℝ 𝕜) ..
 
-@[simp, norm_cast]
-lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → 𝕜) a := by simp [cdconv_apply, coe_expect]
+@[simp, norm_cast] lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → 𝕜) a := by
+  simp [cdconv_apply, ofReal_expect]
 
 @[simp]
 lemma coe_comp_cconv : ofReal ∘ (f ∗ₙ g) = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) := funext $ coe_cconv _ _
diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean
index 7c87e5c29e..38ed01cada 100644
--- a/LeanAPAP/Prereqs/Energy.lean
+++ b/LeanAPAP/Prereqs/Energy.lean
@@ -1,6 +1,5 @@
 import LeanAPAP.Prereqs.AddChar.Basic
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 
diff --git a/LeanAPAP/Prereqs/Expect/Complex.lean b/LeanAPAP/Prereqs/Expect/Complex.lean
deleted file mode 100644
index 94805cf3cd..0000000000
--- a/LeanAPAP/Prereqs/Expect/Complex.lean
+++ /dev/null
@@ -1,43 +0,0 @@
-import Mathlib.Algebra.Order.BigOperators.Expect
-import Mathlib.Analysis.RCLike.Basic
-import Mathlib.Data.Complex.Basic
-
-open Finset
-open scoped BigOperators NNReal
-
-section
-variable {ι K E : Type*} [RCLike K] [NormedField E] [CharZero E] [NormedSpace K E]
-
-include K in
-@[bound]
-lemma norm_expect_le {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ :=
-  le_expect_of_subadditive norm_zero norm_add_le (fun _ _ ↦ by rw [RCLike.norm_nnqsmul K])
-
-end
-
-namespace NNReal
-variable {ι : Type*}
-
-@[simp, norm_cast]
-lemma coe_expect (s : Finset ι) (f : ι → ℝ≥0) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : ℝ) :=
-  map_expect toRealHom ..
-
-end NNReal
-
-namespace Complex
-variable {ι : Type*}
-
-@[simp, norm_cast]
-lemma ofReal_expect (s : Finset ι) (f : ι → ℝ) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : ℂ) :=
-  map_expect ofReal ..
-
-end Complex
-
-namespace RCLike
-variable {ι 𝕜 : Type*} [RCLike 𝕜]
-
-@[simp, norm_cast]
-lemma coe_expect (s : Finset ι) (f : ι → ℝ) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : 𝕜) :=
-  map_expect (algebraMap ..) ..
-
-end RCLike
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean
index 684664b845..42a2190810 100644
--- a/LeanAPAP/Prereqs/LpNorm/Compact.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean
@@ -4,7 +4,6 @@ import Mathlib.Data.Finset.Density
 import Mathlib.Data.Fintype.Order
 import Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.NNLpNorm
diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
index 8f80578f18..96d1c94d22 100644
--- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
+++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Yaël Dillies, Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
+import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalitiesPow
 import Mathlib.Data.Nat.Choose.Multinomial
 import Mathlib.Tactic.Positivity.Finset
@@ -39,7 +40,7 @@ private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι)
     _ = (∑ b in B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / B.card ^ m / B.card := by
       rw [div_div, ← _root_.pow_succ]
     _ ≤ (∑ b in B, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / B.card := by
-      gcongr; exact pow_sum_div_card_le_sum_pow _ _ fun _ _ ↦ abs_nonneg _
+      gcongr; exact pow_sum_div_card_le_sum_pow (fun _ _ ↦ abs_nonneg _) _
     _ = _ := by simp [B]
 
 private lemma step_one' (hA : A.Nonempty) (f : ι → ℝ) (hf : ∀ i, ∑ a in A ^^ n, f (a i) = 0) (m : ℕ)
@@ -227,7 +228,7 @@ theorem marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → ℝ) (hf : ∀ i, ∑ a
       simp_rw [mul_assoc, mul_sum]; rfl
   gcongr with a
   rw [← div_le_iff₀']
-  have := Real.pow_sum_div_card_le_sum_pow (f := fun i ↦ f (a i) ^ 2) univ m fun i _ ↦ ?_
+  have := pow_sum_div_card_le_sum_pow (f := fun i ↦ f (a i) ^ 2) (s := univ) (fun i _ ↦ ?_) m
   simpa only [Finset.card_fin, pow_mul] using this
   all_goals { positivity }
 
diff --git a/LeanAPAP/Prereqs/Randomisation.lean b/LeanAPAP/Prereqs/Randomisation.lean
index ead086fdb0..a5a24e469d 100644
--- a/LeanAPAP/Prereqs/Randomisation.lean
+++ b/LeanAPAP/Prereqs/Randomisation.lean
@@ -1,6 +1,5 @@
 import Mathlib.Combinatorics.Additive.Dissociation
 import LeanAPAP.Prereqs.AddChar.Basic
-import LeanAPAP.Prereqs.Expect.Complex
 
 /-!
 # Randomisation
diff --git a/lake-manifest.json b/lake-manifest.json
index fb1d2a96d1..b6231c8aca 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd",
+   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a",
+   "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
+   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "rev": "781beceb959c68b36d3d96205b3531e341879d2c",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "eed3300c27c9f168d53e13bb198a92a147b671d0",
+   "rev": "d902abe2c36d37eb76fddd9e43290bcef3bcb6e8",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7afce91e4fcee25c1ed06dca8d71b82bed396776",
+   "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0a294fe9bf23b396c5cc955054c50b9b652ec5ad",
+   "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0",
+   "rev": "5119580cd7510a440d54f67834c9024cc03a3e32",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 98556ba065..89985206ac 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0-rc1
+leanprover/lean4:v4.12.0