diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index dc5c086c19..c1dc7abf71 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -4,6 +4,7 @@ import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Algebra.BigOperators.Group.Finset
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Group.Basic
+import LeanAPAP.Mathlib.Algebra.Group.Pointwise.Finset
 import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic
 import LeanAPAP.Mathlib.Algebra.Order.BigOperators.Group.Finset
 import LeanAPAP.Mathlib.Algebra.Order.Field.Defs
@@ -24,8 +25,8 @@ import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Operations
 import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Mathlib.Data.Finset.Density
-import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic
 import LeanAPAP.Mathlib.Data.Finset.Preimage
+import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Mathlib.Data.Real.ConjExponents
 import LeanAPAP.Mathlib.Data.ZMod.Module
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
diff --git a/LeanAPAP/Mathlib/Data/Finset/Pointwise/Basic.lean b/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean
similarity index 85%
rename from LeanAPAP/Mathlib/Data/Finset/Pointwise/Basic.lean
rename to LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean
index c532082453..90f2073173 100644
--- a/LeanAPAP/Mathlib/Data/Finset/Pointwise/Basic.lean
+++ b/LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean
@@ -1,5 +1,5 @@
+import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.Data.Finset.Density
-import Mathlib.Data.Finset.Pointwise.Basic
 
 open scoped Pointwise
 
diff --git a/LeanAPAP/Mathlib/Data/Fintype/Basic.lean b/LeanAPAP/Mathlib/Data/Fintype/Basic.lean
new file mode 100644
index 0000000000..2920eebb80
--- /dev/null
+++ b/LeanAPAP/Mathlib/Data/Fintype/Basic.lean
@@ -0,0 +1,3 @@
+import Mathlib.Data.Fintype.Basic
+
+attribute [simp] Finset.univ_nonempty
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
index 5f1fc2451f..2a8335967c 100644
--- a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
+++ b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
@@ -1,6 +1,5 @@
 import Mathlib.MeasureTheory.Function.EssSup
 import Mathlib.Probability.ConditionalProbability
-import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
 
 open Filter MeasureTheory ProbabilityTheory
 open scoped ENNReal
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index d39f62cea6..b0a33275ed 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -200,7 +200,7 @@ lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0)
     ∃ a : Fin k → G, a ∈ L ∧
       L.card * S.card ≤ (A + S).card ^ k * (univ.filter fun t : G ↦ (a - fun _ ↦ t) ∈ L).card := by
   rcases S.eq_empty_or_nonempty with (rfl | hS)
-  · simpa only [card_empty, mul_zero, zero_le', and_true_iff] using hL'
+  · simpa only [card_empty, mul_zero, zero_le', and_true] using hL'
   have hS' : 0 < S.card := by rwa [card_pos]
   have : (L + S.piDiag (Fin k)).card ≤ (A + S).card ^ k := by
     refine (card_le_card (add_subset_add_right hL)).trans ?_
@@ -421,7 +421,7 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (
     exact T_bound hK₂ L.card S.card A.card (A + S).card _ rfl hL' this
       (by rw [← cast_addConst_mul_card]; gcongr) hA.card_pos hε hε' hm
   intro t ht
-  simp only [exists_prop, exists_eq_right, mem_filter, mem_univ, true_and_iff] at ht
+  simp only [exists_prop, exists_eq_right, mem_filter, mem_univ, true_and] at ht
   have := just_the_triangle_inequality ha ht hk.bot_lt hm
   rwa [neg_neg, mul_div_cancel₀ _ (two_ne_zero' ℝ)] at this
 
diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean
index 8a363c5242..3c3457c47c 100644
--- a/LeanAPAP/Physics/DRC.lean
+++ b/LeanAPAP/Physics/DRC.lean
@@ -94,7 +94,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         (dconv_nonneg indicate_nonneg indicate_nonneg) _) fun _ ↦ by simp -- positivity
     refine Fintype.sum_pos $ this.gt_iff_ne.2 $ support_nonempty_iff.1 ?_
     simp only [support_comp_eq, Set.Nonempty, and_assoc, support_mul', support_dconv,
-      indicate_nonneg, mu_nonneg, support_indicate, support_mu, NNReal.coe_eq_zero, iff_self_iff,
+      indicate_nonneg, mu_nonneg, support_indicate, support_mu, NNReal.coe_eq_zero, iff_self,
       forall_const, Set.mem_inter_iff, ← coe_sub, mem_coe, support_pow' _ hp₀, hf]
   set A₁ := fun s ↦ B₁ ∩ c p A s
   set A₂ := fun s ↦ B₂ ∩ c p A s
@@ -111,7 +111,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         (2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭_[ℝ] A ○ 𝟭 A) x ^ p * f x) by
     obtain ⟨s, -, hs⟩ := exists_lt_of_sum_lt this
     refine ⟨_, inter_subset_left (s₂ := c p A s), _, inter_subset_left (s₂ := c p A s), ?_⟩
-    simp only [indicate_apply, mem_filter, mem_univ, true_and_iff, boole_mul] at hs
+    simp only [indicate_apply, mem_filter, mem_univ, true_and, boole_mul] at hs
     split_ifs at hs with h; swap
     · simp only [zero_mul, dL2Inner_eq_sum, Function.comp_apply, RCLike.inner_apply,
         RCLike.conj_to_real] at hs
@@ -133,7 +133,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     all_goals exact Nat.cast_le.2 $ card_mono inter_subset_left
   rw [← sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ← sum_mul, mul_right_comm, ← hgB,
     mul_left_comm, ← mul_assoc]
-  simp only [indicate_apply, boole_mul, mem_filter, mem_univ, true_and_iff, ← sum_filter,
+  simp only [indicate_apply, boole_mul, mem_filter, mem_univ, true_and, ← sum_filter,
     mul_lt_mul_right hf, Function.comp_apply]
   by_cases h : ∀ s, g s ≠ 0 → M ^ 2 ≤ g s
   · rw [← sum_filter_ne_zero (s := filter _ _), Finset.filter_comm,
@@ -161,7 +161,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
           := mul_le_mul_of_nonneg_left
             (sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity) hM.le
       _ = _ := ?_
-  · simp only [mem_filter, mem_univ, true_and_iff, Nat.cast_nonneg, and_imp]
+  · simp only [mem_filter, mem_univ, true_and, Nat.cast_nonneg, and_imp]
     exact fun s hsM hs ↦ mul_lt_mul_of_pos_right ((sqrt_lt' hM).2 hsM) $
       sqrt_pos.2 $ (hg _).lt_of_ne' hs
   rw [sum_cast_c, sum_cast_c, sqrt_mul', sqrt_mul', mul_mul_mul_comm (sqrt _), mul_self_sqrt,
diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
index fe965a2f9b..cae9fa5bbc 100644
--- a/LeanAPAP/Physics/Unbalancing.lean
+++ b/LeanAPAP/Physics/Unbalancing.lean
@@ -34,7 +34,7 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : g ○ g = f) (hν : h ○ h = (↑
   have : ∀ x, ∀ yz ∈ univ.filter fun yz : G × G ↦ yz.1 - yz.2 = x,
     conj ((g ○ g) x) ^ k * (h yz.1 * conj (h yz.2)) =
       conj ((g ○ g) (yz.1 - yz.2)) ^ k * (h yz.1 * conj (h yz.2)) := by
-    simp only [mem_filter, mem_univ, true_and_iff]
+    simp only [mem_filter, mem_univ, true_and]
     rintro _ _ rfl
     rfl
   refine (sum_congr rfl fun _ _ ↦ sum_congr rfl $ this _).trans ?_
@@ -121,7 +121,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ = (3 / 4) ^ p * ε ^ p * ∑ i in P \ T, (ν i : ℝ) := by rw [← sum_mul, mul_comm, mul_pow]
       _ ≤ 4⁻¹ * ε ^ p * ∑ i, (ν i : ℝ) := ?_
       _ = 4⁻¹ * ε ^ p := by norm_cast; simp [hν₁]
-    · simp only [mem_sdiff, mem_filter, mem_univ, true_and_iff, not_le, P, T] at hi
+    · simp only [mem_sdiff, mem_filter, mem_univ, true_and, not_le, P, T] at hi
       exact mul_le_mul_of_nonneg_left (pow_le_pow_left hi.1 hi.2.le _) (by positivity)
     · refine mul_le_mul (mul_le_mul_of_nonneg_right (le_trans (pow_le_pow_of_le_one ?_ ?_ hp) ?_)
         ?_) (sum_le_univ_sum_of_nonneg fun i ↦ ?_) ?_ ?_ <;>
diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean
index 54e14192be..771b865f13 100644
--- a/LeanAPAP/Prereqs/AddChar/Basic.lean
+++ b/LeanAPAP/Prereqs/AddChar/Basic.lean
@@ -1,5 +1,5 @@
+import Mathlib.Algebra.BigOperators.Expect
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
-import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Inner.Discrete.Defs
 
 open Finset hiding card
diff --git a/LeanAPAP/Prereqs/Balance.lean b/LeanAPAP/Prereqs/Balance.lean
index c22d984b5b..0e59941f8f 100644
--- a/LeanAPAP/Prereqs/Balance.lean
+++ b/LeanAPAP/Prereqs/Balance.lean
@@ -1,4 +1,4 @@
-import LeanAPAP.Prereqs.Expect.Basic
+import Mathlib.Algebra.BigOperators.Expect
 
 /-!
 # Balancing a function
diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean
index 90e9924fa2..d8ef1f22b6 100644
--- a/LeanAPAP/Prereqs/Convolution/Compact.lean
+++ b/LeanAPAP/Prereqs/Convolution/Compact.lean
@@ -1,4 +1,6 @@
+import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
+import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 
diff --git a/LeanAPAP/Prereqs/Expect/Basic.lean b/LeanAPAP/Prereqs/Expect/Basic.lean
index e06c3cd41c..d90e62e50f 100644
--- a/LeanAPAP/Prereqs/Expect/Basic.lean
+++ b/LeanAPAP/Prereqs/Expect/Basic.lean
@@ -3,14 +3,10 @@ Copyright (c) 2024 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.Algebra.Rat
-import Mathlib.Algebra.BigOperators.GroupWithZero.Action
+import Mathlib.Algebra.BigOperators.Expect
 import Mathlib.Algebra.BigOperators.Pi
-import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Data.Finset.Density
-import Mathlib.Data.Finset.Pointwise.Basic
-import Mathlib.Data.Fintype.BigOperators
 
 /-!
 # Average over a finset
@@ -34,120 +30,15 @@ Connect `Finset.expect` with the expectation over `s` in the probability theory
 
 open Finset Function
 open Fintype (card)
-open scoped Pointwise
+open scoped BigOperators Pointwise
 
 variable {ι κ M N : Type*}
 
-local notation a " /ℚ " q => (q : ℚ≥0)⁻¹ • a
-
-/-- Average of a function over a finset. If the finset is empty, this is equal to zero. -/
-def Finset.expect [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (f : ι → M) : M :=
-  (s.card : ℚ≥0)⁻¹ • ∑ i ∈ s, f i
-
-namespace BigOperators
-open Batteries.ExtendedBinder Lean Meta
-
-/--
-* `𝔼 i ∈ s, f i` is notation for `Finset.expect s f`. It is the expectation of `f i` where `i`
-  ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance).
-* `𝔼 i, f i` is notation for `Finset.expect Finset.univ f`. It is the expectation of `f i` where `i`
-  ranges over the finite domain of `f`.
-* `𝔼 i ∈ s with p i, f i` is notation for `Finset.expect (Finset.filter p s) f`.
-* `𝔼 (i ∈ s) (j ∈ t), f i j` is notation for `Finset.expect (s ×ˢ t) (fun ⟨i, j⟩ ↦ f i j)`.
-
-These support destructuring, for example `𝔼 ⟨i, j⟩ ∈ s ×ˢ t, f i j`.
-
-Notation: `"𝔼" bigOpBinders* ("with" term)? "," term` -/
-scoped syntax (name := bigexpect) "𝔼 " bigOpBinders ("with " term)? ", " term:67 : term
-
-scoped macro_rules (kind := bigexpect)
-  | `(𝔼 $bs:bigOpBinders $[with $p?]?, $v) => do
-    let processed ← processBigOpBinders bs
-    let i ← bigOpBindersPattern processed
-    let s ← bigOpBindersProd processed
-    match p? with
-    | some p => `(Finset.expect (Finset.filter (fun $i ↦ $p) $s) (fun $i ↦ $v))
-    | none => `(Finset.expect $s (fun $i ↦ $v))
-
-open Lean Meta Parser.Term PrettyPrinter.Delaborator SubExpr
-open Batteries.ExtendedBinder
-
-/-- Delaborator for `Finset.expect`. The `pp.piBinderTypes` option controls whether
-to show the domain type when the expect is over `Finset.univ`. -/
-@[scoped delab app.Finset.expect] def delabFinsetExpect : Delab :=
-  whenPPOption getPPNotation <| withOverApp 6 <| do
-  let #[_, _, _, _, s, f] := (← getExpr).getAppArgs | failure
-  guard <| f.isLambda
-  let ppDomain ← getPPOption getPPPiBinderTypes
-  let (i, body) ← withAppArg <| withBindingBodyUnusedName fun i => do
-    return (i, ← delab)
-  if s.isAppOfArity ``Finset.univ 2 then
-    let binder ←
-      if ppDomain then
-        let ty ← withNaryArg 0 delab
-        `(bigOpBinder| $(.mk i):ident : $ty)
-      else
-        `(bigOpBinder| $(.mk i):ident)
-    `(𝔼 $binder:bigOpBinder, $body)
-  else
-    let ss ← withNaryArg 4 <| delab
-    `(𝔼 $(.mk i):ident ∈ $ss, $body)
-
-end BigOperators
-
-open scoped BigOperators
-
 namespace Finset
 section AddCommMonoid
 variable [AddCommMonoid M] [Module ℚ≥0 M] [AddCommMonoid N] [Module ℚ≥0 N] {s t : Finset ι}
   {f g : ι → M} {m : N → M} {p q : ι → Prop} [DecidablePred p] [DecidablePred q]
 
-lemma expect_univ [Fintype ι] : 𝔼 i, f i = (∑ i, f i) /ℚ Fintype.card ι := by
-  rw [expect, card_univ]
-
-@[simp] lemma expect_empty (f : ι → M) : 𝔼 i ∈ ∅, f i = 0 := by simp [expect]
-@[simp] lemma expect_singleton (f : ι → M) (i : ι) : 𝔼 j ∈ {i}, f j = f i := by simp [expect]
-@[simp] lemma expect_const_zero (s : Finset ι) : 𝔼 _i ∈ s, (0 : M) = 0 := by simp [expect]
-
-@[congr]
-lemma expect_congr {t : Finset ι} (hst : s = t) (h : ∀ i ∈ t, f i = g i) :
-    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by rw [expect, expect, sum_congr hst h, hst]
-
-lemma expectWith_congr (hst : s = t) (hpq : ∀ i ∈ t, p i ↔ q i) (h : ∀ i ∈ t, q i → f i = g i) :
-    𝔼 i ∈ s with p i, f i = 𝔼 i ∈ t with q i, g i :=
-  expect_congr (by rw [hst, (filter_inj' ..).2 hpq]) <| by simpa using h
-
-lemma expect_sum_comm (s : Finset ι) (t : Finset κ) (f : ι → κ → M) :
-    𝔼 i ∈ s, ∑ j ∈ t, f i j = ∑ j ∈ t, 𝔼 i ∈ s, f i j := by
-  simpa only [expect, smul_sum] using sum_comm
-
-lemma expect_comm (s : Finset ι) (t : Finset κ) (f : ι → κ → M) :
-    𝔼 i ∈ s, 𝔼 j ∈ t, f i j = 𝔼 j ∈ t, 𝔼 i ∈ s, f i j := by
-  rw [expect, expect, ← expect_sum_comm, ← expect_sum_comm, expect, expect, smul_comm, sum_comm]
-
-lemma expect_eq_zero (h : ∀ i ∈ s, f i = 0) : 𝔼 i ∈ s, f i = 0 :=
-  (expect_congr rfl h).trans s.expect_const_zero
-
-lemma exists_ne_zero_of_expect_ne_zero (h : 𝔼 i ∈ s, f i ≠ 0) : ∃ i ∈ s, f i ≠ 0 := by
-  contrapose! h; exact expect_eq_zero h
-
-lemma expect_add_distrib (s : Finset ι) (f g : ι → M) :
-    𝔼 i ∈ s, (f i + g i) = 𝔼 i ∈ s, f i + 𝔼 i ∈ s, g i := by
-  simp [expect, sum_add_distrib]
-
-lemma expect_add_expect_comm (f₁ f₂ g₁ g₂ : ι → M) :
-    𝔼 i ∈ s, (f₁ i + f₂ i) + 𝔼 i ∈ s, (g₁ i + g₂ i) =
-      𝔼 i ∈ s, (f₁ i + g₁ i) + 𝔼 i ∈ s, (f₂ i + g₂ i) := by
-  simp_rw [expect_add_distrib, add_add_add_comm]
-
-lemma expect_eq_single_of_mem (i : ι) (hi : i ∈ s) (h : ∀ j ∈ s, j ≠ i → f j = 0) :
-    𝔼 i ∈ s, f i = f i /ℚ s.card := by rw [expect, sum_eq_single_of_mem _ hi h]
-
-lemma expect_ite_zero (s : Finset ι) (p : ι → Prop) [DecidablePred p]
-    (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : M) :
-    𝔼 i ∈ s, ite (p i) a 0 = ite (∃ i ∈ s, p i) (a /ℚ s.card) 0 := by
-  split_ifs <;> simp [expect, sum_ite_zero _ _ h, *]
-
 section DecidableEq
 variable [DecidableEq ι]
 
@@ -157,267 +48,30 @@ variable [DecidableEq ι]
   · simp [expect, hst]
   · simp [expect, smul_smul, ← inv_mul_eq_div, hst.card_ne_zero]
 
-@[simp] lemma expect_dite_eq (i : ι) (f : ∀ j, i = j → M) :
-    𝔼 j ∈ s, (if h : i = j then f j h else 0) = if i ∈ s then f i rfl /ℚ s.card else 0 := by
-  split_ifs <;> simp [expect, *]
-
-@[simp] lemma expect_dite_eq' (i : ι) (f : ∀ j, j = i → M) :
-    𝔼 j ∈ s, (if h : j = i then f j h else 0) = if i ∈ s then f i rfl /ℚ s.card else 0 := by
-  split_ifs <;> simp [expect, *]
-
-@[simp] lemma expect_ite_eq (i : ι) (f : ι → M) :
-    𝔼 j ∈ s, (if i = j then f j else 0) = if i ∈ s then f i /ℚ s.card else 0 := by
-  split_ifs <;> simp [expect, *]
-
-@[simp] lemma expect_ite_eq' (i : ι) (f : ι → M) :
-    𝔼 j ∈ s, (if j = i then f j else 0) = if i ∈ s then f i /ℚ s.card else 0 := by
-  split_ifs <;> simp [expect, *]
-
 end DecidableEq
-
-section bij
-variable {t : Finset κ} {g : κ → M}
-
-/-- Reorder an average.
-
-The difference with `Finset.expect_bij'` is that the bijection is specified as a surjective
-injection, rather than by an inverse function.
-
-The difference with `Finset.expect_nbij` is that the bijection is allowed to use membership of the
-domain of the average, rather than being a non-dependent function. -/
-lemma expect_bij (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha))
-    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
-    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
-  simp_rw [expect, card_bij i hi i_inj i_surj, sum_bij i hi i_inj i_surj h]
-
-/-- Reorder an average.
-
-The difference with `Finset.expect_bij` is that the bijection is specified with an inverse, rather
-than as a surjective injection.
-
-The difference with `Finset.expect_nbij'` is that the bijection and its inverse are allowed to use
-membership of the domains of the averages, rather than being non-dependent functions. -/
-lemma expect_bij' (i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t)
-    (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a)
-    (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) (h : ∀ a ha, f a = g (i a ha)) :
-    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
-  simp_rw [expect, card_bij' i j hi hj left_inv right_inv, sum_bij' i j hi hj left_inv right_inv h]
-
-/-- Reorder an average.
-
-The difference with `Finset.expect_nbij'` is that the bijection is specified as a surjective
-injection, rather than by an inverse function.
-
-The difference with `Finset.expect_bij` is that the bijection is a non-dependent function, rather
-than being allowed to use membership of the domain of the average. -/
-lemma expect_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (h : ∀ a ∈ s, f a = g (i a))
-    (i_inj : (s : Set ι).InjOn i) (i_surj : (s : Set ι).SurjOn i t) :
-    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
-  simp_rw [expect, card_nbij i hi i_inj i_surj, sum_nbij i hi i_inj i_surj h]
-
-/-- Reorder an average.
-
-The difference with `Finset.expect_nbij` is that the bijection is specified with an inverse, rather
-than as a surjective injection.
-
-The difference with `Finset.expect_bij'` is that the bijection and its inverse are non-dependent
-functions, rather than being allowed to use membership of the domains of the averages.
-
-The difference with `Finset.expect_equiv` is that bijectivity is only required to hold on the
-domains of the averages, rather than on the entire types. -/
-lemma expect_nbij' (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s)
-    (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a)
-    (h : ∀ a ∈ s, f a = g (i a)) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by
-  simp_rw [expect, card_nbij' i j hi hj left_inv right_inv,
-    sum_nbij' i j hi hj left_inv right_inv h]
-
-/-- `Finset.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in
-most arguments. -/
-lemma expect_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
-    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by simp_rw [expect, card_equiv e hst, sum_equiv e hst hfg]
-
-lemma expect_product (f : ι × κ → M) : 𝔼 x ∈ s ×ˢ t, f x = 𝔼 i ∈ s, 𝔼 j ∈ t, f (i, j) := by
-  simp only [expect, card_product, sum_product, smul_sum, mul_inv, mul_smul, Nat.cast_mul]
-
-lemma expect_product' (f : ι → κ → M) : 𝔼 i ∈ s ×ˢ t, f i.1 i.2 = 𝔼 i ∈ s, 𝔼 j ∈ t, f i j := by
-  simp only [expect, card_product, sum_product', smul_sum, mul_inv, mul_smul, Nat.cast_mul]
-
-@[simp]
-lemma expect_image [DecidableEq ι] {m : κ → ι} (hm : (t : Set κ).InjOn m) :
-    𝔼 i ∈ t.image m, f i = 𝔼 i ∈ t, f (m i) := by
-  simp_rw [expect, card_image_of_injOn hm, sum_image hm]
-
-end bij
-
-@[simp] lemma expect_inv_index [DecidableEq ι] [InvolutiveInv ι] (s : Finset ι) (f : ι → M) :
-    𝔼 i ∈ s⁻¹, f i = 𝔼 i ∈ s, f i⁻¹ := expect_image inv_injective.injOn
-
-@[simp] lemma expect_neg_index [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → M) :
-    𝔼 i ∈ -s, f i = 𝔼 i ∈ s, f (-i) := expect_image neg_injective.injOn
-
-lemma _root_.map_expect {F : Type*} [FunLike F M N] [LinearMapClass F ℚ≥0 M N]
-    (g : F) (f : ι → M) (s : Finset ι) :
-    g (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, g (f i) := by simp only [expect, map_smul, map_natCast, map_sum]
-
-@[simp]
-lemma card_smul_expect (s : Finset ι) (f : ι → M) : s.card • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i := by
-  obtain rfl | hs := s.eq_empty_or_nonempty
-  · simp
-  · rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀]
-    exact mod_cast hs.card_ne_zero
-
-@[simp] lemma _root_.Fintype.card_smul_expect [Fintype ι] (f : ι → M) :
-    Fintype.card ι • 𝔼 i, f i = ∑ i, f i := Finset.card_smul_expect _ _
-
-@[simp] lemma expect_const (hs : s.Nonempty) (a : M) : 𝔼 _i ∈ s, a = a := by
-  rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]
-  exact mod_cast hs.card_ne_zero
-
-lemma smul_expect {G : Type*} [DistribSMul G M] [SMulCommClass G ℚ≥0 M] (a : G)
-    (s : Finset ι) (f : ι → M) : a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i := by
-  simp only [expect, smul_sum, smul_comm]
-
 end AddCommMonoid
 
-section AddCommGroup
-variable [AddCommGroup M] [Module ℚ≥0 M] [Field N] [Module ℚ≥0 N] {s : Finset ι}
-
-lemma expect_sub_distrib (s : Finset ι) (f g : ι → M) :
-    𝔼 i ∈ s, (f i - g i) = 𝔼 i ∈ s, f i - 𝔼 i ∈ s, g i := by
-  simp only [expect, sum_sub_distrib, smul_sub]
-
-@[simp]
-lemma expect_neg_distrib (s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, -f i = -𝔼 i ∈ s, f i := by
-  simp [expect]
-
-end AddCommGroup
-
-section Semiring
-variable [Semiring M] [Module ℚ≥0 M] {s : Finset ι} {f g : ι → M} {m : N → M}
-
-@[simp] lemma card_mul_expect (s : Finset ι) (f : ι → M) :
-    s.card * 𝔼 i ∈ s, f i = ∑ i ∈ s, f i := by rw [← nsmul_eq_mul, card_smul_expect]
-
-@[simp] lemma _root_.Fintype.card_mul_expect [Fintype ι] (f : ι → M) :
-    Fintype.card ι * 𝔼 i, f i = ∑ i, f i := Finset.card_mul_expect _ _
-
-lemma expect_mul [IsScalarTower ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) :
-    (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a := by rw [expect, expect, smul_mul_assoc, sum_mul]
-
-lemma mul_expect [SMulCommClass ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) :
-    a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i := by rw [expect, expect, mul_smul_comm, mul_sum]
-
-lemma expect_mul_expect [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (s : Finset ι)
-    (t : Finset κ) (f : ι → M) (g : κ → M) :
-    (𝔼 i ∈ s, f i) * 𝔼 j ∈ t, g j = 𝔼 i ∈ s, 𝔼 j ∈ t, f i * g j := by
-  simp_rw [expect_mul, mul_expect]
-
-end Semiring
-
-section CommSemiring
-variable [CommSemiring M] [Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M]
-
-lemma expect_pow (s : Finset ι) (f : ι → M) (n : ℕ) :
-    (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun _ : Fin n ↦ s, ∏ i, f (p i) := by
-  classical
-  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
-
-end CommSemiring
-
-section Semifield
-variable [Semifield M] [CharZero M] {s : Finset ι} {f g : ι → M} {m : N → M}
-
-lemma expect_boole_mul [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) :
-    𝔼 j, ite (i = j) (Fintype.card ι : M) 0 * f j = f i := by
-  simp_rw [expect_univ, ite_mul, zero_mul, sum_ite_eq, if_pos (mem_univ _)]
-  rw [← @NNRat.cast_natCast M, ← NNRat.smul_def, inv_smul_smul₀]
-  simp [Fintype.card_ne_zero]
-
-lemma expect_boole_mul' [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) :
-    𝔼 j, ite (j = i) (Fintype.card ι : M) 0 * f j = f i := by
-  simp_rw [@eq_comm _ _ i, expect_boole_mul]
-
-lemma expect_eq_sum_div_card (s : Finset ι) (f : ι → M) :
-    𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / s.card := by
-  rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]
-
-lemma _root_.Fintype.expect_eq_sum_div_card [Fintype ι] (f : ι → M) :
-    𝔼 i, f i = (∑ i, f i) / Fintype.card ι := Finset.expect_eq_sum_div_card _ _
-
-lemma expect_div (s : Finset ι) (f : ι → M) (a : M) : (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a := by
-  simp_rw [div_eq_mul_inv, expect_mul]
-
-end Semifield
-
 @[simp] lemma expect_apply {α : Type*} {π : α → Type*} [∀ a, CommSemiring (π a)]
     [∀ a, Module ℚ≥0 (π a)] (s : Finset ι) (f : ι → ∀ a, π a) (a : α) :
     (𝔼 i ∈ s, f i) a = 𝔼 i ∈ s, f i a := by simp [expect]
 
 end Finset
 
-namespace algebraMap
-variable [Semifield M] [CharZero M] [Semifield N] [CharZero N] [Algebra M N]
-
-@[simp, norm_cast]
-lemma coe_expect (s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : N) :=
-  map_expect (algebraMap _ _) _ _
-
-end algebraMap
-
 namespace Fintype
 variable [Fintype ι] [Fintype κ]
 
 section AddCommMonoid
-variable [AddCommMonoid M] [Module ℚ≥0 M] {f : ι → M}
-
-/-- `Fintype.expect_bijective` is a variant of `Finset.expect_bij` that accepts
-`Function.Bijective`.
-
-See `Function.Bijective.expect_comp` for a version without `h`. -/
-lemma expect_bijective (e : ι → κ) (he : Bijective e) (f : ι → M) (g : κ → M)
-    (h : ∀ i, f i = g (e i)) : 𝔼 i, f i = 𝔼 i, g i :=
-  expect_nbij e (fun _ _ ↦ mem_univ _) (fun i _ ↦ h i) he.injective.injOn <| by
-    simpa using he.surjective.surjOn _
-
-/-- `Fintype.expect_equiv` is a specialization of `Finset.expect_bij` that automatically fills in
-most arguments.
-
-See `Equiv.expect_comp` for a version without `h`. -/
-lemma expect_equiv (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ i, f i = g (e i)) :
-    𝔼 i, f i = 𝔼 i, g i := expect_bijective _ e.bijective f g h
-
-@[simp] lemma expect_const [Nonempty ι] (a : M) : 𝔼 _i : ι, a = a :=
-  Finset.expect_const univ_nonempty _
-
-lemma expect_ite_zero (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j) (a : M) :
-    𝔼 i, ite (p i) a 0 = ite (∃ i, p i) (a /ℚ Fintype.card ι) 0 := by
-  simp [univ.expect_ite_zero p (by simpa using h), card_univ]
-
-variable [DecidableEq ι]
+variable [AddCommMonoid M] [Module ℚ≥0 M] {f : ι → M} [DecidableEq ι]
 
 @[simp] lemma expect_ite_mem (s : Finset ι) (f : ι → M) :
     𝔼 i, (if i ∈ s then f i else 0) = s.dens • 𝔼 i ∈ s, f i := by
   simp [Finset.expect_ite_mem, dens]
 
-lemma expect_dite_eq (i : ι) (f : ∀ j, i = j → M) :
-    𝔼 j, (if h : i = j then f j h else 0) = f i rfl /ℚ card ι := by simp [card_univ]
-
-lemma expect_dite_eq' (i : ι) (f : ∀ j, j = i → M) :
-    𝔼 j, (if h : j = i then f j h else 0) = f i rfl /ℚ card ι := by simp [card_univ]
-
-lemma expect_ite_eq (i : ι) (f : ι → M) :
-    𝔼 j, (if i = j then f j else 0) = f i /ℚ card ι := by simp [card_univ]
-
-lemma expect_ite_eq' (i : ι) (f : ι → M) :
-    𝔼 j, (if j = i then f j else 0) = f i /ℚ card ι := by simp [card_univ]
-
 end AddCommMonoid
 
 section Semiring
 variable [Semiring M] [Module ℚ≥0 M]
 
-@[simp] lemma expect_one [Nonempty ι] : 𝔼 _i : ι, (1 : M) = 1 := expect_const _
-
 lemma expect_mul_expect [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (f : ι → M)
     (g : κ → M) : (𝔼 i, f i) * 𝔼 j, g j = 𝔼 i, 𝔼 j, f i * g j :=
   Finset.expect_mul_expect ..
diff --git a/LeanAPAP/Prereqs/Expect/MeanInequalities.lean b/LeanAPAP/Prereqs/Expect/MeanInequalities.lean
index c22fbe51d5..07069cada6 100644
--- a/LeanAPAP/Prereqs/Expect/MeanInequalities.lean
+++ b/LeanAPAP/Prereqs/Expect/MeanInequalities.lean
@@ -1,5 +1,5 @@
+import Mathlib.Algebra.BigOperators.Expect
 import Mathlib.Analysis.MeanInequalities
-import LeanAPAP.Prereqs.Expect.Basic
 
 open Finset
 open scoped BigOperators
diff --git a/LeanAPAP/Prereqs/Expect/Order.lean b/LeanAPAP/Prereqs/Expect/Order.lean
index b0e002c26a..4c430ccb37 100644
--- a/LeanAPAP/Prereqs/Expect/Order.lean
+++ b/LeanAPAP/Prereqs/Expect/Order.lean
@@ -1,15 +1,9 @@
-import Mathlib.Data.Real.Basic
-import Mathlib.Algebra.Algebra.Rat
-import Mathlib.Algebra.BigOperators.GroupWithZero.Action
-import Mathlib.Algebra.BigOperators.Ring
-import Mathlib.Algebra.CharP.Defs
+import Mathlib.Algebra.BigOperators.Expect
 import Mathlib.Algebra.Module.Rat
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.Module.Rat
-import Mathlib.Data.Finset.Pointwise.Basic
-import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.NNRat.Order
-import LeanAPAP.Prereqs.Expect.Basic
+import Mathlib.Tactic.GCongr
 
 /-!
 # Order properties of the average over a finset
@@ -103,8 +97,9 @@ variable [LinearOrderedCommSemiring R] [ExistsAddOfLE R] [Module ℚ≥0 R] [Pos
 lemma expect_mul_sq_le_sq_mul_sq (s : Finset ι) (f g : ι → R) :
     (𝔼 i ∈ s, f i * g i) ^ 2 ≤ (𝔼 i ∈ s, f i ^ 2) * 𝔼 i ∈ s, g i ^ 2 := by
   simp only [expect, smul_pow, inv_pow, smul_mul_smul_comm, ← sq]
+  have : (0 : ℚ) ≤ (s.card ^ 2 : ℚ)⁻¹ := by positivity
   gcongr
-  exact sum_mul_sq_le_sq_mul_sq ..
+  exact sum_mul_sq_le_sq_mul_sq (R := R) ..
 
 end LinearOrderedCommSemiring
 end Finset
@@ -165,11 +160,11 @@ def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do
     | _, _ => pure .none
   | _ => throwError "not Finset.expect"
 
-example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j ∈ range n, a j^2 := by positivity
-example (a : ULift.{2} ℕ → ℝ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ 𝔼 j ∈ s, a j^2 := by positivity
-example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j : Fin 8, 𝔼 i ∈ range n, (a j^2 + i ^ 2) := by positivity
-example (n : ℕ) (a : ℕ → ℝ) : 0 < 𝔼 j : Fin (n + 1), (a j^2 + 1) := by positivity
-example (a : ℕ → ℝ) : 0 < 𝔼 j ∈ ({1} : Finset ℕ), (a j^2 + 1) := by
+example (n : ℕ) (a : ℕ → ℚ) : 0 ≤ 𝔼 j ∈ range n, a j^2 := by positivity
+example (a : ULift.{2} ℕ → ℚ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ 𝔼 j ∈ s, a j^2 := by positivity
+example (n : ℕ) (a : ℕ → ℚ) : 0 ≤ 𝔼 j : Fin 8, 𝔼 i ∈ range n, (a j^2 + i ^ 2) := by positivity
+example (n : ℕ) (a : ℕ → ℚ) : 0 < 𝔼 j : Fin (n + 1), (a j^2 + 1) := by positivity
+example (a : ℕ → ℚ) : 0 < 𝔼 j ∈ ({1} : Finset ℕ), (a j^2 + 1) := by
   have : Finset.Nonempty {1} := singleton_nonempty 1
   positivity
 
diff --git a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
index bf4dcacaa7..43343ab2f2 100644
--- a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
+++ b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
@@ -1,7 +1,8 @@
 import Mathlib.Algebra.AddTorsor
+import Mathlib.Algebra.BigOperators.Expect
 import Mathlib.Algebra.Star.Conjneg
 import Mathlib.Data.Fintype.Lattice
-import LeanAPAP.Prereqs.Expect.Basic
+import Mathlib.Data.NNRat.Order
 import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 
diff --git a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean
index 762ff2f034..bbc1199109 100644
--- a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean
+++ b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean
@@ -1,8 +1,8 @@
 import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
 import Mathlib.Algebra.BigOperators.Pi
+import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Star.Pi
-import Mathlib.Data.Finset.Pointwise.Basic
 import Mathlib.Data.Fintype.Lattice
 import Mathlib.Data.Nat.Cast.Order.Ring
 
diff --git a/LeanAPAP/Prereqs/Inner/Function.lean b/LeanAPAP/Prereqs/Inner/Function.lean
index ec73d9a684..e6961308d2 100644
--- a/LeanAPAP/Prereqs/Inner/Function.lean
+++ b/LeanAPAP/Prereqs/Inner/Function.lean
@@ -1,4 +1,4 @@
-import LeanAPAP.Prereqs.Expect.Basic
+import Mathlib.Algebra.BigOperators.Expect
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Inner.Discrete.Defs
 
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean
index 8ce3b62686..594984cbdb 100644
--- a/LeanAPAP/Prereqs/LpNorm/Compact.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean
@@ -3,6 +3,7 @@ import Mathlib.Data.Finset.Density
 import Mathlib.Data.Fintype.Order
 import Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
+import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Expect.Order
 import LeanAPAP.Prereqs.Function.Translate
diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
index dda2b05ffb..15bba63610 100644
--- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
@@ -212,8 +212,6 @@ lemma norm_le_dLinftyNorm {i : α} : ‖f i‖ ≤ ‖f‖_[∞] := by
 @[simp] lemma dLpNorm_pos (hp : p ≠ 0) : 0 < ‖f‖_[p] ↔ f ≠ 0 :=
   pos_iff_ne_zero.trans (dLpNorm_eq_zero hp).not
 
-@[gcongr] lemma dLpNorm_mono_right (hpq : p ≤ q) : ‖f‖_[p] ≤ ‖f‖_[q] := sorry
-
 lemma dLpNorm_mono_real {g : α → ℝ} (h : ∀ x, ‖f x‖ ≤ g x) : ‖f‖_[p] ≤ ‖g‖_[p] :=
   nnLpNorm_mono_real .of_discrete h
 
diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
index 651afa53ab..8f80578f18 100644
--- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
+++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
@@ -30,7 +30,7 @@ private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι)
     _ = |(∑ b in B, ∑ i, (f (a i) - f (b i))) / B.card| ^ (m + 1) := by
       simp only [sum_sub_distrib]
       rw [sum_const, sub_div, sum_comm, sum_div, nsmul_eq_mul, card_piFinset, prod_const,
-        card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀]
+        Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀]
       positivity
     _ = |∑ b in B, ∑ i, (f (a i) - f (b i))| ^ (m + 1) / B.card ^ (m + 1) := by
       rw [abs_div, div_pow, Nat.abs_cast]
@@ -174,7 +174,7 @@ private lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) :
       simp only [mul_add, sum_add_distrib, sum_const, nsmul_eq_mul, ← mul_sum]
       rw [← mul_add, ← two_mul, ← mul_assoc 2, ← mul_assoc 2, mul_right_comm 2, ← _root_.pow_succ',
         add_assoc, Nat.sub_add_cancel hm, pow_add, ← mul_pow, ← mul_pow, card_piFinset, prod_const,
-        card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀]
+        Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀]
       norm_num
       positivity
 
diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean
index d42b1b9348..efde1e2939 100644
--- a/LeanAPAP/Prereqs/NNLpNorm.lean
+++ b/LeanAPAP/Prereqs/NNLpNorm.lean
@@ -1,9 +1,9 @@
+import Mathlib.Algebra.BigOperators.Expect
 import Mathlib.Analysis.Normed.Group.Constructions
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Mathlib.Algebra.Order.Module.Rat
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Prereqs.Expect.Basic
 
 open Filter
 open scoped BigOperators ComplexConjugate ENNReal NNReal
diff --git a/LeanAPAP/Prereqs/PointwiseDensity.lean b/LeanAPAP/Prereqs/PointwiseDensity.lean
index aabc07d1ff..dca272e63f 100644
--- a/LeanAPAP/Prereqs/PointwiseDensity.lean
+++ b/LeanAPAP/Prereqs/PointwiseDensity.lean
@@ -1,5 +1,5 @@
+import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.Data.Finset.Density
-import Mathlib.Data.Finset.Pointwise.Basic
 
 open scoped Pointwise
 
diff --git a/lake-manifest.json b/lake-manifest.json
index d4ca8068f8..d556b65b24 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
+   "rev": "2ce0037d487217469a1efeb9ea8196fe15ab9c46",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e5e4f1e9385f5a636cd95f7b5833d9ba7907115c",
+   "rev": "61fb4d1a2a6a4fe4be260ca31c58af1234ff298b",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -61,11 +61,21 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4b83244f3ea8cf1ebc70f68bc5b94691e826c827",
+   "rev": "555be78e7f1df5d448c64e4282ece0dcc21214ff",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,