diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 91646a803f..287f72d05a 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -15,10 +15,10 @@ import LeanAPAP.Mathlib.Algebra.GroupPower.Basic
 import LeanAPAP.Mathlib.Algebra.GroupPower.Hom
 import LeanAPAP.Mathlib.Algebra.GroupPower.Order
 import LeanAPAP.Mathlib.Algebra.Group.TypeTags
+import LeanAPAP.Mathlib.Algebra.ModEq
 import LeanAPAP.Mathlib.Algebra.Module.Basic
 import LeanAPAP.Mathlib.Algebra.Order.LatticeGroup
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Canonical
-import LeanAPAP.Mathlib.Algebra.Order.SMul
 import LeanAPAP.Mathlib.Algebra.Star.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Order
 import LeanAPAP.Mathlib.Algebra.Star.Pi
@@ -26,6 +26,7 @@ import LeanAPAP.Mathlib.Algebra.Star.SelfAdjoint
 import LeanAPAP.Mathlib.Algebra.Support
 import LeanAPAP.Mathlib.Analysis.Complex.Basic
 import LeanAPAP.Mathlib.Analysis.Complex.Circle
+import LeanAPAP.Mathlib.Analysis.Convex.SpecificFunctions.Basic
 import LeanAPAP.Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Mathlib.Analysis.MeanInequalities
 import LeanAPAP.Mathlib.Analysis.MeanInequalitiesPow
@@ -35,6 +36,9 @@ import LeanAPAP.Mathlib.Analysis.NormedSpace.PiLp
 import LeanAPAP.Mathlib.Analysis.NormedSpace.Ray
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
 import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.Complex.Exponential
 import LeanAPAP.Mathlib.Data.Finset.Basic
@@ -77,6 +81,7 @@ import LeanAPAP.Mathlib.Order.Disjoint
 import LeanAPAP.Mathlib.Order.Heyting.Basic
 import LeanAPAP.Mathlib.Order.Partition.Finpartition
 import LeanAPAP.Mathlib.Tactic.Positivity
+import LeanAPAP.Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean
index 0c9dfa2127..4f826d6f27 100644
--- a/LeanAPAP/FiniteField/Basic.lean
+++ b/LeanAPAP/FiniteField/Basic.lean
@@ -33,20 +33,20 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.card / card G) (hγ :
       (abs_l2inner_le_lpNorm_mul_lpNorm ⟨by exact_mod_cast hp, ?_⟩ _ _)
     _ ≤ ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[p] * (card G ^ (-(p : ℝ)⁻¹) * γ ^ (-(p : ℝ)⁻¹)) :=
         mul_le_mul (lpNorm_conv_le_lpNorm_dconv' (by positivity) (even_two_mul _) _) ?_
-          (by sorry) (by sorry) -- positivity
+          (by positivity) (by positivity)
     _ = ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈γ.curlog⌉₊), const _ (card G)⁻¹] *
           γ ^ (-(p : ℝ)⁻¹) := ?_
     _ ≤ _ := mul_le_mul_of_nonneg_left ?_ $ by positivity
   · rw [←balance_conv, balance, l2inner_sub_left, l2inner_const_left, expect_conv, sum_mu ℝ hA,
       expect_mu ℝ hA, sum_mu ℝ hC, conj_trivial, one_mul, mul_one, ←mul_inv_cancel, ←mul_sub,
-      abs_mul, abs_of_nonneg, mul_div_cancel_left] <;> sorry -- positivity
+      abs_mul, abs_of_nonneg, mul_div_cancel_left] <;> positivity
   · rw [NNReal.coe_inv, NNReal.coe_sub hp'.le]
     simp
-  · rw [lpNorm_mu (one_le_inv (tsub_pos_of_lt hp') tsub_le_self) hC, NNReal.coe_inv, NNReal.coe_inv,
+  · rw [lpNorm_mu (one_le_inv (tsub_pos_of_lt hp') tsub_le_self) hC, NNReal.coe_inv,
       NNReal.coe_sub hp'.le, NNReal.coe_one, inv_inv, sub_sub_cancel_left, ←mul_rpow]
     rw [le_div_iff, mul_comm] at hγC
     refine' rpow_le_rpow_of_nonpos _ hγC (neg_nonpos.2 _)
-    all_goals sorry -- positivity
+    all_goals positivity
   · simp_rw [Nat.cast_mul, Nat.cast_two]
     rw [wlpNorm_const_right, mul_assoc, mul_left_comm, NNReal.coe_inv, inv_rpow, rpow_neg]
     push_cast
@@ -87,7 +87,7 @@ lemma di_in_ff (hε₀ : 0 < ε) (hε₁ : ε < 1) (hαA : α ≤ A.card / card
       Finset.card_empty, zero_div] at hαA ⊢
     exact ⟨by positivity, mul_nonpos_of_nonneg_of_nonpos (by positivity) hαA⟩
   have hγ₁ : γ ≤ 1 := hγC.trans (div_le_one_of_le (Nat.cast_le.2 C.card_le_univ) $ by positivity)
-  have hG : (card G : ℝ) ≠ 0 := by sorry -- positivity
+  have hG : (card G : ℝ) ≠ 0 := by positivity
   have := unbalancing _ (mul_ne_zero two_ne_zero (Nat.ceil_pos.2 $ curlog_pos hγ hγ₁).ne') (ε / 2)
     (by positivity) (div_le_one_of_le (hε₁.le.trans $ by norm_num) $ by norm_num)
     (const _ (card G)⁻¹) (card G • (balance (μ A) ○ balance (μ A)))
diff --git a/LeanAPAP/Mathlib/Algebra/BigOperators/Expect.lean b/LeanAPAP/Mathlib/Algebra/BigOperators/Expect.lean
index c8d13e3004..9ba981a059 100644
--- a/LeanAPAP/Mathlib/Algebra/BigOperators/Expect.lean
+++ b/LeanAPAP/Mathlib/Algebra/BigOperators/Expect.lean
@@ -308,39 +308,34 @@ open Finset
 namespace Mathlib.Meta.Positivity
 open Qq Lean Meta
 
--- TODO: This doesn't handle universe-polymorphic input
 @[positivity Finset.expect _ _]
-def evalExpect : PositivityExt where eval {u β2} zβ pβ e := do
-  let .app (.app (.app (.app (.app (.const _ [_, v]) (α : Q(Type v))) (β : Q(Type u)))
-    (_a : Q(Semifield $β))) (s : Q(Finset $α))) (b : Q($α → $β)) ← withReducible (whnf e)
-      | throwError "not `Finset.expect`"
-  haveI' : $β =Q $β2 := ⟨⟩
-  haveI' : $e =Q Finset.expect $s $b := ⟨⟩
-  let (lhs, _, (rhs : Q($β))) ← lambdaMetaTelescope b
-  let rb ← core zβ pβ rhs
-
-  let so : Option Q(Finset.Nonempty $s) ← do -- TODO: if I make a typo it doesn't complain?
-    try {
-      let _fi ← synthInstanceQ (q(Fintype $α) : Q(Type v))
-      let _no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
-      match s with
-      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
-      | _ => pure none }
-    catch _e => do
-      let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
-      pure (some (.fvar fv))
-  match rb, so with
-  | .nonnegative pb, _ => do
-    let pα' ← synthInstanceQ (q(LinearOrderedSemifield $β) : Q(Type u))
-    assertInstancesCommute
-    let pr : Q(∀ (i : $α), 0 ≤ $b i) ← mkLambdaFVars lhs pb
-    pure (.nonnegative q(@expect_nonneg.{u, v} $α $β $pα' $s $b (fun i _h => $pr i)))
-  | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
-    let pα' ← synthInstanceQ (q(LinearOrderedSemifield $β) : Q(Type u))
-    assertInstancesCommute
-    let pr : Q(∀ (i : $α), 0 < $b i) ← mkLambdaFVars lhs pb
-    pure (.positive q(@expect_pos.{u, v} $α $β $pα' $s $b (fun i _h => $pr i) $fi))
-  | _, _ => pure .none
+def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do
+  match e with
+  | ~q(@Finset.expect $ι _ $instα $s $f) =>
+    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f
+    let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo?
+      try {
+        let _fi ← synthInstanceQ q(Fintype $ι)
+        let _no ← synthInstanceQ q(Nonempty $ι)
+        match s with
+        | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι)))
+        | _ => pure none
+      } catch _ => do
+        let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
+        pure (some (.fvar fv))
+    match ← core zα pα rhs, so with
+    | .nonnegative pb, _ => do
+      let instα' ← synthInstanceQ q(LinearOrderedSemifield $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
+      pure (.nonnegative q(@expect_nonneg $ι $α $instα' $s $f fun i _ ↦ $pr i))
+    | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
+      let instα' ← synthInstanceQ q(LinearOrderedSemifield $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
+      pure (.positive q(@expect_pos $ι $α $instα' $s $f (fun i _ ↦ $pr i) $fi))
+    | _, _ => 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
diff --git a/LeanAPAP/Mathlib/Algebra/BigOperators/Order.lean b/LeanAPAP/Mathlib/Algebra/BigOperators/Order.lean
index 50aea90f4e..77d788fdf7 100644
--- a/LeanAPAP/Mathlib/Algebra/BigOperators/Order.lean
+++ b/LeanAPAP/Mathlib/Algebra/BigOperators/Order.lean
@@ -23,43 +23,38 @@ lemma sum_mul_sq_le_sq_mul_sq (s : Finset α) (f g : α → 𝕜) :
 
 end Finset
 
-open Finset
-open scoped BigOperators
-open Qq Lean Meta
 
--- TODO: This doesn't handle universe-polymorphic input
-@[positivity Finset.sum _ _]
-def Mathlib.Meta.Positivity.evalFinsetSum : PositivityExt where eval {u β2} zβ pβ e := do
-  let .app (.app (.app (.app (.app (.const _ [_, v]) (β : Q(Type u))) (α : Q(Type v)))
-    (_a : Q(AddCommMonoid $β))) (s : Q(Finset $α))) (b : Q($α → $β)) ← withReducible (whnf e)
-      | throwError "not `Finset.sum`"
-  haveI' : $β =Q $β2 := ⟨⟩
-  haveI' : $e =Q Finset.sum $s $b := ⟨⟩
-  let (lhs, _, (rhs : Q($β))) ← lambdaMetaTelescope b
-  let rb ← core zβ pβ rhs
+namespace Mathlib.Meta.Positivity
+open Qq Lean Meta Finset
 
-  let so : Option Q(Finset.Nonempty $s) ← do -- TODO: if I make a typo it doesn't complain?
-    try {
-      let _fi ← synthInstanceQ (q(Fintype $α) : Q(Type v))
-      let _no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
-      match s with
-      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
-      | _ => pure none }
-    catch _e => do
-      let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
-      pure (some (.fvar fv))
-  match rb, so with
-  | .nonnegative pb, _ => do
-    let pα' ← synthInstanceQ (q(OrderedAddCommMonoid $β) : Q(Type u))
-    assertInstancesCommute
-    let pr : Q(∀ (i : $α), 0 ≤ $b i) ← mkLambdaFVars lhs pb
-    pure (.nonnegative q(@sum_nonneg.{u, v} $α $β $pα' $b $s (fun i _h => $pr i)))
-  | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
-    let pα' ← synthInstanceQ (q(OrderedCancelAddCommMonoid $β) : Q(Type u))
-    assertInstancesCommute
-    let pr : Q(∀ (i : $α), 0 < $b i) ← mkLambdaFVars lhs pb
-    pure (.positive q(@sum_pos.{u, v} $α $β $pα' $b $s (fun i _h => $pr i) $fi))
-  | _, _ => pure .none
+@[positivity Finset.sum _ _]
+def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do
+  match e with
+  | ~q(@Finset.sum _ $ι $instα $s $f) =>
+    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f
+    let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo?
+      try {
+        let _fi ← synthInstanceQ q(Fintype $ι)
+        let _no ← synthInstanceQ q(Nonempty $ι)
+        match s with
+        | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι)))
+        | _ => pure none
+      } catch _ => do
+        let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
+        pure (some (.fvar fv))
+    match ← core zα pα rhs, so with
+    | .nonnegative pb, _ => do
+      let pα' ← synthInstanceQ q(OrderedAddCommMonoid $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
+      pure (.nonnegative q(@sum_nonneg $ι $α $pα' $f $s fun i _ ↦ $pr i))
+    | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
+      let pα' ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
+      assertInstancesCommute
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
+      pure (.positive q(@sum_pos $ι $α $pα' $f $s (fun i _ ↦ $pr i) $fi))
+    | _, _ => pure .none
+  | _ => throwError "not Finset.sum"
 
 example (n : ℕ) (a : ℕ → ℤ) : 0 ≤ ∑ j in range n, a j^2 := by positivity
 example (a : ULift.{2} ℕ → ℤ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ ∑ j in s, a j^2 := by positivity
diff --git a/LeanAPAP/Mathlib/Algebra/Order/SMul.lean b/LeanAPAP/Mathlib/Algebra/Order/SMul.lean
deleted file mode 100644
index a28488bb9e..0000000000
--- a/LeanAPAP/Mathlib/Algebra/Order/SMul.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-import Mathlib.Algebra.Order.SMul
-
-namespace Mathlib.Meta.Positivity
-open Lean Meta Qq Function
-
--- /-- The `positivity` extension which identifies expressions of the form `a • b`,
--- such that `positivity` successfully recognises both `a` and `b`. -/
--- @[positivity _ • _, SMul.smul _ _] def evalSMul : PositivityExt where eval {u α} zα pα e := do
---   let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
---     | throwError "not •"
---   let _e_eq : $e =Q $f $a $b := ⟨⟩
---   let _a ← synthInstanceQ q(StrictOrderedSemiring $α)
---   assumeInstancesCommute
---   let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ (u := u.succ) f q(HMul.hMul)
---   let ra ← core zα pα a; let rb ← core zα pα b
---   match ra, rb with
---   | .positive pa, .positive pb => pure (.positive q(mul_pos $pa $pb))
---   | .positive pa, .nonnegative pb => pure (.nonnegative q(mul_nonneg_of_pos_of_nonneg $pa $pb))
---   | .nonnegative pa, .positive pb => pure (.nonnegative q(mul_nonneg_of_nonneg_of_pos $pa $pb))
---   | .nonnegative pa, .nonnegative pb => pure (.nonnegative q(mul_nonneg $pa $pb))
---   | .positive pa, .nonzero pb =>
---     let _a ← synthInstanceQ (q(NoZeroDivisors $α) : Q(Prop))
---     pure (.nonzero q(mul_ne_zero_of_pos_of_ne_zero $pa $pb))
---   | .nonzero pa, .positive pb =>
---     let _a ← synthInstanceQ (q(NoZeroDivisors $α) : Q(Prop))
---     pure (.nonzero q(mul_ne_zero_of_ne_zero_of_pos $pa $pb))
---   | .nonzero pa, .nonzero pb =>
---     let _a ← synthInstanceQ (q(NoZeroDivisors $α) : Q(Prop))
---     pure (.nonzero (q(mul_ne_zero $pa $pb)))
---   | _, _ => pure .none
-
--- example {a : ℤ} {b : ℚ} (ha : 0 < a) (hb : 0 < b) : 0 < a • b := by positivity
--- example {a : ℤ} {b : ℚ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a • b := by positivity
--- example {a : ℤ} {b : ℚ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a • b := by positivity
--- example {a : ℤ} {b : ℚ} (ha : 0 < a) (hb : b ≠ 0) : a • b ≠ 0 := by positivity
--- example {a : ℤ} {b : ℚ} (ha : a ≠ 0) (hb : 0 < b) : a • b ≠ 0 := by positivity
--- example {a : ℤ} {b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : a • b ≠ 0 := by positivity
-
-end Mathlib.Meta.Positivity
diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
index ba1af9bc0c..b164446460 100644
--- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
+++ b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
@@ -19,21 +19,20 @@ private alias ⟨_, sinh_ne_zero_of_ne_zero⟩ := Real.sinh_ne_zero
 /-- Extension for the `positivity` tactic: `Real.sinh` is positive/nonnegative/nonzero if its input
 is. -/
 @[positivity Real.sinh _]
-def evalSinh : PositivityExt where eval zα pα e := do
-  let (.app f (a : Q(ℝ))) ← withReducible (whnf e) | throwError "not Real.sinh"
-  guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(Real.sinh)
-  let ra ← core zα pα a
-  match ra with
-  | .positive pa =>
-      have pa' : Q(0 < $a) := pa
-      return .positive (q(sinh_pos_of_pos $pa') : Expr)
-  | .nonnegative pa =>
-      have pa' : Q(0 ≤ $a) := pa
-      return .nonnegative (q(sinh_nonneg_of_nonneg $pa') : Expr)
-  | .nonzero pa =>
-      have pa' : Q($a ≠ 0) := pa
-      return .nonzero (q(sinh_ne_zero_of_ne_zero $pa') : Expr)
-  | _ => return .none
+def evalSinh : PositivityExt where eval {u α} _ _ e := do
+  let zα : Q(Zero ℝ) := q(inferInstance)
+  let pα : Q(PartialOrder ℝ) := q(inferInstance)
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℝ), ~q(Real.sinh $a) =>
+      assumeInstancesCommute
+      match ← core zα pα a with
+      | .positive pa => return .positive q(sinh_pos_of_pos $pa)
+      | .nonnegative pa => return .nonnegative q(sinh_nonneg_of_nonneg $pa)
+      | .nonzero pa => return .nonzero q(sinh_ne_zero_of_ne_zero $pa)
+      | _ => return .none
+    | _, _ => throwError "not Real.sinh"
+  else throwError "not Real.sinh"
 
 example (x : ℝ) (hx : 0 < x) : 0 < x.sinh := by positivity
 example (x : ℝ) (hx : 0 ≤ x) : 0 ≤ x.sinh := by positivity
diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean
new file mode 100644
index 0000000000..4bda4041bb
--- /dev/null
+++ b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean
@@ -0,0 +1,48 @@
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
+import LeanAPAP.Mathlib.Data.Nat.Factorial.Basic
+
+open NormedSpace
+open scoped Nat
+
+namespace Complex
+
+/-- The power series expansion of `Complex.cosh`. -/
+lemma hasSum_cosh (z : ℂ) : HasSum (fun n ↦ z ^ (2 * n) / ↑(2 * n)!) (cosh z) := by
+  simpa [mul_assoc, cos_mul_I] using hasSum_cos' (z * I)
+
+/-- The power series expansion of `Complex.sinh`. -/
+lemma hasSum_sinh (z : ℂ) : HasSum (fun n ↦ z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sinh z) := by
+  simpa [mul_assoc, sin_mul_I, neg_pow z, pow_add, pow_mul, neg_mul, neg_div]
+    using (hasSum_sin' (z * I)).mul_right (-I)
+
+lemma cosh_eq_tsum (z : ℂ) : cosh z = ∑' n, z ^ (2 * n) / ↑(2 * n)! := z.hasSum_cosh.tsum_eq.symm
+
+lemma sinh_eq_tsum (z : ℂ) : sinh z = ∑' n, z ^ (2 * n + 1) / ↑(2 * n + 1)! :=
+  z.hasSum_sinh.tsum_eq.symm
+
+end Complex
+
+namespace Real
+
+/-- The power series expansion of `Real.cosh`. -/
+lemma hasSum_cosh (r : ℝ) : HasSum (fun n  ↦ r ^ (2 * n) / ↑(2 * n)!) (cosh r) :=
+  mod_cast Complex.hasSum_cosh r
+
+/-- The power series expansion of `Real.sinh`. -/
+lemma hasSum_sinh (r : ℝ) : HasSum (fun n ↦ r ^ (2 * n + 1) / ↑(2 * n + 1)!) (sinh r) :=
+  mod_cast Complex.hasSum_sinh r
+
+lemma cosh_eq_tsum (r : ℝ) : cosh r = ∑' n, r ^ (2 * n) / ↑(2 * n)! := r.hasSum_cosh.tsum_eq.symm
+
+lemma sinh_eq_tsum (r : ℝ) : sinh r = ∑' n, r ^ (2 * n + 1) / ↑(2 * n + 1)! :=
+  r.hasSum_sinh.tsum_eq.symm
+
+lemma cosh_le_exp_half_sq (x : ℝ) : cosh x ≤ exp (x ^ 2 / 2) := by
+  rw [cosh_eq_tsum, exp_eq_exp_ℝ, exp_eq_tsum]
+  refine tsum_le_tsum (fun i ↦ ?_) x.hasSum_cosh.summable $ expSeries_summable' (x ^ 2 / 2)
+  simp only [div_pow, pow_mul, smul_eq_mul, inv_mul_eq_div, div_div]
+  gcongr
+  norm_cast
+  exact Nat.two_pow_mul_factorial_le_factorial_two_mul
+
+end Real
diff --git a/LeanAPAP/Mathlib/Data/Complex/Exponential.lean b/LeanAPAP/Mathlib/Data/Complex/Exponential.lean
index 2edd643db1..454744260f 100644
--- a/LeanAPAP/Mathlib/Data/Complex/Exponential.lean
+++ b/LeanAPAP/Mathlib/Data/Complex/Exponential.lean
@@ -22,6 +22,11 @@ lemma one_sub_le_exp_neg (x : ℝ) : 1 - x ≤ exp (-x) :=
 lemma one_sub_lt_exp_neg (hx : x ≠ 0) : 1 - x < exp (-x) :=
   (sub_eq_neg_add _ _).trans_lt $ add_one_lt_exp $ neg_ne_zero.2 hx
 
+lemma exp_nonneg (x : ℝ) : 0 ≤ exp x := x.exp_pos.le
+
+lemma exp_abs_le (x : ℝ) : exp |x| ≤ exp x + exp (-x) := by
+  cases le_total x 0 <;> simp [abs_of_nonpos, abs_of_nonneg, exp_nonneg, *]
+
 lemma pow_div_factorial_le_exp (hx : 0 ≤ x) (n : ℕ) : x ^ n / n ! ≤ exp x :=
   calc
     x ^ n / n ! ≤ ∑ k in range (n + 1), x ^ k / k !
@@ -31,12 +36,19 @@ lemma pow_div_factorial_le_exp (hx : 0 ≤ x) (n : ℕ) : x ^ n / n ! ≤ exp x
 end Real
 
 namespace Mathlib.Meta.Positivity
-open Lean.Meta Qq
+open Lean Meta Qq
 
 /-- Extension for the `positivity` tactic: `Real.cosh` is always positive. -/
 @[positivity Real.cosh _]
-def evalCosh : PositivityExt where eval _ _ e := do
-  let (.app _ (a : Q(ℝ))) ← withReducible (whnf e) | throwError "not Real.cosh"
-  pure (.positive (q(Real.cosh_pos $a) : Lean.Expr))
+def evalCosh : PositivityExt where eval {u α} _ _ e := do
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℝ), ~q(Real.cosh $a) =>
+      assumeInstancesCommute
+      return .positive q(Real.cosh_pos $a)
+    | _, _ => throwError "not Real.cosh"
+  else throwError "not Real.cosh"
+
+example (x : ℝ) : 0 < x.cosh := by positivity
 
 end Mathlib.Meta.Positivity
diff --git a/LeanAPAP/Mathlib/Data/Nat/Factorial/Basic.lean b/LeanAPAP/Mathlib/Data/Nat/Factorial/Basic.lean
index fb664a7275..10063f2663 100644
--- a/LeanAPAP/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/LeanAPAP/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -9,4 +9,12 @@ lemma factorial_two_mul_le : (2 * n)! ≤ (2 * n) ^ n * n ! := by
   rw [two_mul, ←factorial_mul_ascFactorial, mul_comm]
   exact mul_le_mul_right' (ascFactorial_le_pow_add _ _) _
 
+lemma two_pow_mul_factorial_le_factorial_two_mul : 2 ^ n * n ! ≤ (2 * n) ! := by
+  obtain _ | n := n
+  · simp
+  rw [mul_comm, two_mul]
+  calc
+    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) := mul_le_mul_left' (pow_le_pow_of_le_left le_add_self _) _
+    _ ≤ _ := Nat.factorial_mul_pow_le_factorial
+
 end Nat
diff --git a/LeanAPAP/Mathlib/Data/Rat/Order.lean b/LeanAPAP/Mathlib/Data/Rat/Order.lean
index a8bbc6b4ac..f86da967af 100644
--- a/LeanAPAP/Mathlib/Data/Rat/Order.lean
+++ b/LeanAPAP/Mathlib/Data/Rat/Order.lean
@@ -21,26 +21,30 @@ private alias ⟨_, num_ne_zero_of_ne_zero⟩ := num_ne_zero
 /-- The `positivity` extension which identifies expressions of the form `Rat.num a`,
 such that `positivity` successfully recognises `a`. -/
 @[positivity Rat.num _]
-def evalRatnum : PositivityExt where eval _zα _pα (e : Q(ℤ)) := do
-  let ~q(Rat.num $a) := e | throwError "not Rat.num"
-  let zα' : Q(Zero ℚ) := q(inferInstance)
-  let pα' : Q(PartialOrder ℚ) := q(inferInstance)
-  -- TODO: what's the right way to write these `: Expr`s?
-  match ← core zα' pα' a with
-  | .positive pa =>
-    return .positive (q(num_pos_of_pos $pa) : Expr)
-  | .nonnegative pa =>
-    return .nonnegative (q(num_nonneg_of_nonneg $pa) : Expr)
-  | .nonzero pa =>
-    return .nonzero (q(num_ne_zero_of_ne_zero $pa) : Expr)
-  | .none =>
-    return .none
+def evalRatnum : PositivityExt where eval {u α} _ _ e := do
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℤ), ~q(Rat.num $a) =>
+      let pα : Q(PartialOrder ℚ) := q(inferInstance)
+      assumeInstancesCommute
+      match ← core (q(inferInstance)) pα a with
+      | .positive pa => return .positive q(num_pos_of_pos $pa)
+      | .nonnegative pa => return .nonnegative q(num_nonneg_of_nonneg $pa)
+      | .nonzero pa => return .nonzero q(num_ne_zero_of_ne_zero $pa)
+      | .none => return .none
+    | _, _ => throwError "not Rat.num"
+  else throwError "not Rat.num"
 
 /-- The `positivity` extension which identifies expressions of the form `Rat.den a`. -/
 @[positivity Rat.den _]
-def evalRatden : PositivityExt where eval _zα _pα (e : Q(ℕ)) := do
-  let ~q(Rat.den $a) := e | throwError "not Rat.den"
-  return .positive (q(den_pos $a) :)
+def evalRatden : PositivityExt where eval {u α} _ _ e := do
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℕ), ~q(Rat.den $a) =>
+      assumeInstancesCommute
+      return .positive q(den_pos $a)
+    | _, _ => throwError "not Rat.num"
+  else throwError "not Rat.num"
 
 variable {q : ℚ}
 
diff --git a/LeanAPAP/Mathlib/Tactic/Positivity/Finset.lean b/LeanAPAP/Mathlib/Tactic/Positivity/Finset.lean
index 1d70b3f9f4..cbc288dffb 100644
--- a/LeanAPAP/Mathlib/Tactic/Positivity/Finset.lean
+++ b/LeanAPAP/Mathlib/Tactic/Positivity/Finset.lean
@@ -6,31 +6,37 @@ namespace Mathlib.Meta.Positivity
 open Qq Lean Meta
 
 @[positivity Finset.card _]
-def evalFinsetCard : PositivityExt where eval _ _ e := do
-  let ⟨v, _l, _r⟩ ← inferTypeQ' <| (Expr.getAppArgs (← withReducible (whnf e))).get! 1
-  let .app (.app _f (α : Q(Type v))) (s : Q(Finset $α)) ← withReducible (whnf e) | throwError "not `Finset.card`"
-
-  let so : Option Q(Finset.Nonempty $s) ← do -- TODO: if I make a typo it doesn't complain?
-    try {
-      let _fi ← synthInstanceQ (q(Fintype $α) : Q(Type v))
-      let _no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
-      match s with
-      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
-      | _ => pure none }
-    catch _e => do
-      let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
-      pure (some (.fvar fv))
-  match so with
-  | .some (fi : Q(Finset.Nonempty $s)) => do
-    return .positive (q(@Finset.Nonempty.card_pos.{v} $α $s $fi) : Q(0 < Finset.card $s))
-  | _ => pure .none
+def evalFinsetCard : PositivityExt where eval {u α} _ _ e := do
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℕ), ~q(@Finset.card $β $s) =>
+      let so : Option Q(Finset.Nonempty $s) ← do -- TODO: if I make a typo it doesn't complain?
+        try {
+          let _fi ← synthInstanceQ q(Fintype $β)
+          let _no ← synthInstanceQ q(Nonempty $β)
+          match s with
+          | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $β)))
+          | _ => pure none }
+        catch _e => do
+          let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
+          pure (some (.fvar fv))
+      assumeInstancesCommute
+      match so with
+      | .some (fi : Q(Finset.Nonempty $s)) => return .positive q(Finset.Nonempty.card_pos $fi)
+      | _ => return .none
+    | _, _ => throwError "not Finset.card"
+  else throwError "not Finset.card"
 
 @[positivity Fintype.card _]
-def evalFintypeCard : PositivityExt where eval _ _ e := do
-  let .app (.app (.const _ [u]) (α : Q(Type u))) (fi : Q(Fintype $α)) ← withReducible (whnf e)
-    | throwError "not `Fintype.card`"
-  let no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
-  pure (.positive (q(@Fintype.card_pos.{u} $α $fi $no) : Q(0 < Fintype.card $α)))
+def evalFintypeCard : PositivityExt where eval {u α} _ _ e := do
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℕ), ~q(@Fintype.card $β $instβ) =>
+      let instβno ← synthInstanceQ (q(Nonempty $β) : Q(Prop))
+      assumeInstancesCommute
+      return .positive q(@Fintype.card_pos $β $instβ $instβno)
+    | _, _ => throwError "not Fintype.card"
+  else throwError "not Fintype.card"
 
 example {α : Type*} {s : Finset α} (hs : s.Nonempty) : 0 < s.card := by positivity
 example {α : Type*} [Fintype α] [Nonempty α] : 0 < (univ : Finset α).card := by positivity
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index 869900fe12..62212d4915 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -103,11 +103,7 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
       1 / 2 * (k * ε * ‖f‖_[2 * m]) ^ (2 * m) * A.card ^ k) :
     (A.card ^ k : ℝ) / 2 ≤ (l k m ε f A).card := by
   rw [←Nat.cast_pow, ←Fintype.card_piFinsetConst] at h
-  have := my_other_markov ?_ (by norm_num) ?_ h
-  rotate_left
-  · sorry -- positivity
-  · intro a ha
-    sorry -- positivity
+  have := my_other_markov (by positivity) (by norm_num) (fun _ _ ↦ by positivity) h
   norm_num1 at this
   rw [Fintype.card_piFinsetConst, mul_comm, mul_one_div, Nat.cast_pow] at this
   refine' this.trans_eq _
@@ -116,7 +112,6 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
   refine' (@strictMonoOn_pow ℝ _ _ _).le_iff_le _ _
   any_goals rw [Set.mem_Ici]
   any_goals positivity
-  all_goals sorry -- positivity
 
 lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
     ∑ a in Fintype.piFinset fun _ : Fin k ↦ A, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤
@@ -141,16 +136,9 @@ lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) :
         ∑ a in Fintype.piFinset fun _ : Fin k ↦ A, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by
   -- lots of the equalities about m can be automated but it's *way* slower
   have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two]
-  have hm' : 1 < 2 * m := by
-    refine' (Nat.mul_le_mul_left 2 hm).trans_lt' _
-    norm_num1
-  have hm'' : (1 : ℝ≥0∞) ≤ 2 * m := by
-    rw [←hmeq, Nat.one_le_cast]
-    exact hm'.le
-  refine' mul_le_mul_of_nonneg_left _ (by sorry) -- positivity
-  refine' sum_le_sum fun a ha ↦ _
-  refine' sum_le_sum fun i hi ↦ _
-  refine' pow_le_pow_of_le_left (by sorry) _ _ -- positivity
+  have hm' : 1 < 2 * m := (Nat.mul_le_mul_left 2 hm).trans_lt' $ by norm_num1
+  have hm'' : (1 : ℝ≥0∞) ≤ 2 * m := by rw [←hmeq, Nat.one_le_cast]; exact hm'.le
+  gcongr
   refine' (lpNorm_sub_le hm'' _ _).trans _
   rw [lpNorm_translate, two_mul ‖f‖_[2 * m], add_le_add_iff_left]
   have hmeq' : ((2 * m : ℝ≥0) : ℝ≥0∞) = 2 * m := by
@@ -162,7 +150,7 @@ lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) :
   refine' (lpNorm_conv_le this.le _ _).trans _
   rw [L1norm_mu hA, mul_one]
 
-lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hA : A.Nonempty) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) :
+lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m)  (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) :
     (8 * m : ℝ) ^ m * k ^ (m - 1) * A.card ^ k * k * (2 * ‖f‖_[2 * m]) ^ (2 * m) ≤
       1 / 2 * ((k * ε) ^ (2 * m) * ∑ i : G, ‖f i‖ ^ (2 * m)) * ↑A.card ^ k := by
   have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two]
@@ -173,10 +161,9 @@ lemma lemma28_end (hε : 0 < ε) (hm : 1 ≤ m) (hA : A.Nonempty) (hk : (64 : 
   rw [mul_pow (2 : ℝ), ←hmeq, ←lpNorm_pow_eq_sum hm' f, ←mul_assoc, ←mul_assoc,
     mul_right_comm _ (A.card ^ k : ℝ), mul_right_comm _ (A.card ^ k : ℝ),
     mul_right_comm _ (A.card ^ k : ℝ)]
-  -- positivity
-  refine' mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_right _ $ by sorry) (by positivity)
-  rw [mul_assoc (_ ^ m : ℝ), ←pow_succ', Nat.sub_add_cancel hm, pow_mul, pow_mul, ←mul_pow, ←
-    mul_pow]
+  gcongr ?_ * _ * _
+  rw [mul_assoc (_ ^ m : ℝ), ←pow_succ', Nat.sub_add_cancel hm, pow_mul, pow_mul, ← mul_pow,
+    ← mul_pow]
   have : (1 / 2 : ℝ) ^ m ≤ 1 / 2 := by
     have :=
       pow_le_pow_of_le_one (show (0 : ℝ) ≤ 1 / 2 by norm_num) (show (1 / 2 : ℝ) ≤ 1 by norm_num) hm
@@ -233,7 +220,7 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k)
     lemma28_part_two hm hA
   refine' this.trans _
   simp only [sum_const, Fintype.card_piFinsetConst, nsmul_eq_mul, Nat.cast_pow]
-  refine' (lemma28_end hε hm hA hk).trans_eq' _
+  refine' (lemma28_end hε hm hk).trans_eq' _
   simp only [mul_assoc]
   sorry
 
diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
index 537ce33798..f595a42de1 100644
--- a/LeanAPAP/Physics/Unbalancing.lean
+++ b/LeanAPAP/Physics/Unbalancing.lean
@@ -1,5 +1,6 @@
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Data.Complex.ExponentialBounds
+import LeanAPAP.Mathlib.Algebra.BigOperators.Order
 import LeanAPAP.Mathlib.Algebra.BigOperators.Ring
 import LeanAPAP.Mathlib.Algebra.Order.LatticeGroup
 import LeanAPAP.Mathlib.Analysis.Complex.Basic
@@ -9,6 +10,7 @@ import LeanAPAP.Mathlib.Data.Complex.Exponential
 import LeanAPAP.Mathlib.Data.Nat.Order.Basic
 import LeanAPAP.Prereqs.Convolution.Basic
 import LeanAPAP.Prereqs.LpNorm
+import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 /-!
 # Unbalancing
@@ -71,6 +73,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ ≤ 2 := by norm_num
       _ ≤ ‖f + 1‖_[2 * p, ν] := hf₁
       _ ≤ _ := wlpNorm_mono_right (NNReal.coe_le_coe.1 ?_) _ _
+    push_cast
     refine mul_le_mul_of_nonneg_right ?_ ?_
     calc
       2 ≤ 24 / 1 * 0.6931471803 := by norm_num
@@ -80,8 +83,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
             (log_le_log_of_le zero_lt_two $
               (div_le_div_of_le_left (by norm_num) hε₀ hε₁).trans' $ by norm_num))
           (by norm_num) ?_
-    any_goals positivity
-    sorry -- positivity
+    all_goals positivity
   have : ε ^ p ≤ 2 * ∑ i, ↑(ν i) * ((f ^ (p - 1)) i * (f⁺) i) := by
     calc
       ε ^ p ≤ ‖f‖_[p, ν] ^ p := hp₁.strictMono_pow.monotone hε
@@ -96,8 +98,8 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       pow_sub_one_mul hp₁.pos.ne']
     simp [l2inner_eq_sum, ←sum_add_distrib, ←mul_add, ←pow_sub_one_mul hp₁.pos.ne' (f _),
       mul_sum, mul_left_comm (2 : ℝ), add_abs_eq_two_nsmul_posPart]
-  set P := univ.filter fun i ↦ 0 ≤ f i with hP
-  set T := univ.filter fun i ↦ 3 / 4 * ε ≤ f i with hT
+  set P := univ.filter fun i ↦ 0 ≤ f i
+  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]
@@ -149,9 +151,7 @@ private lemma unbalancing' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
     simp only [wlpNorm_eq_sum hp'.ne', sqrt_eq_rpow, Nonneg.coe_one, rpow_two,
       abs_nonneg, NNReal.smul_def, rpow_mul, Pi.pow_apply, abs_pow, norm_eq_abs, mul_pow,
       rpow_nat_cast, smul_eq_mul, pow_mul, one_div, NNReal.coe_two]
-    · exact rpow_nonneg (sum_nonneg fun i _ ↦ by sorry) -- positivity
-    · positivity
-    · exact sum_nonneg fun i _ ↦ by sorry -- positivity
+    all_goals positivity
   set p' := 24 / ε * log (3 / ε) * p
   have hp' : 0 < p' := p'_pos hp hε₀ hε₁
   have : 1 - 8⁻¹ * ε ≤ (∑ i in T, ↑(ν i)) ^ p'⁻¹ := by
diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean
index 82a420f0fc..e1feab18f3 100644
--- a/LeanAPAP/Prereqs/Chang.lean
+++ b/LeanAPAP/Prereqs/Chang.lean
@@ -34,7 +34,7 @@ lemma largeSpec_anti (f : G → ℂ) : Antitone (largeSpec f) := fun η ν h ψ
 private noncomputable def α (f : G → ℂ) := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G
 
 lemma α_nonneg (f : G → ℂ) : 0 ≤ α f := by unfold α; positivity
-lemma α_pos (hf : f ≠ 0) : 0 < α f := by unfold α; sorry -- positivity
+lemma α_pos (hf : f ≠ 0) : 0 < α f := by unfold α; positivity
 
 lemma α_le_one (f : G → ℂ) : α f ≤ 1 := by
   refine' div_le_one_of_le (div_le_of_nonneg_of_le_mul _ _ _) _
diff --git a/LeanAPAP/Prereqs/DFT.lean b/LeanAPAP/Prereqs/DFT.lean
index bfe51c98ad..2d4032bff1 100644
--- a/LeanAPAP/Prereqs/DFT.lean
+++ b/LeanAPAP/Prereqs/DFT.lean
@@ -28,6 +28,8 @@ lemma dft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft f ψ = ⟪ψ, f⟫_
 @[simp] lemma dft_add (f g : α → ℂ) : dft (f + g) = dft f + dft g := by
   ext; simp [l2inner_add_right, dft_apply]
 
+@[simp] lemma dft_neg (f : α → ℂ) : dft (-f) = - dft f := by ext; simp [dft_apply]
+
 @[simp] lemma dft_sub (f g : α → ℂ) : dft (f - g) = dft f - dft g := by
   ext; simp [l2inner_sub_right, dft_apply]
 
@@ -143,10 +145,8 @@ lemma lpNorm_conv_le_lpNorm_dconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → 
     ‖f ∗ f‖_[n] ≤ ‖f ○ f‖_[n] := by
   cases isEmpty_or_nonempty α
   · rw [Subsingleton.elim (f ∗ f) (f ○ f)]
-  refine' le_of_pow_le_pow _ _ hn₀.bot_lt (le_of_mul_le_mul_left _ (_ : (0 : ℝ) < card α ^ n))
-  sorry -- positivity
-  swap
-  sorry -- positivity
+  refine' le_of_pow_le_pow _ (by positivity) hn₀.bot_lt $
+    le_of_mul_le_mul_left _ (by positivity : (0 : ℝ) < card α ^ n)
   obtain ⟨n, rfl⟩ := hn.two_dvd
   simp_rw [lpNorm_pow_eq_sum hn₀, mul_sum, ←mul_pow, ←nsmul_eq_mul, ←norm_nsmul, nsmul_eq_mul,
     ← dft_inversion', dft_conv, dft_dconv, Pi.mul_apply]
@@ -172,7 +172,6 @@ lemma lpNorm_conv_le_lpNorm_dconv (hn₀ : n ≠ 0) (hn : Even n) (f : α → 
     arg 2
     ext
     rw [←Complex.eq_coe_norm_of_nonneg (this _ _)]
-  letI : Fintype (Fin n → AddChar α ℂ) := @Pi.fintype _ _ _ _ fun i ↦ AddChar.instFintype _ _
   simp only [@sum_comm _ _ α, mul_sum, map_prod, map_mul, IsROrC.conj_conj, ←prod_mul_distrib]
   refine' sum_congr rfl fun x _ ↦ sum_congr rfl fun a _ ↦ prod_congr rfl fun i _ ↦ _
   ring
diff --git a/LeanAPAP/Prereqs/Indicator.lean b/LeanAPAP/Prereqs/Indicator.lean
index 0532d8cae0..ba02fb238a 100644
--- a/LeanAPAP/Prereqs/Indicator.lean
+++ b/LeanAPAP/Prereqs/Indicator.lean
@@ -114,6 +114,8 @@ variable [OrderedSemiring β] {s : Finset α}
   simp [indicate_apply, Pi.lt_def, Function.funext_iff, lt_iff_le_and_ne, @eq_comm β 0,
     Finset.Nonempty]
 
+protected alias ⟨_, Finset.Nonempty.indicate_pos⟩ := indicate_pos
+
 end OrderedSemiring
 
 /-! ### Normalised indicator -/
@@ -211,13 +213,47 @@ variable [LinearOrderedSemifield β] {s : Finset α}
 @[simp] lemma mu_nonneg : 0 ≤ μ_[β] s := fun a ↦ by rw [mu_apply]; split_ifs <;> norm_num
 @[simp] lemma mu_pos : 0 < μ_[β] s ↔ s.Nonempty := mu_nonneg.gt_iff_ne.trans mu_ne_zero
 
+protected alias ⟨_, Finset.Nonempty.mu_pos⟩ := mu_pos
+
 end LinearOrderedSemifield
 
 namespace Mathlib.Meta.Positivity
 open Lean Meta Qq Function
 
-private alias ⟨_, indicate_pos_of_nonempty⟩ := indicate_pos
-private alias ⟨_, mu_pos_of_nonempty⟩ := mu_pos
+-- private abbrev TypeFunction (α β : Type*) := α → β
+
+-- private alias ⟨_, mu_pos_of_nonempty⟩ := mu_pos
+-- #check indicate
+-- /-- Extension for the `positivity` tactic: an indicator is nonnegative, and positive if its support
+-- is nonempty. -/
+-- @[positivity indicate _]
+-- def evalIndicate : PositivityExt where eval {u π} zπ pπ e := do
+--   let u1 ← mkFreshLevelMVar
+--   let u2 ← mkFreshLevelMVar
+--   let _ : u =QL max u1 u2 := ⟨⟩
+--   match π, e with
+--   | ~q(TypeFunction.{u2, u1} $α $β), ~q(@indicate _ _ $instα $instβ $s) =>
+--     let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo?
+--       try {
+--         let _fi ← synthInstanceQ q(Fintype $α)
+--         let _no ← synthInstanceQ q(Nonempty $α)
+--         match s with
+--         | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
+--         | _ => pure none
+--       } catch _ => do
+--         let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
+--         pure (some (.fvar fv))
+--     assumeInstancesCommute
+--     match so with
+--     | .some (fi : Q(Finset.Nonempty $s)) =>
+--       try {
+--         let instβnontriv ← synthInstanceQ q(Nontrivial $β)
+--         assumeInstancesCommute
+--         return .positive q(Finset.Nonempty.indicate_pos $fi)
+--       } catch _ => return .nonnegative q(indicate_nonneg.{u, u_1})
+
+--     | none => return .nonnegative q(indicate_nonneg.{u, u_1})
+--   | _ => throwError "not Finset.indicate"
 
 -- TODO: Fix
 
diff --git a/LeanAPAP/Prereqs/LpNorm.lean b/LeanAPAP/Prereqs/LpNorm.lean
index 76de3aeea2..d3c8ba6ed9 100644
--- a/LeanAPAP/Prereqs/LpNorm.lean
+++ b/LeanAPAP/Prereqs/LpNorm.lean
@@ -8,7 +8,6 @@ import LeanAPAP.Mathlib.Data.Real.Archimedean
 import LeanAPAP.Mathlib.Data.Real.ENNReal
 import LeanAPAP.Mathlib.Data.Real.NNReal
 import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Finset
-import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Prereqs.Indicator
 
 /-!
@@ -26,13 +25,13 @@ section NormedAddCommGroup
 variable {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] {p q : ℝ≥0∞} {f g h : ∀ i, α i}
 
 /-- The Lp norm of a function. -/
-noncomputable def lpNorm (p : ℝ≥0∞) (f : ∀ i, α i) : ℝ :=‖(WithLp.equiv p _).symm f‖
+noncomputable def lpNorm (p : ℝ≥0∞) (f : ∀ i, α i) : ℝ := ‖(WithLp.equiv p _).symm f‖
 
 notation "‖" f "‖_[" p "]" => lpNorm p f
 
 lemma lpNorm_eq_sum' (hp : p.toReal ≠ 0) (f : ∀ i, α i) :
     ‖f‖_[p] = (∑ i, ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹ := by
-  rw [←one_div];  exact PiLp.norm_eq_sum (hp.lt_of_le' ENNReal.toReal_nonneg) _
+  rw [←one_div]; exact PiLp.norm_eq_sum (hp.lt_of_le' ENNReal.toReal_nonneg) _
 
 lemma lpNorm_eq_sum'' {p : ℝ} (hp : 0 < p) (f : ∀ i, α i) :
     ‖f‖_[p.toNNReal] = (∑ i, ‖f i‖ ^ p) ^ p⁻¹ := by rw [lpNorm_eq_sum'] <;>  simp [hp.ne', hp.le]
@@ -213,9 +212,7 @@ lemma wlpNorm_eq_sum' {p : ℝ} (hp : 0 < p) (w : ι → ℝ≥0) (f : ∀ i, α
 
 lemma wlpNorm_rpow_eq_sum {p : ℝ≥0} (hp : p ≠ 0) (w : ι → ℝ≥0) (f : ∀ i, α i) :
     ‖f‖_[p, w] ^ (p : ℝ) = ∑ i, w i • ‖f i‖ ^ (p : ℝ) := by
-  rw [wlpNorm_eq_sum hp, rpow_inv_rpow (sum_nonneg fun i _ ↦ ?_)]
-  · positivity
-  · sorry -- positivity
+  rw [wlpNorm_eq_sum hp, rpow_inv_rpow (sum_nonneg fun i _ ↦ ?_)] <;> positivity
 
 lemma wlpNorm_pow_eq_sum {p : ℕ} (hp : p ≠ 0) (w : ι → ℝ≥0) (f : ∀ i, α i) :
     ‖f‖_[p, w] ^ p = ∑ i, w i • ‖f i‖ ^ p := by
@@ -250,7 +247,7 @@ lemma wlpNorm_add_le (hp : 1 ≤ p) (w : ι → ℝ≥0) (f g : ∀ i, α i) :
     ‖f + g‖_[p, w] ≤ ‖f‖_[p, w] + ‖g‖_[p, w] := by
   unfold wlpNorm
   refine' (lpNorm_add_le (by exact_mod_cast hp) _ _).trans'
-    (lpNorm_mono (fun i ↦ by dsimp; sorry) fun i ↦ _) -- positivity
+    (lpNorm_mono (fun i ↦ by dsimp; positivity) fun i ↦ _)
   dsimp
   rw [←smul_add]
   exact smul_le_smul_of_nonneg (norm_add_le _ _) (zero_le _)
@@ -335,10 +332,8 @@ lemma wlpNorm_one (hp : p ≠ 0) (w : ι → ℝ≥0) :
   simp [wlpNorm_eq_sum hp, NNReal.smul_def]
 
 lemma wlpNorm_mono (hf : 0 ≤ f) (hfg : f ≤ g) : ‖f‖_[p, w] ≤ ‖g‖_[p, w] :=
-  lpNorm_mono (fun i ↦ by dsimp; sorry) fun i ↦ -- positivity
-    smul_le_smul_of_nonneg
-        (by rw [norm_of_nonneg (hf _), norm_of_nonneg (hf.trans hfg _)]; exact hfg _) $
-      by positivity
+  lpNorm_mono (fun i ↦ by dsimp; positivity) fun i ↦ smul_le_smul_of_nonneg
+    (by rw [norm_of_nonneg (hf _), norm_of_nonneg (hf.trans hfg _)]; exact hfg _) $ by positivity
 
 end Real
 
@@ -388,9 +383,11 @@ end CommSemiring
 section CommRing
 variable [CommRing 𝕜] [StarRing 𝕜]
 
+@[simp]
 lemma l2inner_neg_left (f g : ι → 𝕜) : ⟪-f, g⟫_[𝕜] = -⟪f, g⟫_[𝕜] := by
   simp [l2inner_eq_sum, sum_add_distrib]
 
+@[simp]
 lemma l2inner_neg_right (f g : ι → 𝕜) : ⟪f, -g⟫_[𝕜] = -⟪f, g⟫_[𝕜] := by
   simp [l2inner_eq_sum, sum_add_distrib]
 
@@ -541,46 +538,66 @@ private lemma l2inner_nonneg_of_pos_of_pos (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪
 
 end OrderedCommSemiring
 
--- TODO: Make it sound again :(
-set_option linter.unusedVariables false in
 /-- The `positivity` extension which identifies expressions of the form `‖f‖_[p]`. -/
-@[positivity ‖_‖_[_]] def evalLpNorm : PositivityExt where eval {u α} zα pα e := do
-  let .app (.app (_f :) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
-    | throwError "not ‖_‖_[_]"
-  match ← core zα pα b with
-  | .positive pa => return .positive q(dummy_pos_of_pos $pa)
-  | .nonzero pa => return .positive q(dummy_pos_of_nzr $pa)
-  | _ => return .nonnegative q(dummy_nng)
--- TODO: Make it sound again :(
-set_option linter.unusedVariables false in
+@[positivity ‖_‖_[_]] def evalLpNorm : PositivityExt where eval {u} α _z _p e := do
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℝ), ~q(@lpNorm $ι $instι $α $instnorm $p $f) =>
+      try {
+        let _pα ← synthInstanceQ (q(∀ i, PartialOrder ($α i)) : Q(Type (max u_1 u_2)))
+        assumeInstancesCommute
+        match ← core q(inferInstance) q(inferInstance) f with
+        | .positive pf => return .positive q(lpNorm_pos_of_pos $pf)
+        | .nonzero pf => return .positive q(lpNorm_pos_of_ne_zero $pf)
+        | _ => return .nonnegative q(lpNorm_nonneg)
+      } catch _ =>
+        assumeInstancesCommute
+        if let some pf ← findLocalDeclWithType? q($f ≠ 0) then
+          let pf : Q($f ≠ 0) := .fvar pf
+          return .positive q(lpNorm_pos_of_ne_zero $pf)
+        else
+          return .nonnegative q(lpNorm_nonneg)
+    | _ => throwError "not lpNorm"
+  else
+    throwError "not lpNorm"
+
 /-- The `positivity` extension which identifies expressions of the form `‖f‖_[p, w]`. -/
-@[positivity ‖_‖_[_, _]] def evalWLpNorm : PositivityExt where eval {u α} zα pα e := do
-  let .app (.app (_f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
-    | throwError "not ‖_‖_[_, _]"
-  return .nonnegative q(dummy_nng)
+@[positivity ‖_‖_[_, _]] def evalWLpNorm : PositivityExt where eval {u α} _ _ e := do
+  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
+    match α, e with
+    | ~q(ℝ), ~q(@wlpNorm $ι $instι $α $instnorm $p $w $f) =>
+          assumeInstancesCommute
+          return .nonnegative q(wlpNorm_nonneg)
+    | _ => throwError "not wlpNorm"
+  else
+    throwError "not wlpNorm"
 
--- TODO: Make it sound again :(
-set_option linter.unusedVariables false in
 /-- The `positivity` extension which identifies expressions of the form `⟪f, g⟫_[𝕜]`. -/
-@[positivity ⟪_, _⟫_[_]] def evall2inner : PositivityExt where eval {u α} zα pα e := do
-  let .app (.app (_f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
-    | throwError "not ⟪_, _⟫_[_]"
-  let ra ← core zα pα a; let rb ← core zα pα b
-  match ra, rb with
-  | .positive pa, .positive pb => return .positive q(dummy_pos_of_pos_pos $pa $pb)
-  | .positive pa, .nonnegative pb => return .nonnegative q(dummy_nng_of_pos_nng $pa $pb)
-  | .nonnegative pa, .positive pb => return .nonnegative q(dummy_nng_of_nng_pos $pa $pb)
-  | .nonnegative pa, .nonnegative pb => return .nonnegative q(dummy_nng_of_nng_nng $pa $pb)
-  | _, _ => pure .none
+@[positivity ⟪_, _⟫_[_]] def evalL2inner : PositivityExt where eval {u 𝕜} _ _ e := do
+  match e with
+  | ~q(@l2inner $ι _ $instι $instring $inststar $f $g) =>
+      let _p𝕜 ← synthInstanceQ q(OrderedCommSemiring $𝕜)
+      let _p𝕜 ← synthInstanceQ q(StarOrderedRing $𝕜)
+      assumeInstancesCommute
+      match ← core q(inferInstance) q(inferInstance) f,
+        ← core q(inferInstance) q(inferInstance) g with
+      | .positive pf, .positive pg => return .nonnegative q(l2inner_nonneg_of_pos_of_pos $pf $pg)
+      | .positive pf, .nonnegative pg =>
+        return .nonnegative q(l2inner_nonneg_of_pos_of_nonneg $pf $pg)
+      | .nonnegative pf, .positive pg =>
+        return .nonnegative q(l2inner_nonneg_of_nonneg_of_pos $pf $pg)
+      | .nonnegative pf, .nonnegative pg => return .nonnegative q(l2inner_nonneg $pf $pg)
+      | _, _ => return .none
+  | _ => throwError "not l2inner"
 
 section Examples
 
 section NormedAddCommGroup
 variable {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] {w : ι → ℝ≥0} {f : ∀ i, α i}
 
--- example {p : ℝ≥0∞} : 0 ≤ ‖f‖_[p] := by positivity
--- example {p : ℝ≥0∞} (hf : f ≠ 0) : 0 < ‖f‖_[p] := by positivity
--- example {p : ℝ≥0∞} {f : ι → ℝ} (hf : 0 < f) : 0 < ‖f‖_[p] := by positivity
+example {p : ℝ≥0∞} : 0 ≤ ‖f‖_[p] := by positivity
+example {p : ℝ≥0∞} (hf : f ≠ 0) : 0 < ‖f‖_[p] := by positivity
+example {p : ℝ≥0∞} {f : ι → ℝ} (hf : 0 < f) : 0 < ‖f‖_[p] := by positivity
 example {p : ℝ≥0} : 0 ≤ ‖f‖_[p, w] := by positivity
 
 end NormedAddCommGroup
@@ -588,19 +605,19 @@ end NormedAddCommGroup
 section OrderedCommSemiring
 variable [OrderedCommSemiring 𝕜] [StarOrderedRing 𝕜] {f g : ι → 𝕜}
 
--- example (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity
--- example (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity
--- example (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity
--- example (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity
+example (hf : 0 < f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity
+example (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity
+example (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity
+example (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[𝕜] := by positivity
 
 end OrderedCommSemiring
 
 section Complex
 variable {w : ι → ℝ≥0} {f : ι → ℂ}
 
--- example {p : ℝ≥0∞} : 0 ≤ ‖f‖_[p] := by positivity
--- example {p : ℝ≥0∞} (hf : f ≠ 0) : 0 < ‖f‖_[p] := by positivity
--- example {p : ℝ≥0∞} {f : ι → ℝ} (hf : 0 < f) : 0 < ‖f‖_[p] := by positivity
+example {p : ℝ≥0∞} : 0 ≤ ‖f‖_[p] := by positivity
+example {p : ℝ≥0∞} (hf : f ≠ 0) : 0 < ‖f‖_[p] := by positivity
+example {p : ℝ≥0∞} {f : ι → ℝ} (hf : 0 < f) : 0 < ‖f‖_[p] := by positivity
 example {p : ℝ≥0} : 0 ≤ ‖f‖_[p, w] := by positivity
 
 end Complex
@@ -621,7 +638,7 @@ lemma L1norm_mul_of_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f * g‖_[1] = ⟪
 
 lemma lpNorm_rpow (hp : p ≠ 0) (hq : q ≠ 0) (hf : 0 ≤ f) :
     ‖HPow.hPow f (q : ℝ)‖_[p] = ‖f‖_[p * q] ^ (q : ℝ) := by
-  refine' rpow_left_injOn (NNReal.coe_ne_zero.2 hp) lpNorm_nonneg (by dsimp; sorry) _ -- positivity
+  refine' rpow_left_injOn (NNReal.coe_ne_zero.2 hp) lpNorm_nonneg (by dsimp; positivity) _
   dsimp
   rw [←rpow_mul lpNorm_nonneg, ←mul_comm, ←ENNReal.coe_mul, ←NNReal.coe_mul,
     lpNorm_rpow_eq_sum hp, lpNorm_rpow_eq_sum (mul_ne_zero hq hp)]
@@ -672,7 +689,7 @@ lemma lpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹ +
   · norm_cast
     simp [div_eq_mul_inv, hpqr, ←mul_add, hr]
   any_goals intro a; dsimp
-  all_goals sorry -- positivity
+  all_goals positivity
 
 /-- Hölder's inequality, finitary case. -/
 lemma lpNorm_prod_le {s : Finset ι} (hs : s.Nonempty) {p : ι → ℝ≥0} (hp : ∀ i, p i ≠ 0) (q : ℝ≥0)
@@ -704,7 +721,7 @@ lemma lpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖_[p
     sum_boole, this, zero_rpow, filter_mem_eq_inter]
 
 lemma lpNorm_indicate (hp : p ≠ 0) (s : Finset α) : ‖𝟭_[β] s‖_[p] = s.card ^ (p⁻¹ : ℝ) := by
-  refine' (eq_rpow_inv _ _ _).2 (lpNorm_rpow_indicate _ _) <;> sorry -- positivity
+  refine' (eq_rpow_inv _ _ _).2 (lpNorm_rpow_indicate _ _) <;> positivity
 
 lemma lpNorm_pow_indicate {p : ℕ} (hp : p ≠ 0) (s : Finset α) :
     ‖𝟭_[β] s‖_[p] ^ (p : ℝ) = s.card := by
@@ -714,7 +731,7 @@ lemma l2norm_sq_indicate (s : Finset α) : ‖𝟭_[β] s‖_[2] ^ 2 = s.card :=
   simpa using lpNorm_pow_indicate two_ne_zero s
 
 lemma l2norm_indicate (s : Finset α) : ‖𝟭_[β] s‖_[2] = Real.sqrt s.card := by
-  rw [eq_comm, sqrt_eq_iff_sq_eq, l2norm_sq_indicate] <;> sorry -- positivity
+  rw [eq_comm, sqrt_eq_iff_sq_eq, l2norm_sq_indicate] <;> positivity
 
 @[simp] lemma L1norm_indicate (s : Finset α) : ‖𝟭_[β] s‖_[1] = s.card := by
   simpa using lpNorm_pow_indicate one_ne_zero s
@@ -724,10 +741,9 @@ end indicate
 section mu
 variable {α β : Type*} [IsROrC β] [Fintype α] [DecidableEq α] {s : Finset α} {p : ℝ≥0}
 
-lemma lpNorm_mu (hp : 1 ≤ p) (hs : s.Nonempty) : ‖μ_[β] s‖_[p] = s.card ^ (p⁻¹ - 1 : ℝ) := by
+lemma lpNorm_mu (hp : 1 ≤ p) (hs : s.Nonempty) : ‖μ_[β] s‖_[p] = s.card ^ ((p : ℝ)⁻¹ - 1) := by
   rw [mu, lpNorm_smul (ENNReal.one_le_coe_iff.2 hp) (s.card⁻¹ : β) (𝟭_[β] s), lpNorm_indicate,
-      norm_inv, IsROrC.norm_natCast, inv_mul_eq_div, ←rpow_sub_one] <;>
-    sorry -- positivity
+      norm_inv, IsROrC.norm_natCast, inv_mul_eq_div, ←rpow_sub_one] <;> positivity
 
 lemma lpNorm_mu_le (hp : 1 ≤ p) : ‖μ_[β] s‖_[p] ≤ s.card ^ (p⁻¹ - 1 : ℝ) := by
   obtain rfl | hs := s.eq_empty_or_nonempty
diff --git a/LeanAPAP/Prereqs/Rudin.lean b/LeanAPAP/Prereqs/Rudin.lean
index ca912508b5..cee47537d3 100644
--- a/LeanAPAP/Prereqs/Rudin.lean
+++ b/LeanAPAP/Prereqs/Rudin.lean
@@ -27,7 +27,7 @@ variable {α : Type*} [Fintype α] [AddCommGroup α] {p : ℕ}
 
 /-- **Rudin's inequality**, exponential form. -/
 lemma rudin_exp_ineq (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociated $ support $ dft f) :
-    𝔼 a, exp (card α * f a).re ≤ exp (‖f‖_[2] ^ 2 / 2) := by
+    𝔼 a, exp (card α * f a).re ≤ exp (card α * ‖f‖_[2] ^ 2 / 2) := by
   have (z : ℂ) : exp (re z) ≤ cosh ‖z‖ + re (z / ‖z‖) * sinh ‖z‖ :=
     calc
       _ = _ := by obtain rfl | hz := eq_or_ne z 0 <;> simp [norm_pos_iff.2, *]
@@ -54,12 +54,16 @@ lemma rudin_exp_ineq (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociated $ supp
     _ = _ := ?_
   sorry
 
-
-  -- calc
-  --   _ = exp (𝔼 a, 𝔼 ψ, dft f ψ * ψ a).re
-  -- rw [← dft_inversion']
-  -- calc
-  --   _ = exp (∑ )
+/-- **Rudin's inequality**, exponential form with absolute values. -/
+lemma rudin_exp_abs_ineq (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociated $ support $ dft f) :
+    𝔼 a, exp |(card α * f a).re| ≤ 2 * exp (card α * ‖f‖_[2] ^ 2 / 2) := by
+  calc
+    _ ≤ 𝔼 a, (exp (card α * f a).re + exp (-(card α * f a).re)) :=
+        expect_le_expect fun _ _ ↦ exp_abs_le _
+    _ = 𝔼 a, exp (card α * f a).re + 𝔼 a, exp (card α * (-f) a).re := by simp [expect_add_distrib]
+    _ ≤ exp (card α * ‖f‖_[2] ^ 2 / 2) + exp (card α * ‖-f‖_[2] ^ 2 / 2) :=
+        add_le_add (rudin_exp_ineq hp f hf) (rudin_exp_ineq hp (-f) $ by simpa using hf)
+    _ = _ := by simp [two_mul]
 
 private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociated $ support $ dft f) :
     ‖re ∘ f‖_[p] ≤ exp 2⁻¹ * sqrt p * ‖f‖_[2] := by
@@ -68,20 +72,16 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate
     · simp
     specialize H hp ((sqrt p / ‖f‖_[2]) • f) ?_
     · rwa [dft_smul, support_smul']
-      sorry -- positivity
+      positivity
     simp_rw [Function.comp_def, Pi.smul_apply, Complex.smul_re, ←Pi.smul_def] at H
     rw [lpNorm_smul, lpNorm_smul, norm_div, norm_of_nonneg, norm_of_nonneg, div_mul_cancel,
       div_mul_comm, mul_le_mul_right, div_le_iff] at H
     exact H rfl
-    · sorry -- positivity
-    · positivity
-    · sorry -- positivity
-    · sorry -- positivity
-    · positivity
+    any_goals positivity
     · norm_cast
       exact one_le_two.trans hp
     · norm_num
-  have h := rudin_exp_ineq hp f hf
+  have h := rudin_exp_abs_ineq hp f hf
   rw [hfp, sq_sqrt] at h
   -- We currently can't fill the next `sorry`
   have : Fintype.card α * p ! ≤ p ^ p := sorry -- false because wrong normalisation
@@ -89,9 +89,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate
   simp_rw [←expect_div, expect, ←norm_eq_abs, card_univ, div_div, ←Nat.cast_mul] at h
   rw [←lpNorm_pow_eq_sum, div_le_iff, div_eq_inv_mul, exp_mul, rpow_nat_cast] at h
   replace h := h.trans $ mul_le_mul_of_nonneg_left (Nat.cast_le.2 this) $ by positivity
-  rw [Nat.cast_pow, ←mul_pow, pow_le_pow_iff_left] at h
-  rwa [hfp, mul_assoc, ←sq, sq_sqrt]
-  all_goals sorry -- positivity
+  all_goals sorry
 
 -- This actually uses `Complex.ext`