diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 891ea081e3..3b8e5a853f 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -1,19 +1,10 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
-import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
-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
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Order.Hom.Basic
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
@@ -22,7 +13,6 @@ import LeanAPAP.Prereqs.AddChar.Basic
 import LeanAPAP.Prereqs.AddChar.MeasurableSpace
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Balance.Complex
-import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Bohr.Arc
 import LeanAPAP.Prereqs.Bohr.Basic
 import LeanAPAP.Prereqs.Bohr.Regular
@@ -34,7 +24,6 @@ import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Convolution.Order
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 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/Extras/BSG.lean b/LeanAPAP/Extras/BSG.lean
index 7ede410bd5..b40afd33a8 100644
--- a/LeanAPAP/Extras/BSG.lean
+++ b/LeanAPAP/Extras/BSG.lean
@@ -239,7 +239,7 @@ lemma claim_eight (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < card A) (hB : (0 :
 lemma test_case {E A B : ℕ} {K : ℝ} (hK : 0 < K) (hE : K⁻¹ * (A ^ 2 * B) ≤ E)
     (hA : 0 < A) (hB : 0 < B) :
     A / (Real.sqrt 2 * K) ≤ Real.sqrt 2⁻¹ * (E / (A * B)) := by
-  rw [inv_mul_le_iff hK] at hE
+  rw [inv_mul_le_iff₀ hK] at hE
   rw [mul_div_assoc', div_le_div_iff, ← mul_assoc, ← sq]
   rotate_left
   · positivity
@@ -266,7 +266,7 @@ lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K)
       Real.sqrt_sq (by positivity)] at this
     refine this.trans' ?_
     -- I'd like automation to handle the rest of this
-    rw [inv_mul_le_iff hK] at hE
+    rw [inv_mul_le_iff₀ hK] at hE
     rw [mul_div_assoc', div_le_div_iff, ← mul_assoc, ← sq]
     rotate_left
     · positivity
diff --git a/LeanAPAP/FiniteField.lean b/LeanAPAP/FiniteField.lean
index 74291e03e1..8fe1efaea8 100644
--- a/LeanAPAP/FiniteField.lean
+++ b/LeanAPAP/FiniteField.lean
@@ -1,5 +1,4 @@
 import Mathlib.FieldTheory.Finite.Basic
-import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
 import LeanAPAP.Prereqs.Balance.Complex
 import LeanAPAP.Prereqs.Chang
 import LeanAPAP.Prereqs.Convolution.ThreeAP
@@ -193,7 +192,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
     calc
       (↑(finrank (ZMod q) G - finrank (ZMod q) V) : ℝ)
         ≤ ↑(finrank (ZMod q) G - finrank (ZMod q) W) := by
-        gcongr; exact Submodule.finrank_le_finrank_of_le hWV
+        gcongr; exact Submodule.finrank_mono hWV
       _ ≤ Δ'.card := sorry
       _ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖μ T‖_[1] ^ 2 / ‖μ T‖_[2] ^ 2 / card G)⌉₊ / 2⁻¹ ^ 2⌉₊ := by
         gcongr
@@ -289,7 +288,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
           (2⁻¹ : ℝ) ≤ 2 ^ 15 * 1 * 1 := by norm_num
           _ ≤ 2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ := ?_
         gcongr
-        exact one_le_pow₀ (one_le_inv hε₀ hε₁.le) _
+        exact one_le_pow₀ (one_le_inv hε₀ hε₁.le)
       _ = 2 ^ 17 * 𝓛 γ / ε ^ 3 := by ring
   obtain ⟨A₁, A₂, hA, hA₁, hA₂⟩ : ∃ (A₁ A₂ : Finset G),
       1 - ε / 32 ≤ ∑ x ∈ s q' (ε / 16) univ univ A, (μ A₁ ○ μ A₂) x ∧
@@ -341,7 +340,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
     ap_in_ff' _ (by positivity)
     (calc
       4⁻¹ * (A.dens : ℝ) ^ (2 * q') ≤ 4⁻¹ * 1 := by
-        gcongr; exact pow_le_one _ (by positivity) $ mod_cast A.dens_le_one
+        gcongr; exact pow_le_one₀ (by positivity) $ mod_cast A.dens_le_one
       _ ≤ 2⁻¹ := by norm_num) (by positivity) (by linarith) hA₁ hA₂
   replace hV :=
     calc
@@ -362,7 +361,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
           𝓛 (ε / 32 * (4⁻¹ * α ^ (2 * q'))) ^ 2 * (ε / 32)⁻¹ ^ 2 := hVdim
       _ ≤ 2 ^ 32 * (8 * q' * 𝓛 α) ^ 2 *
           (2 ^ 8 * q' * 𝓛 α / ε) ^ 2 * (ε / 32)⁻¹ ^ 2 := by
-        have : α ^ (2 * q') ≤ 1 := pow_le_one _ hα₀.le hα₁
+        have : α ^ (2 * q') ≤ 1 := pow_le_one₀ hα₀.le hα₁
         have : 4⁻¹ * α ^ (2 * q') ≤ 1 := mul_le_one (by norm_num) (by positivity) ‹_›
         have : ε / 32 * (4⁻¹ * α ^ (2 * q')) ≤ 1 := mul_le_one (by linarith) (by positivity) ‹_›
         have : 0 ≤ log (ε / 32 * (4⁻¹ * α ^ (2 * q')))⁻¹ :=
@@ -526,7 +525,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
     calc
       _ ≤ (1 : ℝ) := mod_cast dens_le_one
       _ < _ := ?_
-    rw [← inv_pos_lt_iff_one_lt_mul, lt_pow_iff_log_lt, ← div_lt_iff]
+    rw [← inv_pos_lt_iff_one_lt_mul, lt_pow_iff_log_lt, ← div_lt_iff₀]
     calc
       log α⁻¹ / log (65 / 64)
         < ⌊log α⁻¹ / log (65 / 64)⌋₊ + 1 := Nat.lt_floor_add_one _
diff --git a/LeanAPAP/Mathlib/Algebra/Order/Group/Unbundled/Basic.lean b/LeanAPAP/Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
deleted file mode 100644
index 6805c47487..0000000000
--- a/LeanAPAP/Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-/-!
-# TODO
-
-Rename `le_mul_inv_iff_mul_le` to `le_mul_inv_iff`
--/
diff --git a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean b/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
deleted file mode 100644
index e598ac7587..0000000000
--- a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
+++ /dev/null
@@ -1,13 +0,0 @@
-import Mathlib.Algebra.Order.GroupWithZero.Unbundled
-
-/-!
-# TODO
-
-Rename `one_le_mul_of_one_le_of_one_le` to `one_le_mul₀`
--/
-
-variable {G₀ : Type*} [GroupWithZero G₀] [PartialOrder G₀] [ZeroLEOneClass G₀] [PosMulReflectLT G₀]
-  {a b : G₀} [PosMulMono G₀]
-
--- TODO: Unify with `le_inv`
-lemma le_inv_comm₀ (ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹ := sorry
diff --git a/LeanAPAP/Mathlib/Algebra/Order/Ring/Basic.lean b/LeanAPAP/Mathlib/Algebra/Order/Ring/Basic.lean
deleted file mode 100644
index d13893bb83..0000000000
--- a/LeanAPAP/Mathlib/Algebra/Order/Ring/Basic.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Mathlib.Algebra.Order.Ring.Basic
-
-alias one_le_pow₀ := one_le_pow_of_one_le
diff --git a/LeanAPAP/Mathlib/Algebra/Star/Rat.lean b/LeanAPAP/Mathlib/Algebra/Star/Rat.lean
deleted file mode 100644
index cb9e712090..0000000000
--- a/LeanAPAP/Mathlib/Algebra/Star/Rat.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-import Mathlib.Algebra.Module.Defs
-import Mathlib.Algebra.Star.Rat
-
-variable {α : Type*}
-
-@[simp] lemma star_nnqsmul [AddCommMonoid α] [Module ℚ≥0 α] [StarAddMonoid α] (q : ℚ≥0) (a : α) :
-    star (q • a) = q • star a := sorry
-
-@[simp] lemma star_qsmul [AddCommGroup α] [Module ℚ α] [StarAddMonoid α] (q : ℚ) (a : α) :
-    star (q • a) = q • star a := sorry
-
-instance StarAddMonoid.toStarModuleNNRat [AddCommMonoid α] [Module ℚ≥0 α] [StarAddMonoid α] :
-    StarModule ℚ≥0 α where star_smul := star_nnqsmul
-
-instance StarAddMonoid.toStarModuleRat [AddCommGroup α] [Module ℚ α] [StarAddMonoid α] :
-    StarModule ℚ α where star_smul := star_qsmul
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/ENNReal/Real.lean b/LeanAPAP/Mathlib/Data/ENNReal/Real.lean
deleted file mode 100644
index f72528d6e4..0000000000
--- a/LeanAPAP/Mathlib/Data/ENNReal/Real.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Mathlib.Data.ENNReal.Real
-
-attribute [norm_cast] ENNReal.ofReal_le_natCast
diff --git a/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean b/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean
deleted file mode 100644
index c34b1cba25..0000000000
--- a/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean
+++ /dev/null
@@ -1,79 +0,0 @@
-import Mathlib.Data.ENNReal.Inv
-import Mathlib.Data.Real.ConjExponents
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
-
-open scoped NNReal
-
-namespace ENNReal
-
-/-- Two nonnegative real exponents `p, q` are conjugate if they are `> 1` and satisfy the equality
-`1/p + 1/q = 1`. This condition shows up in many theorems in analysis, notably related to `L^p`
-norms. -/
-@[mk_iff]
-structure IsConjExponent (p q : ℝ≥0∞) : Prop where
-  inv_add_inv_conj : p⁻¹ + q⁻¹ = 1
-
-/-- The conjugate exponent of `p` is `q = p/(p - 1)`, so that `1/p + 1/q = 1`. -/
-noncomputable def conjExponent (p : ℝ≥0∞) : ℝ≥0∞ := 1 + (p - 1)⁻¹
-
-variable {a b p q : ℝ≥0∞} (h : p.IsConjExponent q)
-
-@[simp, norm_cast] lemma isConjExponent_coe {p q : ℝ≥0} :
-    IsConjExponent p q ↔ p.IsConjExponent q := by
-  simp [NNReal.isConjExponent_iff, isConjExponent_iff]; sorry
-
-alias ⟨_, _root_.NNReal.IsConjExponent.coe_ennreal⟩ := isConjExponent_coe
-
-namespace IsConjExponent
-
-/- Register several non-vanishing results following from the fact that `p` has a conjugate exponent
-`q`: many computations using these exponents require clearing out denominators, which can be done
-with `field_simp` given a proof that these denominators are non-zero, so we record the most usual
-ones. -/
-
-section
-include h
-
-lemma one_le : 1 ≤ p := ENNReal.inv_le_one.1 $ by
-  rw [← add_zero p⁻¹, ← h.inv_add_inv_conj]; gcongr; positivity
-
-lemma pos : 0 < p := zero_lt_one.trans_le h.one_le
-lemma ne_zero : p ≠ 0 := h.pos.ne'
-
-lemma one_sub_inv : 1 - p⁻¹ = q⁻¹ :=
-  ENNReal.sub_eq_of_eq_add_rev' one_ne_top h.inv_add_inv_conj.symm
-
-lemma conj_eq : q = 1 + (p - 1)⁻¹ := sorry
-
-lemma conjExponent_eq : conjExponent p = q := h.conj_eq.symm
-
-lemma mul_eq_add : p * q = p + q := sorry
-
-@[symm]
-protected lemma symm : q.IsConjExponent p where
-  inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj
-
-lemma div_conj_eq_sub_one : p / q = p - 1 := sorry
-
-end
-
-protected lemma inv_inv (hab : a + b = 1) : a⁻¹.IsConjExponent b⁻¹ where
-  inv_add_inv_conj := by simpa only [inv_inv] using hab
-
-lemma inv_one_sub_inv (ha : a ≤ 1) : a⁻¹.IsConjExponent (1 - a)⁻¹ :=
-  .inv_inv <| add_tsub_cancel_of_le ha
-
-lemma one_sub_inv_inv (ha : a ≤ 1) : (1 - a)⁻¹.IsConjExponent a⁻¹ := (inv_one_sub_inv ha).symm
-
-lemma top_one : IsConjExponent ∞ 1 := sorry
-lemma one_top : IsConjExponent 1 ∞ := sorry
-
-end IsConjExponent
-
-lemma isConjExponent_iff_eq_conjExponent (h : 1 < p) : p.IsConjExponent q ↔ q = 1 + (p - 1)⁻¹ :=
-  sorry
-
-protected lemma IsConjExponent.conjExponent (h : 1 < p) : p.IsConjExponent (conjExponent p) :=
-  (isConjExponent_iff_eq_conjExponent h).2 rfl
-
-end ENNReal
diff --git a/LeanAPAP/Mathlib/Order/Hom/Basic.lean b/LeanAPAP/Mathlib/Order/Hom/Basic.lean
deleted file mode 100644
index 18740e95f5..0000000000
--- a/LeanAPAP/Mathlib/Order/Hom/Basic.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Mathlib.Order.Hom.Basic
-
-@[gcongr] protected alias ⟨_, GCongr.orderIso_apply_le_apply⟩ := OrderIso.le_iff_le
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index 2e37f02717..f79d543bad 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
 
@@ -363,7 +362,7 @@ lemma T_bound (hK₂ : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ)
     refine h₂.trans (mul_le_mul_of_nonneg_right hK₂ (Nat.cast_nonneg _))
     exact zero_lt_two
   rw [neg_mul, neg_div, Real.rpow_neg hK.le, mul_left_comm,
-    inv_mul_le_iff (Real.rpow_pos_of_pos hK _)]
+    inv_mul_le_iff₀ (Real.rpow_pos_of_pos hK _)]
   refine (mul_le_mul_of_nonneg_right this (Nat.cast_nonneg _)).trans ?_
   rw [mul_assoc]
   rw [← @Nat.cast_le ℝ, Nat.cast_mul] at h₁
diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean
index 8abc6a92d3..4887087d8a 100644
--- a/LeanAPAP/Physics/DRC.lean
+++ b/LeanAPAP/Physics/DRC.lean
@@ -87,7 +87,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
   set M : ℝ :=
     2 ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p * (sqrt B₁.card * sqrt B₂.card) / A.card ^ p
       with hM_def
-  have hM : 0 < M := by rw [hM_def]; sorry -- positivity
+  have hM : 0 < M := by rw [hM_def]; positivity
   replace hf : 0 < ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by
     have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ * (𝟭 A ○ 𝟭 A) ^ p * (↑) ∘ f :=
       mul_nonneg (mul_nonneg (dconv_nonneg mu_nonneg mu_nonneg) $ pow_nonneg
@@ -148,7 +148,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     refine (le_or_lt_of_add_le_add ?_).resolve_left h.not_le
     simp_rw [← not_le, ← compl_filter, ← two_mul, ← mul_add, sum_compl_add_sum]
     rfl
-  rw [← lt_div_iff' (zero_lt_two' ℝ), div_eq_inv_mul]
+  rw [← lt_div_iff₀' (zero_lt_two' ℝ), div_eq_inv_mul]
   calc
     ∑ s with g s < M ^ 2, g s = ∑ s with g s < M ^ 2 ∧ g s ≠ 0, sqrt (g s) * sqrt (g s)
           := by simp_rw [mul_self_sqrt (hg _), ← filter_filter, sum_filter_ne_zero]
@@ -189,7 +189,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
         c.Nonempty := by
     simp_rw [nonempty_iff_ne_empty]
     rintro c r h rfl
-    simp [pow_mul', (zero_lt_four' ℝ).not_le, inv_mul_le_iff (zero_lt_four' ℝ), mul_assoc,
+    simp [pow_mul', (zero_lt_four' ℝ).not_le, inv_mul_le_iff₀ (zero_lt_four' ℝ), mul_assoc,
       div_nonpos_iff, mul_nonpos_iff, (pow_pos (dLpNorm_conv_pos hp₀.ne' hB hA) 2).not_le] at h
     norm_cast at h
     simp [hp₀, hp₀.ne', hA.ne_empty] at h
@@ -233,7 +233,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
     (1 - ε) ^ p ≤ exp (-ε) ^ p := pow_le_pow_left (sub_nonneg.2 hε₁) (one_sub_le_exp_neg _) _
     _ = exp (-(ε * p)) := by rw [← neg_mul, exp_mul, rpow_natCast]
     _ ≤ exp (-log (2 / δ)) :=
-      (exp_monotone $ neg_le_neg $ (inv_mul_le_iff $ by positivity).1 hpε)
+      (exp_monotone $ neg_le_neg $ (inv_mul_le_iff₀ $ by positivity).1 hpε)
     _ = δ / 2 := by rw [exp_neg, exp_log, inv_div]; positivity
 
 -- TODO: When `1 < ε`, the result is trivial since `S = univ`.
diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
index fb2ea0c628..adf5dda556 100644
--- a/LeanAPAP/Physics/Unbalancing.lean
+++ b/LeanAPAP/Physics/Unbalancing.lean
@@ -1,6 +1,5 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 import LeanAPAP.Prereqs.Inner.Weighted
@@ -105,7 +104,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
   set T := univ.filter fun i ↦ 3 / 4 * ε ≤ f i
   have hTP : T ⊆ P := monotone_filter_right _ fun i ↦ le_trans $ by positivity
   have : 2⁻¹ * ε ^ p ≤ ∑ i in P, ↑(ν i) * (f ^ p) i := by
-    rw [inv_mul_le_iff (zero_lt_two' ℝ), sum_filter]
+    rw [inv_mul_le_iff₀ (zero_lt_two' ℝ), sum_filter]
     convert this using 3
     rw [Pi.posPart_apply, posPart_eq_ite]
     split_ifs <;> simp [pow_sub_one_mul hp₁.pos.ne']
diff --git a/LeanAPAP/Prereqs/Balance/Complex.lean b/LeanAPAP/Prereqs/Balance/Complex.lean
index 18bab88079..e811bde46c 100644
--- a/LeanAPAP/Prereqs/Balance/Complex.lean
+++ b/LeanAPAP/Prereqs/Balance/Complex.lean
@@ -1,8 +1,9 @@
-import LeanAPAP.Prereqs.Balance.Defs
-import LeanAPAP.Prereqs.Expect.Complex
+import Mathlib.Algebra.BigOperators.Balance
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Data.Complex.BigOperators
 
-open Finset
-open scoped BigOperators NNReal
+open Fintype
+open scoped NNReal
 
 namespace Complex
 variable {ι : Type*}
@@ -28,4 +29,3 @@ lemma coe_balance : (↑(balance f a) : 𝕜) = balance ((↑) ∘ f) a := map_b
   simp [balance]
 
 end RCLike
-
diff --git a/LeanAPAP/Prereqs/Balance/Defs.lean b/LeanAPAP/Prereqs/Balance/Defs.lean
deleted file mode 100644
index e08cb14e38..0000000000
--- a/LeanAPAP/Prereqs/Balance/Defs.lean
+++ /dev/null
@@ -1,46 +0,0 @@
-import Mathlib.Algebra.BigOperators.Expect
-
-/-!
-# Balancing a function
--/
-
-open Function
-open Fintype (card)
-open scoped BigOperators Pointwise NNRat
-
-variable {ι α β : Type*}
-
-namespace Finset
-
-section AddCommGroup
-variable [AddCommGroup α] [Module ℚ≥0 α] [Field β] [Module ℚ≥0 β] {s : Finset ι}
-
-variable [Fintype ι]
-
-def balance (f : ι → α) : ι → α := f - Function.const _ (𝔼 y, f y)
-
-lemma balance_apply (f : ι → α) (x : ι) : balance f x = f x - 𝔼 y, f y := rfl
-
-@[simp] lemma balance_zero : balance (0 : ι → α) = 0 := by simp [balance]
-
-@[simp] lemma balance_add (f g : ι → α) : balance (f + g) = balance f + balance g := by
-  simp only [balance, expect_add_distrib, ← const_add, add_sub_add_comm, Pi.add_apply]
-
-@[simp] lemma balance_sub (f g : ι → α) : balance (f - g) = balance f - balance g := by
-  simp only [balance, expect_sub_distrib, const_sub, sub_sub_sub_comm, Pi.sub_apply]
-
-@[simp] lemma balance_neg (f : ι → α) : balance (-f) = -balance f := by
-  simp only [balance, expect_neg_distrib, const_neg, neg_sub', Pi.neg_apply]
-
-@[simp] lemma sum_balance (f : ι → α) : ∑ x, balance f x = 0 := by
-  cases isEmpty_or_nonempty ι <;> simp [balance_apply]
-
-@[simp] lemma expect_balance (f : ι → α) : 𝔼 x, balance f x = 0 := by simp [expect]
-
-@[simp] lemma balance_idem (f : ι → α) : balance (balance f) = balance f := by
-  cases isEmpty_or_nonempty ι <;> ext x <;> simp [balance, expect_sub_distrib]
-
-@[simp] lemma map_balance {F : Type*} [FunLike F α β] [LinearMapClass F ℚ≥0 α β] (g : F) (f : ι → α)
-    (a : ι) : g (balance f a) = balance (g ∘ f) a := by simp [balance, map_expect]
-
-end AddCommGroup
diff --git a/LeanAPAP/Prereqs/Bohr/Basic.lean b/LeanAPAP/Prereqs/Bohr/Basic.lean
index 08b05818d0..5844c931d8 100644
--- a/LeanAPAP/Prereqs/Bohr/Basic.lean
+++ b/LeanAPAP/Prereqs/Bohr/Basic.lean
@@ -116,9 +116,11 @@ lemma mem_chordSet_iff_norm_width : x ∈ B.chordSet ↔ ∀ ⦃ψ⦄, ψ ∈ B.
 @[simp, norm_cast] lemma coeSort_coe (B : BohrSet G) : ↥(B : Set G) = B := rfl
 
 @[simp] lemma zero_mem : 0 ∈ B.chordSet := by simp [mem_chordSet_iff_nnnorm_width]
+
+-- TODO: This lemma needs `Finite G` because we are using `AddChar G ℂ` rather than `AddChar G ℂˣ`
+-- as the dual group.
 @[simp] lemma neg_mem [Finite G] : -x ∈ B.chordSet ↔ x ∈ B.chordSet :=
-  forall₂_congr fun ψ hψ ↦ by sorry
-    -- rw [Iff.comm, ← RCLike.nnnorm_conj, map_sub, map_one, map_neg_eq_conj]
+  forall₂_congr fun ψ hψ ↦ by rw [Iff.comm, ← RCLike.nnnorm_conj, map_sub, map_one, map_neg_eq_conj]
 
 /-! ### Lattice structure -/
 
diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean
index a2f6bcd7f0..f1bc5b3273 100644
--- a/LeanAPAP/Prereqs/Convolution/Compact.lean
+++ b/LeanAPAP/Prereqs/Convolution/Compact.lean
@@ -1,6 +1,5 @@
-import LeanAPAP.Prereqs.Balance.Defs
+import Mathlib.Algebra.BigOperators.Balance
 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/Convolution/Discrete/Basic.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
index f568f958a2..22245f4799 100644
--- a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
+++ b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
@@ -1,6 +1,6 @@
+import Mathlib.Algebra.BigOperators.Balance
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 
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/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
index f306e59cfd..1c371f2bdd 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
@@ -11,8 +11,7 @@ Parseval-Plancherel identity and Fourier inversion formula for it.
 
 noncomputable section
 
-open AddChar Finset Function MeasureTheory RCLike
-open Fintype (card)
+open AddChar Finset Fintype Function MeasureTheory RCLike
 open scoped ComplexConjugate ComplexOrder
 
 variable {α γ : Type*} [AddCommGroup α] [Fintype α] {f : α → ℂ} {ψ : AddChar α ℂ} {n : ℕ}
diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
index 1a7984d5ec..f530b64f15 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
@@ -1,6 +1,6 @@
+import Mathlib.Algebra.BigOperators.Balance
 import LeanAPAP.Prereqs.AddChar.MeasurableSpace
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
-import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Inner.Hoelder.Compact
@@ -12,12 +12,9 @@ This file defines the discrete Fourier transform and shows the Parseval-Plancher
 Fourier inversion formula for it.
 -/
 
-open Fintype (card)
-open AddChar Finset Function MeasureTheory RCLike
+open AddChar Finset Fintype Function MeasureTheory RCLike
 open scoped BigOperators ComplexConjugate ComplexOrder
 
-local notation a " /ℚ " q => (q : ℚ≥0)⁻¹ • a
-
 variable {α γ : Type*} [AddCommGroup α] [Fintype α] {f : α → ℂ} {ψ : AddChar α ℂ} {n : ℕ}
 
 /-- The discrete Fourier transform. -/
diff --git a/LeanAPAP/Prereqs/Inner/Hoelder/Discrete.lean b/LeanAPAP/Prereqs/Inner/Hoelder/Discrete.lean
index 8fc228182f..97c06ca62c 100644
--- a/LeanAPAP/Prereqs/Inner/Hoelder/Discrete.lean
+++ b/LeanAPAP/Prereqs/Inner/Hoelder/Discrete.lean
@@ -1,4 +1,3 @@
-import LeanAPAP.Mathlib.Data.Real.ConjExponents
 import LeanAPAP.Prereqs.Inner.Weighted
 import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 
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/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
index 15bba63610..ebfae0c3ab 100644
--- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
@@ -271,9 +271,7 @@ example {p : ℝ≥0∞} (hp : p ≠ 0) {f : α → ℝ} (hf : 0 < f) : 0 < ‖f
 end NormedAddCommGroup
 
 section Complex
-variable [Fintype α] [DiscreteMeasurableSpace α] {w : α → ℝ≥0} {f : α → ℂ}
-
-open scoped ComplexOrder
+variable [Fintype α] [DiscreteMeasurableSpace α] {f : α → ℂ}
 
 example {p : ℝ≥0∞} (hp : p ≠ 0) (hf : f ≠ 0) : 0 < ‖f‖_[p] := by positivity
 example {p : ℝ≥0∞} (hp : p ≠ 0) {f : α → ℝ} (hf : 0 < f) : 0 < ‖f‖_[p] := by positivity
diff --git a/LeanAPAP/Prereqs/LpNorm/Weighted.lean b/LeanAPAP/Prereqs/LpNorm/Weighted.lean
index cf87533a4f..ab6de63804 100644
--- a/LeanAPAP/Prereqs/LpNorm/Weighted.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Weighted.lean
@@ -49,12 +49,6 @@ variable {K : Type*} [RCLike K]
 
 @[simp] lemma wLpNorm_conj (f : α → K) : ‖conj f‖_[p, w] = ‖f‖_[p, w] := by simp [← wLpNorm_norm]
 
-variable [AddGroup α]
-
-@[simp] lemma wLpNorm_conjneg (f : α → K) : ‖conjneg f‖_[p, w] = ‖f‖_[p, w] := by
-  simp [← wLpNorm_norm]
-  sorry
-
 end RCLike
 
 variable [Fintype α]
@@ -108,7 +102,7 @@ lemma wL1Norm_eq_sum_nnnorm (w : α → ℝ≥0) (f : α → E) : ‖f‖_[1, w]
 lemma wL1Norm_eq_sum_norm (w : α → ℝ≥0) (f : α → E) : ‖f‖_[1, w] = ∑ i, w i • ‖f i‖ := by
   simp [wLpNorm_eq_sum_norm]
 
-@[gcongr] 
+@[gcongr]
 lemma wLpNorm_mono_right (hpq : p ≤ q) (w : α → ℝ≥0) (f : α → E) : ‖f‖_[p, w] ≤ ‖f‖_[q, w] :=
   sorry
 
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/LeanAPAP/Prereqs/Rudin.lean b/LeanAPAP/Prereqs/Rudin.lean
index 8eea7ca725..f21a8e6a60 100644
--- a/LeanAPAP/Prereqs/Rudin.lean
+++ b/LeanAPAP/Prereqs/Rudin.lean
@@ -1,5 +1,6 @@
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
+import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.Randomisation
 
@@ -68,8 +69,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate
     · simp
     specialize H hp ((sqrt p / ‖f‖ₙ_[2]) • f) ?_
     · rwa [cft_smul, support_const_smul_of_ne_zero]
-      sorry
-      -- positivity
+      positivity
     have : 0 < ‖f‖ₙ_[2] := (cLpNorm_pos two_ne_zero).2 hf
     have : 0 < |√ p| := by positivity
     simp_rw [Function.comp_def, Pi.smul_apply, Complex.smul_re, ← Pi.smul_def] at H
diff --git a/lake-manifest.json b/lake-manifest.json
index fb1d2a96d1..d5319ed35d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd",
+   "rev": "f274aed7ae8d1addd3e70adaf3183ccc6e1ed43d",
    "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": "d369bba55fcefeb0d7600e9c2e4856ac9bbece72",
    "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": "ccb4e97ffb7ad0f9b1852e9669d5e2922f984175",
    "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