Bump mathlib

LeanAPAP.lean

@@ -1,14 +1,20 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField.Basic
 import LeanAPAP.Mathlib.Algebra.Algebra.Basic
-import LeanAPAP.Mathlib.Algebra.BigOperators.Pi
+import LeanAPAP.Mathlib.Algebra.BigOperators.Ring
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Order.Module.Defs
 import LeanAPAP.Mathlib.Analysis.Complex.Circle
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Circle
-import LeanAPAP.Mathlib.Data.Fintype.Pi
+import LeanAPAP.Mathlib.Data.Fintype.BigOperators
 import LeanAPAP.Mathlib.Data.Rat.Cast.Defs
 import LeanAPAP.Mathlib.Data.Rat.Cast.Lemmas
+import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
+import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import LeanAPAP.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
+import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
+import LeanAPAP.Mathlib.MeasureTheory.OuterMeasure.AE
+import LeanAPAP.Mathlib.Order.LiminfLimsup
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
@@ -28,6 +34,7 @@ import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.Convolution.WithConv
 import LeanAPAP.Prereqs.Curlog
 import LeanAPAP.Prereqs.Energy
+import LeanAPAP.Prereqs.EssSupCount
 import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Compact

LeanAPAP/Mathlib/Algebra/Algebra/Basic.lean

@@ -1,19 +1,18 @@
 import Mathlib.Algebra.Algebra.Basic
 import LeanAPAP.Mathlib.Data.Rat.Cast.Lemmas
 
-open NNRat
-
 variable {F α β : Type*}
 
+namespace NNRat
 section DivisionSemiring
 variable [DivisionSemiring α] [CharZero α] [DivisionSemiring β] [CharZero β]
 
-instance NNRat.instAlgebra : Algebra ℚ≥0 α where
+instance instAlgebra : Algebra ℚ≥0 α where
   smul_def' := smul_def
   toRingHom := castHom α
   commutes' := cast_commute
 
-instance NNRat.instlinearMapClass [FunLike F α β] [RingHomClass F α β] :
+instance instlinearMapClass [FunLike F α β] [RingHomClass F α β] :
     LinearMapClass F ℚ≥0 α β where
   map_smulₛₗ f q a := by simp [smul_def, cast_id]
 
@@ -22,10 +21,10 @@ end DivisionSemiring
 section Semifield
 variable [Semifield β] [CharZero β] [SMul α β]
 
-instance NNRat.instSMulCommClass [SMulCommClass α β β] : SMulCommClass ℚ≥0 α β where
+instance instSMulCommClass [SMulCommClass α β β] : SMulCommClass ℚ≥0 α β where
   smul_comm q a b := by simp [smul_def, mul_smul_comm]
 
-instance NNRat.instSMulCommClass' [SMulCommClass β α β] : SMulCommClass α ℚ≥0 β :=
+instance instSMulCommClass' [SMulCommClass β α β] : SMulCommClass α ℚ≥0 β :=
   have := SMulCommClass.symm β α β
   SMulCommClass.symm _ _ _
 
@@ -35,13 +34,13 @@ section Semifield
 variable [Semifield α] [CharZero α] [Semiring β] [CharZero β] [NNRatCast β] [Module ℚ≥0 β]
 
 variable (α) in
--- TODO: Change `nnsmul_eq_smul_cast` to match
 /-- `nnqsmul` is equal to any other module structure via a cast. -/
-lemma _root_.nnratCast_smul_eq_nnqsmul [Module α β] (q : ℚ≥0) (a : β) : (q : α) • a = q • a := by
+lemma cast_smul_eq_nnqsmul [Module α β] (q : ℚ≥0) (a : β) : (q : α) • a = q • a := by
   refine MulAction.injective₀ (α := ℚ≥0) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_
   dsimp
-  rw [← mul_smul, den_mul_eq_num, ← nsmul_eq_smul_cast, ← nsmul_eq_smul_cast, ← smul_assoc,
+  rw [← mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Nat.cast_smul_eq_nsmul, ← smul_assoc,
     nsmul_eq_mul q.den, ← cast_natCast, ←cast_mul, den_mul_eq_num, cast_natCast,
-    ← nsmul_eq_smul_cast]
+    Nat.cast_smul_eq_nsmul]
 
 end Semifield
+end NNRat

LeanAPAP/Mathlib/Algebra/BigOperators/Pi.lean → LeanAPAP/Mathlib/Algebra/BigOperators/Ring.lean

@@ -1,6 +1,4 @@
-import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Algebra.BigOperators.Ring
-import LeanAPAP.Mathlib.Data.Fintype.Pi
 
 open Finset
 

LeanAPAP/Mathlib/Data/Fintype/BigOperators.lean

@@ -0,0 +1,15 @@
+import Mathlib.Data.Fintype.BigOperators
+
+open Finset
+
+namespace Fintype
+variable {α β : Type*} {δ : α → Type*} {s : Finset α} {n : ℕ}
+
+local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
+
+protected lemma _root_.Finset.Nonempty.piFinset_const (hs : s.Nonempty) : (s ^^ n).Nonempty :=
+  piFinset_nonempty.2 fun _ ↦ hs
+
+lemma card_piFinset_const (s : Finset α) (n : ℕ) : (s ^^ n).card = s.card ^ n := by simp
+
+end Fintype

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -87,6 +87,8 @@ variable {G : Type*} [DecidableEq G] [Fintype G] [AddCommGroup G] {A S : Finset
 open Finset Real
 open scoped BigOperators Pointwise NNReal ENNReal
 
+local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
+
 namespace AlmostPeriodicity
 
 def LProp (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) (a : Fin k → G) : Prop :=
@@ -102,10 +104,10 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
         ‖fun x : G ↦ ∑ i : Fin k, f (x - a i) - (k • (mu A ∗ f)) x‖_[2 * m] ^ (2 * 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
+  rw [←Nat.cast_pow, ←Fintype.card_piFinset_const] at h
   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
+  rw [Fintype.card_piFinset_const, mul_comm, mul_one_div, Nat.cast_pow] at this
   refine this.trans_eq ?_
   rw [l]
   congr with a : 3
@@ -212,7 +214,7 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k)
         ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) :=
     lemma28_part_two hm hA
   refine this.trans ?_
-  simp only [sum_const, Fintype.card_piFinsetConst, nsmul_eq_mul, Nat.cast_pow]
+  simp only [sum_const, Fintype.card_piFinset_const, nsmul_eq_mul, Nat.cast_pow]
   refine (lemma28_end hε hm hk).trans_eq' ?_
   simp only [mul_assoc, card_fin]
 
@@ -304,7 +306,7 @@ lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0)
   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 ?_
-    rw [←Fintype.card_piFinsetConst]
+    rw [←Fintype.card_piFinset_const]
     refine card_le_card fun i hi ↦ ?_
     simp only [mem_add, mem_piDiag, Fintype.mem_piFinset, exists_prop, exists_and_left,
       exists_exists_and_eq_and] at hi ⊢
@@ -482,10 +484,10 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
   calc
     ‖μ T ∗^ k ∗ F - F‖_[∞]
       = ‖𝔼 a ∈ T ^^ k, (τ (∑ i, a i) F - F)‖_[∞] := by
-        rw [mu_iterConv_conv, expect_sub_distrib, expect_const hT'.piFinsetConst]
+        rw [mu_iterConv_conv, expect_sub_distrib, expect_const hT'.piFinset_const]
     _ ≤ 𝔼 a ∈ T ^^ k, ‖τ (∑ i, a i) F - F‖_[∞] := lpNorm_expect_le le_top _ _
     _ ≤ 𝔼 _a ∈ T ^^ k, ε := expect_le_expect fun x hx ↦ ?_
-    _ = ε := by rw [expect_const hT'.piFinsetConst]
+    _ = ε := by rw [expect_const hT'.piFinset_const]
   calc
     ‖τ (∑ i, x i) F - F‖_[⊤]
     _ ≤ ∑ i, ‖τ (x i) F - F‖_[⊤] := lpNorm_translate_sum_sub_le le_top _ _ _

LeanAPAP/Prereqs/Chang.lean

@@ -12,9 +12,11 @@ import LeanAPAP.Prereqs.Rudin
 open Finset Fintype Function Real
 open scoped ComplexConjugate ComplexOrder NNReal
 
-variable {G : Type*} [AddCommGroup G] [Fintype G] {f : G → ℂ} {η : ℝ} {ψ : AddChar G ℂ}
+  variable {G : Type*} [AddCommGroup G] [Fintype G] {f : G → ℂ} {η : ℝ} {ψ : AddChar G ℂ}
   {Δ : Finset (AddChar G ℂ)} {m : ℕ}
 
+local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
+
 private noncomputable def α (f : G → ℂ) := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G
 
 lemma α_nonneg (f : G → ℂ) : 0 ≤ α f := by unfold α; positivity

LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean

@@ -1,6 +1,5 @@
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Mathlib.Data.Fintype.Pi
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 
@@ -34,6 +33,8 @@ point in time.
 Multiplicativise? Probably ugly and not very useful.
 -/
 
+local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
+
 open Finset Fintype Function
 open scoped BigOperators ComplexConjugate NNReal Pointwise
 
@@ -166,8 +167,8 @@ variable [Semifield β] [CharZero β] [Module ℚ≥0 β] [StarRing β]
 lemma mu_iterConv_conv (s : Finset α) (n : ℕ) (f : α → β) :
     μ s ∗^ n ∗ f = 𝔼 a ∈ piFinset (fun _ : Fin n ↦ s), τ (∑ i, a i) f := by
   simp only [mu, smul_iterConv, inv_pow, smul_conv, indicate_iterConv_conv, expect,
-    card_piFinsetConst, Nat.cast_pow]
-  rw [← nnratCast_smul_eq_nnqsmul β]
+    card_piFinset_const, Nat.cast_pow]
+  rw [← NNRat.cast_smul_eq_nnqsmul β]
   push_cast
   rfl
 

LeanAPAP/Prereqs/Expect/Basic.lean

@@ -3,7 +3,7 @@ import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Mathlib.Algebra.Algebra.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Module.Defs
-import LeanAPAP.Mathlib.Data.Fintype.Pi
+import LeanAPAP.Mathlib.Data.Fintype.BigOperators
 
 /-!
 # Average over a finset
@@ -215,14 +215,14 @@ lemma _root_.map_expect {F : Type*} [FunLike F α β] [LinearMapClass F ℚ≥0
 lemma card_smul_expect (s : Finset ι) (f : ι → α) : s.card • 𝔼 i ∈ s, f i = ∑ i ∈ s, f i := by
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
-  · rw [expect, nsmul_eq_smul_cast ℚ≥0, smul_inv_smul₀]
+  · rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀]
     positivity
 
 @[simp] nonrec lemma _root_.Fintype.card_smul_expect [Fintype ι] (f : ι → α) :
     Fintype.card ι • 𝔼 i, f i = ∑ i, f i := card_smul_expect _ _
 
 @[simp] lemma expect_const (hs : s.Nonempty) (a : α) : 𝔼 _i ∈ s, a = a := by
-  rw [expect, sum_const, nsmul_eq_smul_cast ℚ≥0, inv_smul_smul₀]; positivity
+  rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]; positivity
 
 lemma smul_expect {G : Type*} [DistribSMul G α] [SMulCommClass G ℚ≥0 α] (a : G)
     (s : Finset ι) (f : ι → α) : a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i := by
@@ -297,10 +297,12 @@ end Semiring
 section CommSemiring
 variable [CommSemiring α] [Module ℚ≥0 α] [IsScalarTower ℚ≥0 α α] [SMulCommClass ℚ≥0 α α]
 
+local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
+
 lemma expect_pow (s : Finset ι) (f : ι → α) (n : ℕ) :
     (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ s ^^ n, ∏ i, f (p i) := by
   classical
-  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinsetConst, inv_pow, Nat.cast_pow]
+  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]
 
 end CommSemiring
 
@@ -358,11 +360,11 @@ lemma _root_.GCongr.expect_le_expect (h : ∀ i ∈ s, f i ≤ g i) : s.expect f
 
 lemma expect_le (hs : s.Nonempty) (f : ι → α) (a : α) (h : ∀ x ∈ s, f x ≤ a) : 𝔼 i ∈ s, f i ≤ a :=
   (inv_smul_le_iff_of_pos $ by positivity).2 $ by
-    rw [←nsmul_eq_smul_cast]; exact sum_le_card_nsmul _ _ _ h
+    rw [Nat.cast_smul_eq_nsmul]; exact sum_le_card_nsmul _ _ _ h
 
 lemma le_expect (hs : s.Nonempty) (f : ι → α) (a : α) (h : ∀ x ∈ s, a ≤ f x) : a ≤ 𝔼 i ∈ s, f i :=
   (le_inv_smul_iff_of_pos $ by positivity).2 $ by
-    rw [←nsmul_eq_smul_cast]; exact card_nsmul_le_sum _ _ _ h
+    rw [Nat.cast_smul_eq_nsmul]; exact card_nsmul_le_sum _ _ _ h
 
 lemma expect_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ 𝔼 i ∈ s, f i :=
   smul_nonneg (by positivity) $ sum_nonneg hf

LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean

@@ -25,7 +25,7 @@ lemma lpNorm_expect_le [∀ i, Module ℚ≥0 (α i)] (hp : 1 ≤ p) {κ : Type*
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
   refine (le_inv_smul_iff_of_pos $ by positivity).2 ?_
-  rw [← nsmul_eq_smul_cast, ← lpNorm_nsmul hp, card_smul_expect]
+  rw [Nat.cast_smul_eq_nsmul, ← lpNorm_nsmul hp, card_smul_expect]
   exact lpNorm_sum_le hp _ _
 
 end one_le

LeanAPAP/Prereqs/LpNorm/Weighted.lean

@@ -127,7 +127,7 @@ variable [∀ i, NormedSpace ℝ (α i)]
 
 lemma wlpNorm_nsmul (hp : 1 ≤ p) (n : ℕ) (w : ι → ℝ≥0) (f : ∀ i, α i) :
     ‖n • f‖_[p, w] = n • ‖f‖_[p, w] := by
-  rw [nsmul_eq_smul_cast ℝ, wlpNorm_smul hp, RCLike.norm_natCast, nsmul_eq_mul]
+  rw [← Nat.cast_smul_eq_nsmul ℝ, wlpNorm_smul hp, RCLike.norm_natCast, nsmul_eq_mul]
 
 end one_le
 

LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean

@@ -1,21 +1,23 @@
 import Mathlib.Analysis.MeanInequalitiesPow
-import LeanAPAP.Mathlib.Algebra.BigOperators.Pi
+import LeanAPAP.Mathlib.Data.Fintype.BigOperators
 import LeanAPAP.Prereqs.Multinomial
 
 open Finset Fintype Nat Real
 variable {G : Type*} {A : Finset G} {m n : ℕ}
 
+local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
+
 private lemma step_one (hA : A.Nonempty) (f : G → ℝ) (a : Fin n → G)
-    (hf : ∀ i : Fin n, ∑ a in A^^n, f (a i) = 0) :
+    (hf : ∀ i : Fin n, ∑ a in A ^^ n, f (a i) = 0) :
     |∑ i, f (a i)| ^ (m + 1) ≤ (∑ b in A^^n, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / A.card ^ n :=
   calc
     |∑ i, f (a i)| ^ (m + 1)
       = |∑ i, (f (a i) - (∑ b in A^^n, f (b i)) / (A^^n).card)| ^ (m + 1) := by
         simp only [hf, sub_zero, zero_div]
     _ = |(∑ b in A^^n, ∑ i, (f (a i) - f (b i))) / (A^^n).card| ^ (m + 1) := by
         simp only [sum_sub_distrib]
-        rw [sum_const, sub_div, sum_comm, sum_div, nsmul_eq_mul, card_piFinsetConst, Nat.cast_pow,
-          mul_div_cancel_left₀]
+        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₀]
         exact pow_ne_zero _ $ Nat.cast_ne_zero.2 hA.card_pos.ne'
     _ = |∑ b in A^^n, ∑ i, (f (a i) - f (b i))| ^ (m + 1) / (A^^n).card ^ (m + 1) := by
       rw [abs_div, div_pow, Nat.abs_cast]
@@ -82,7 +84,7 @@ private lemma step_two (f : G → ℝ) :
     ∑ a in A^^n, ∑ b in A^^n, (∑ i, ε i * (f (a i) - f (b i))) ^ (2 * m) =
       ∑ a in A^^n, ∑ b in A^^n, (∑ i, (f (a i) - f (b i))) ^ (2 * m) :=
     fun ε hε ↦ step_two_aux A f _ hε fun z : Fin n → ℝ ↦ univ.sum z ^ (2 * m)
-  rw [Finset.sum_congr rfl this, sum_const, card_piFinsetConst, card_pair, nsmul_eq_mul,
+  rw [Finset.sum_congr rfl this, sum_const, card_piFinset_const, card_pair, nsmul_eq_mul,
     Nat.cast_pow, Nat.cast_two, inv_pow, inv_mul_cancel_left₀]
   · positivity
   · norm_num
@@ -93,7 +95,7 @@ private lemma step_three (f : G → ℝ) :
       ∑ a in A^^n, ∑ b in A^^n, ∑ k in piAntidiag univ (2 * m),
           (multinomial univ k * ∏ t, (f (a t) - f (b t)) ^ k t) *
             ∑ ε in ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t := by
-  simp only [@sum_comm _ _ (Fin n → ℝ) _ _ (A^^n), ←Complex.abs_pow, multinomial_expansion']
+  simp only [@sum_comm _ _ (Fin n → ℝ) _ _ (A^^n), ←Complex.abs_pow, sum_pow_eq_sum_piAntidiag]
   refine sum_congr rfl fun a _ ↦ ?_
   refine sum_congr rfl fun b _ ↦ ?_
   simp only [mul_pow, prod_mul_distrib, @sum_comm _ _ (Fin n → ℝ), ←mul_sum, ←sum_mul]
@@ -103,7 +105,7 @@ private lemma step_three (f : G → ℝ) :
 private lemma step_four {k : Fin n → ℕ} :
     ∑ ε in ({-1, 1} : Finset ℝ)^^n, ∏ t, ε t ^ k t = 2 ^ n * ite (∀ i, Even (k i)) 1 0 := by
   have := sum_prod_piFinset ({-1, 1} : Finset ℝ) fun i fi ↦ fi ^ k i
-  rw [piFinsetConst, this, ←Fintype.prod_boole]
+  rw [this, ←Fintype.prod_boole]
   have : (2 : ℝ) ^ n = ∏ i : Fin n, 2 := by simp
   rw [this, ←prod_mul_distrib]
   refine prod_congr rfl fun t _ ↦ ?_
@@ -121,7 +123,7 @@ private lemma step_six {f : G → ℝ} {a b : Fin n → G} :
     ∑ k : Fin n → ℕ in piAntidiag univ m,
         (multinomial univ fun a ↦ 2 * k a : ℝ) * ∏ i : Fin n, (f (a i) - f (b i)) ^ (2 * k i) ≤
       m ^ m * (∑ i : Fin n, (f (a i) - f (b i)) ^ 2) ^ m := by
-  rw [multinomial_expansion', mul_sum]
+  rw [sum_pow_eq_sum_piAntidiag, mul_sum]
   convert sum_le_sum fun k hk ↦ _
   rw [mem_piAntidiag] at hk
   simp only [←mul_assoc, pow_mul]
@@ -169,8 +171,8 @@ private lemma end_step {f : G → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) :
     _ = _ := by
       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_piFinsetConst,
-        Nat.cast_pow, mul_div_cancel_left₀]
+        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₀]
       norm_num
       · have := hA.card_pos
         positivity
@@ -184,7 +186,7 @@ lemma basic_marcinkiewicz_zygmund (f : G → ℝ) (hf : ∀ i : Fin n, ∑ a in
   rcases A.eq_empty_or_nonempty with (rfl | hA)
   · cases n
     · cases m <;> simp
-    · rw [piFinsetConst, piFinset_empty, Finset.sum_empty]
+    · rw [piFinset_empty, Finset.sum_empty]
       cases m <;> simp
   refine (sum_le_sum fun a (_ : a ∈ A^^n) ↦ @step_one' _ _ _ _ hA f hf a).trans ?_
   rw [←sum_div]