diff --git a/LeanAPAP/Extras/BSG.lean b/LeanAPAP/Extras/BSG.lean
index 7e0944f75a..b8fbeebf82 100644
--- a/LeanAPAP/Extras/BSG.lean
+++ b/LeanAPAP/Extras/BSG.lean
@@ -1,5 +1,6 @@
 import Mathlib.Combinatorics.Additive.Energy
 import Mathlib.Data.Real.StarOrdered
+import Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Order
 
@@ -10,73 +11,66 @@ section
 variable {α : Type*} [DecidableEq α] {H : Finset (α × α)} {A B X : Finset α} {x : α}
 
 private noncomputable def oneOfPair (H : Finset (α × α)) (X : Finset α) : Finset α :=
-  X.filter fun x ↦ (3 / 4 : ℝ) * X.card ≤ (H.filter fun yz ↦ yz.1 = x).card
+  {x ∈ X | (3 / 4 : ℝ) * #X ≤ #{yz ∈ H | yz.1 = x}}
 
 private lemma oneOfPair_mem :
-    x ∈ oneOfPair H X ↔ x ∈ X ∧ (3 / 4 : ℝ) * X.card ≤ (H.filter fun yz ↦ yz.1 = x).card :=
-  mem_filter
+    x ∈ oneOfPair H X ↔ x ∈ X ∧ (3 / 4 : ℝ) * #X ≤ #{yz ∈ H | yz.1 = x} := mem_filter
 
-private lemma oneOfPair_mem' (hH : H ⊆ X ×ˢ X) :
-    (H.filter fun yz ↦ yz.1 = x).card = (X.filter fun c ↦ (x, c) ∈ H).card := by
+private lemma oneOfPair_mem' (hH : H ⊆ X ×ˢ X) : #{yz ∈ H | yz.1 = x} = #{c ∈ X | (x, c) ∈ H} := by
   refine card_nbij' Prod.snd (fun c ↦ (x, c)) ?_ (by simp) (by aesop) (by simp)
   simp (config := { contextual := true }) only [eq_comm, Prod.forall, mem_filter, and_imp, and_true]
   exact fun a b hab _ ↦ (mem_product.1 (hH hab)).2
 
 private lemma oneOfPair_bound_one :
-    ∑ x in X \ oneOfPair H X, ((H.filter (fun xy ↦ xy.1 = x)).card : ℝ) ≤ (3 / 4) * X.card ^ 2 :=
-  calc _ ≤ ∑ _x in X \ oneOfPair H X, (3 / 4 : ℝ) * X.card := sum_le_sum fun i hi ↦ by
-          simp only [oneOfPair, ← filter_not, Prod.forall, not_le, not_lt, mem_filter] at hi
-          exact hi.2.le
-       _ = (X \ oneOfPair H X).card * ((3 / 4 : ℝ) * X.card) := by simp
-       _ ≤ X.card * ((3 / 4 : ℝ) * X.card) := by gcongr; exact sdiff_subset
+    ∑ x ∈ X \ oneOfPair H X, (#{yz ∈ H | yz.1 = x} : ℝ) ≤ (3 / 4) * #X ^ 2 :=
+  calc _ ≤ ∑ _x ∈ X \ oneOfPair H X, (3 / 4 : ℝ) * #X := by
+        gcongr with i hi
+        simp only [oneOfPair, ← filter_not, Prod.forall, not_le, not_lt, mem_filter] at hi
+        exact hi.2.le
+       _ = #(X \ oneOfPair H X) * ((3 / 4 : ℝ) * #X) := by simp
+       _ ≤ #X * ((3 / 4 : ℝ) * #X) := by gcongr; exact sdiff_subset
        _ = _ := by ring
 
-private lemma oneOfPair_bound_two (hH : H ⊆ X ×ˢ X) (Hcard : (7 / 8 : ℝ) * X.card ^ 2 ≤ H.card) :
-    (1 / 8 : ℝ) * X.card ^ 2 ≤ X.card * (oneOfPair H X).card :=
-  calc _ = (7 / 8 : ℝ) * X.card ^ 2 - 3 / 4 * X.card ^ 2 := by ring
-       _ ≤ H.card - (3 / 4 : ℝ) * X.card ^ 2 := by linarith
-       _ ≤ H.card - ∑ x in X \ oneOfPair H X, ↑(H.filter (fun xy ↦ xy.1 = x)).card :=
-          sub_le_sub_left oneOfPair_bound_one _
-       _ = (H.card - ∑ x in X, ↑(H.filter (fun xy ↦ xy.1 = x)).card) +
-              ∑ x in oneOfPair H X, ↑(H.filter (fun xy ↦ xy.1 = x)).card := by
-          rw [sum_sdiff_eq_sub, sub_add]
-          exact filter_subset _ _
-       _ = ∑ x in oneOfPair H X, ↑(H.filter (fun xy ↦ xy.1 = x)).card := by
-          rw [add_left_eq_self, sub_eq_zero, ← Nat.cast_sum, Nat.cast_inj,
-            ← card_eq_sum_card_fiberwise]
-          intro x hx
-          exact (mem_product.1 (hH hx)).1
-       _ ≤ ∑ _x in oneOfPair H X, ↑X.card := sum_le_sum <| fun i hi ↦ Nat.cast_le.2 <| by
-          rw [oneOfPair_mem' hH]
-          exact card_le_card (filter_subset _ _)
-       _ = X.card * (oneOfPair H X).card := by simp [mul_comm]
-
-private lemma oneOfPair_bound {K : ℝ} (hH : H ⊆ X ×ˢ X) (hX : (0 : ℝ) < X.card)
-    (Hcard : (7 / 8 : ℝ) * X.card ^ 2 ≤ H.card) (h : A.card / (2 * K) ≤ X.card) :
-    A.card / (2 ^ 4 * K) ≤ (oneOfPair H X).card := -- by
-  calc _ = (A.card / (2 * K)) / 8 := by ring
-       _ ≤ (X.card / 8 : ℝ) := by gcongr
-       _ ≤ (oneOfPair H X).card :=
-            le_of_mul_le_mul_left ((oneOfPair_bound_two hH Hcard).trans_eq' (by ring)) hX
+private lemma oneOfPair_bound_two (hH : H ⊆ X ×ˢ X) (Hcard : (7 / 8 : ℝ) * #X ^ 2 ≤ #H) :
+    (1 / 8 : ℝ) * #X ^ 2 ≤ #X * #(oneOfPair H X) :=
+  calc _ = (7 / 8 : ℝ) * #X ^ 2 - 3 / 4 * #X ^ 2 := by ring
+       _ ≤ #H - (3 / 4 : ℝ) * #X ^ 2 := by linarith
+       _ ≤ #H - ∑ x ∈ X \ oneOfPair H X, (#{yz ∈ H | yz.1 = x} : ℝ) := by
+        gcongr; exact oneOfPair_bound_one
+       _ = #H - ∑ x ∈ X, (#{yz ∈ H | yz.1 = x} : ℝ) +
+              ∑ x ∈ oneOfPair H X, (#{yz ∈ H | yz.1 = x} : ℝ) := by
+        rw [sum_sdiff_eq_sub, sub_add]; exact filter_subset ..
+       _ = ∑ x ∈ oneOfPair H X, (#{yz ∈ H | yz.1 = x} : ℝ) := by
+        rw [add_left_eq_self, sub_eq_zero, ← Nat.cast_sum, Nat.cast_inj,
+          ← card_eq_sum_card_fiberwise]
+        exact fun x hx ↦ (mem_product.1 (hH hx)).1
+       _ ≤ ∑ _x ∈ oneOfPair H X, (#X : ℝ) := by
+        simp_rw [oneOfPair_mem' hH]; gcongr with i; exact filter_subset ..
+       _ = #X * #(oneOfPair H X) := by simp [mul_comm]
+
+private lemma oneOfPair_bound {K : ℝ} (hH : H ⊆ X ×ˢ X) (hX : (0 : ℝ) < #X)
+    (Hcard : (7 / 8 : ℝ) * #X ^ 2 ≤ #H) (h : #A / (2 * K) ≤ #X) :
+    #A / (2 ^ 4 * K) ≤ #(oneOfPair H X) := -- by
+  calc
+    _ = (#A / (2 * K)) / 8 := by ring
+    _ ≤ (#X / 8 : ℝ) := by gcongr
+    _ ≤ #(oneOfPair H X) :=
+      le_of_mul_le_mul_left ((oneOfPair_bound_two hH Hcard).trans_eq' (by ring)) hX
 
 lemma quadruple_bound_c {a b : α} {H : Finset (α × α)} (ha : a ∈ oneOfPair H X)
     (hb : b ∈ oneOfPair H X) (hH : H ⊆ X ×ˢ X) :
-    (X.card : ℝ) / 2 ≤ (X.filter fun c ↦ (a, c) ∈ H ∧ (b, c) ∈ H).card := by
+    (#X : ℝ) / 2 ≤ #{c ∈ X | (a, c) ∈ H ∧ (b, c) ∈ H} := by
   rw [oneOfPair_mem, oneOfPair_mem' hH] at ha hb
   rw [filter_and, cast_card_inter, ← filter_or]
-  have : ((X.filter fun c ↦ (a, c) ∈ H ∨ (b, c) ∈ H).card : ℝ) ≤ X.card := by
-    rw [Nat.cast_le]
-    exact card_le_card (filter_subset _ _)
+  have : (#{c ∈ X | (a, c) ∈ H ∨ (b, c) ∈ H} : ℝ) ≤ #X := by gcongr; exact filter_subset ..
   linarith [ha.2, hb.2, this]
 
 variable [AddCommGroup α]
 
 lemma quadruple_bound_right {a b : α} (H : Finset (α × α)) (X : Finset α) (h : x = a - b) :
-    (((X.filter fun c ↦ (a, c) ∈ H ∧ (b, c) ∈ H).sigma fun c ↦
-      ((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦
-        a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c).card : ℝ) ≤
-      (((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦
-        (a₁ - a₂) - (a₃ - a₄) = a - b).card := by
+    (#({c ∈ X | (a, c) ∈ H ∧ (b, c) ∈ H}.sigma fun c ↦ ((B ×ˢ B) ×ˢ B ×ˢ B).filter
+        fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c) : ℝ)
+      ≤ #(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = a - b) := by
   rw [← h, Nat.cast_le]
   refine card_le_card_of_injOn Sigma.snd ?_ ?_
   · simp only [not_and, mem_product, and_imp, Prod.forall, mem_sigma, mem_filter, Sigma.forall]
@@ -96,12 +90,12 @@ variable {A B : Finset G} {x : G}
 lemma thing_one : (𝟭_[R] B ○ 𝟭 A) x = ∑ y, 𝟭 A y * 𝟭 B (x + y) := by
   simp only [dconv_eq_sum_add, conj_indicate_apply, mul_comm]
 
-lemma thing_one_right : (𝟭_[R] A ○ 𝟭 B) x = (A ∩ (x +ᵥ B)).card := by
+lemma thing_one_right : (𝟭_[R] A ○ 𝟭 B) x = #(A ∩ (x +ᵥ B)) := by
   rw [indicate_dconv_indicate_apply]
   congr 1
   apply card_nbij' Prod.fst (fun a ↦ (a, a - x)) <;> aesop (add simp [mem_vadd_finset])
 
-lemma thing_two : ∑ s, (𝟭_[R] A ○ 𝟭 B) s = A.card * B.card := by
+lemma thing_two : ∑ s, (𝟭_[R] A ○ 𝟭 B) s = #A * #B := by
   simp only [sum_dconv, conj_indicate_apply, sum_indicate]
 
 lemma thing_three : ∑ s, ((𝟭 A ○ 𝟭 B) s ^ 2 : R) = E[A, B] := by
@@ -113,17 +107,17 @@ lemma thing_three : ∑ s, ((𝟭 A ○ 𝟭 B) s ^ 2 : R) = E[A, B] := by
 
 section lemma1
 
-lemma claim_one : ∑ s, (𝟭_[R] A ○ 𝟭 B) s * (A ∩ (s +ᵥ B)).card = E[A, B] := by
+lemma claim_one : ∑ s, (𝟭_[R] A ○ 𝟭 B) s * #(A ∩ (s +ᵥ B)) = E[A, B] := by
   simp only [← thing_three, ← thing_one_right, sq]
 
 lemma claim_two :
-    (E[A, B]) ^ 2 / (A.card * B.card) ≤ ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (A ∩ (s +ᵥ B)).card ^ 2 := by
+    (E[A, B]) ^ 2 / (#A * #B) ≤ ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * #(A ∩ (s +ᵥ B)) ^ 2 := by
   let f := fun s ↦ ((𝟭_[ℝ] A ○ 𝟭 B) s).sqrt
   have hf : ∀ s, f s ^ 2 = (𝟭_[ℝ] A ○ 𝟭 B) s := by
     intro s
     rw [Real.sq_sqrt]
     exact dconv_nonneg (R := ℝ) indicate_nonneg indicate_nonneg s -- why do I need the annotation??
-  have := sum_mul_sq_le_sq_mul_sq univ f (fun s ↦ f s * (A ∩ (s +ᵥ B)).card)
+  have := sum_mul_sq_le_sq_mul_sq univ f (fun s ↦ f s * #(A ∩ (s +ᵥ B)))
   refine div_le_of_le_mul₀ (by positivity) ?_ ?_
   · refine sum_nonneg fun i _ ↦ ?_
     -- indicate nonneg should be a positivity lemma
@@ -133,8 +127,8 @@ lemma claim_two :
   rw [mul_comm]
 
 lemma claim_three {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) :
-    ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * ((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H).card =
-      ∑ ab in H, ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (𝟭 B (ab.1 - s) * 𝟭 B (ab.2 - s)) := by
+    ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * #((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H) =
+      ∑ ab ∈ H, ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (𝟭 B (ab.1 - s) * 𝟭 B (ab.2 - s)) := by
   simp only [sum_comm (s := H), ← mul_sum]
   refine sum_congr rfl fun x _ ↦ ?_
   congr 1
@@ -146,9 +140,9 @@ lemma claim_three {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) :
 
 lemma claim_four (ab : G × G) :
     ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (𝟭 B (ab.1 - s) * 𝟭 B (ab.2 - s)) ≤
-      B.card * (𝟭 B ○ 𝟭 B) (ab.1 - ab.2) := by
+      #B * (𝟭 B ○ 𝟭 B) (ab.1 - ab.2) := by
   rcases ab with ⟨a, b⟩
-  have : ∀ s, (𝟭_[ℝ] A ○ 𝟭 B) s ≤ B.card := fun s ↦ by
+  have : ∀ s, (𝟭_[ℝ] A ○ 𝟭 B) s ≤ #B := fun s ↦ by
     simp only [dconv_eq_sum_add, conj_indicate_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]
     simp only [indicate_apply, mul_boole, ← sum_filter (· ∈ B), filter_mem_eq_inter, univ_inter]
     refine sum_le_sum fun i _ ↦ ?_
@@ -156,7 +150,7 @@ lemma claim_four (ab : G × G) :
     · rfl
     · exact zero_le_one
   have : ∑ s : G, (𝟭_[ℝ] A ○ 𝟭 B) s * (𝟭 B ((a, b).1 - s) * 𝟭 B ((a, b).2 - s)) ≤
-      B.card * ∑ s : G, (𝟭 B ((a, b).1 - s) * 𝟭 B ((a, b).2 - s)) := by
+      #B * ∑ s : G, (𝟭 B ((a, b).1 - s) * 𝟭 B ((a, b).2 - s)) := by
     rw [mul_sum]
     refine sum_le_sum fun i _ ↦ ?_
     exact mul_le_mul_of_nonneg_right (this _) (mul_nonneg (indicate_nonneg _) (indicate_nonneg _))
@@ -166,48 +160,40 @@ lemma claim_four (ab : G × G) :
   exact Fintype.sum_equiv (Equiv.subLeft b) _ _ $ by simp
 
 lemma claim_five {H : Finset (G × G)} (hH : H ⊆ A ×ˢ A) :
-    ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * ((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H).card ≤
-      B.card * ∑ ab in H, (𝟭 B ○ 𝟭 B) (ab.1 - ab.2) := by
+    ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * #((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H) ≤
+      #B * ∑ ab ∈ H, (𝟭 B ○ 𝟭 B) (ab.1 - ab.2) := by
   rw [claim_three hH, mul_sum]
   exact sum_le_sum fun ab _ ↦ claim_four ab
 
 noncomputable def H_choice (A B : Finset G) (c : ℝ) : Finset (G × G) :=
-  (A ×ˢ A).filter
-    fun ab ↦
-      (𝟭_[ℝ] B ○ 𝟭 B) (ab.1 - ab.2) ≤ c / 2 * (E[A, B] ^ 2 / (A.card ^ 3 * B.card ^ 2))
+  {ab ∈ A ×ˢ A | (𝟭_[ℝ] B ○ 𝟭 B) (ab.1 - ab.2) ≤ c / 2 * (E[A, B] ^ 2 / (#A ^ 3 * #B ^ 2))}
 
--- lemma H_choice_subset :
 lemma claim_six (c : ℝ) (hc : 0 ≤ c) :
-    ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * ((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c).card ≤
-      c / 2 * (E[A, B] ^ 2 / (A.card * B.card)) := by
+    ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * #((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c) ≤
+      c / 2 * (E[A, B] ^ 2 / (#A * #B)) := by
   refine (claim_five (filter_subset _ _)).trans ?_
-  have : ∑ ab in H_choice A B c, (𝟭_[ℝ] B ○ 𝟭 B) (ab.1 - ab.2) ≤
-      (H_choice A B c).card * (c / 2 * (E[A, B] ^ 2 / (A.card ^ 3 * B.card ^ 2))) := by
+  have : ∑ ab ∈ H_choice A B c, (𝟭_[ℝ] B ○ 𝟭 B) (ab.1 - ab.2) ≤
+      #(H_choice A B c) * (c / 2 * (E[A, B] ^ 2 / (#A ^ 3 * #B ^ 2))) := by
     rw [← nsmul_eq_mul]
-    refine sum_le_card_nsmul _ _ _ ?_
-    intro x hx
-    exact (mem_filter.1 hx).2
-  have hA : ((H_choice A B c).card : ℝ) ≤ A.card ^ 2 := by
+    exact sum_le_card_nsmul _ _ _ fun x hx ↦ (mem_filter.1 hx).2
+  have hA : (#(H_choice A B c) : ℝ) ≤ #A ^ 2 := by
     norm_cast
     exact (card_le_card (filter_subset _ _)).trans_eq (by simp [sq])
   refine (mul_le_mul_of_nonneg_left this (by positivity)).trans ?_
-  rcases A.card.eq_zero_or_pos with hA | hA
-  · rw [hA]
-    simp
-  rcases B.card.eq_zero_or_pos with hB | hB
-  · rw [hB]
-    simp
+  obtain rfl | hA := A.eq_empty_or_nonempty
+  · simp
+  obtain rfl | hA := B.eq_empty_or_nonempty
+  · simp
   calc
-    _ ≤ (B.card : ℝ) * (A.card ^ 2 * (c / 2 * (E[A, B] ^ 2 / (A.card ^ 3 * B.card ^ 2))))
-        := by gcongr
-    _ = c / 2 * (E[A, B] ^ 2 / (card A * card B)) := by field_simp; ring
+    _ ≤ (#B : ℝ) * (#A ^ 2 * (c / 2 * (E[A, B] ^ 2 / (#A ^ 3 * #B ^ 2)))) := by gcongr
+    _ = c / 2 * (E[A, B] ^ 2 / (#A * #B)) := by field_simp; ring
 
-lemma claim_seven (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < card A) (hB : (0 : ℝ) < card B) :
+lemma claim_seven (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < #A) (hB : (0 : ℝ) < #B) :
     ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s *
-        ((c / 2) * (E[A, B] ^ 2 / (A.card ^ 2 * B.card ^ 2)) +
-          ((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c).card) ≤
-      ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (c * (A ∩ (s +ᵥ B)).card ^ 2) :=
-  calc _ = (c / 2 * (E[A, B] ^ 2 / (card A * card B))) +
+        ((c / 2) * (E[A, B] ^ 2 / (#A ^ 2 * #B ^ 2)) +
+          #((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c)) ≤
+      ∑ s, (𝟭_[ℝ] A ○ 𝟭 B) s * (c * #(A ∩ (s +ᵥ B)) ^ 2) :=
+  calc _ = (c / 2 * (E[A, B] ^ 2 / (#A * #B))) +
     ∑ x : G, (𝟭_[ℝ] A ○ 𝟭 B) x * (card ((A ∩ (x +ᵥ B)) ×ˢ (A ∩ (x +ᵥ B)) ∩ H_choice A B c)) := by
         simp only [mul_add, sum_add_distrib, ← sum_mul, thing_two, ← mul_pow]
         field_simp
@@ -219,10 +205,10 @@ lemma claim_seven (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < card A) (hB : (0 :
         gcongr
         exact claim_two
 
-lemma claim_eight (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < card A) (hB : (0 : ℝ) < card B) :
-    ∃ s : G, ((c / 2) * (E[A, B] ^ 2 / (A.card ^ 2 * B.card ^ 2)) +
-          ((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c).card) ≤
-      c * (A ∩ (s +ᵥ B)).card ^ 2 := by
+lemma claim_eight (c : ℝ) (hc : 0 ≤ c) (hA : (0 : ℝ) < #A) (hB : (0 : ℝ) < #B) :
+    ∃ s : G, ((c / 2) * (E[A, B] ^ 2 / (#A ^ 2 * #B ^ 2)) +
+          #((A ∩ (s +ᵥ B)) ×ˢ (A ∩ (s +ᵥ B)) ∩ H_choice A B c)) ≤
+      c * #(A ∩ (s +ᵥ B)) ^ 2 := by
   by_contra!
   refine (claim_seven c hc hA hB).not_lt ?_
   refine sum_lt_sum ?_ ?_
@@ -248,17 +234,15 @@ lemma test_case {E A B : ℕ} {K : ℝ} (hK : 0 < K) (hE : K⁻¹ * (A ^ 2 * B)
   field_simp
   ring
 
-lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K)
-  (hE : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B])
-  (hA : (0 : ℝ) < card A) (hB : (0 : ℝ) < card B) :
-    ∃ s : G, ∃ X ⊆ A ∩ (s +ᵥ B), A.card / (Real.sqrt 2 * K) ≤ X.card ∧
-      (1 - c) * X.card ^ 2 ≤
-        ((X ×ˢ X).filter
-          (fun ⟨a, b⟩ ↦ c / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (a - b))).card := by
+lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K) (hE : K⁻¹ * (#A ^ 2 * #B) ≤ E[A, B])
+    (hA : (0 : ℝ) < #A) (hB : (0 : ℝ) < #B) :
+    ∃ s : G, ∃ X ⊆ A ∩ (s +ᵥ B), #A / (Real.sqrt 2 * K) ≤ #X ∧
+      (1 - c) * #X ^ 2 ≤
+        #((X ×ˢ X).filter (fun ⟨a, b⟩ ↦ c / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (a - b))) := by
   obtain ⟨s, hs⟩ := claim_eight c hc.le hA hB
   set X := A ∩ (s +ᵥ B)
   refine ⟨s, X, subset_rfl, ?_, ?_⟩
-  · have : (2 : ℝ)⁻¹ * (E[A, B] / (card A * card B)) ^ 2 ≤ (card X) ^ 2 := by
+  · have : (2 : ℝ)⁻¹ * (E[A, B] / (#A * #B)) ^ 2 ≤ (card X) ^ 2 := by
       refine le_of_mul_le_mul_left ?_ hc
       exact ((le_add_of_nonneg_right (Nat.cast_nonneg _)).trans hs).trans_eq' (by ring)
     replace := Real.sqrt_le_sqrt this
@@ -288,18 +272,17 @@ lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K)
   rw [mul_assoc]
   gcongr _ * ?_
   field_simp [hA, hB, hK, le_div_iff₀, div_le_iff₀] at hE ⊢
-  convert_to (A.card ^ 2 * B.card) ^ 2 ≤ (E[A, B] * K) ^ 2
+  convert_to (#A ^ 2 * #B) ^ 2 ≤ (E[A, B] * K) ^ 2
   · ring_nf
   · ring_nf
   gcongr
 
 lemma lemma_one' {c K : ℝ} (hc : 0 < c) (hK : 0 < K)
-    (hE : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B])
-    (hA : (0 : ℝ) < card A) (hB : (0 : ℝ) < card B) :
-    ∃ s : G, ∃ X ⊆ A ∩ (s +ᵥ B), A.card / (2 * K) ≤ X.card ∧
-      (1 - c) * X.card ^ 2 ≤
-        ((X ×ˢ X).filter
-          (fun ⟨a, b⟩ ↦ c / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (a - b))).card := by
+    (hE : K⁻¹ * (#A ^ 2 * #B) ≤ E[A, B])
+    (hA : (0 : ℝ) < #A) (hB : (0 : ℝ) < #B) :
+    ∃ s : G, ∃ X ⊆ A ∩ (s +ᵥ B), #A / (2 * K) ≤ #X ∧
+      (1 - c) * #X ^ 2 ≤
+        #((X ×ˢ X).filter fun ⟨a, b⟩ ↦ c / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (a - b)) := by
   obtain ⟨s, X, hX₁, hX₂, hX₃⟩ := lemma_one hc hK hE hA hB
   refine ⟨s, X, hX₁, hX₂.trans' ?_, hX₃⟩
   gcongr _ / (?_ * _)
@@ -312,28 +295,27 @@ section lemma2
 
 open Pointwise
 
-lemma many_pairs {K : ℝ} {x : G}
-    (hab : (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) x) :
-    A.card / (2 ^ 4 * K ^ 2) ≤ ((B ×ˢ B).filter (fun ⟨c, d⟩ ↦ c - d = x)).card :=
-  calc _ = (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card := by ring
-       _ ≤ (𝟭 B ○ 𝟭 B) x := hab
-       _ ≤ ((B ×ˢ B).filter (fun ⟨c, d⟩ ↦ c - d = x)).card := by
-          rw [indicate_dconv_indicate_apply _ _ _]
+lemma many_pairs {K : ℝ} {x : G} (hab : (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) x) :
+    #A / (2 ^ 4 * K ^ 2) ≤ #((B ×ˢ B).filter fun ⟨c, d⟩ ↦ c - d = x) :=
+  calc
+    _ = (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A := by ring
+    _ ≤ (𝟭 B ○ 𝟭 B) x := hab
+    _ ≤ #((B ×ˢ B).filter fun ⟨c, d⟩ ↦ c - d = x) := by rw [indicate_dconv_indicate_apply]
 
 variable {H : Finset (G × G)} {X : Finset G}
 
 lemma quadruple_bound_part {K : ℝ} (a c : G)
-    (hac : (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (a - c)) :
-    A.card / (2 ^ 4 * K ^ 2) ≤ ((B ×ˢ B).filter fun ⟨a₁, a₂⟩ ↦ a₁ - a₂ = a - c).card :=
+    (hac : (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (a - c)) :
+    #A / (2 ^ 4 * K ^ 2) ≤ #((B ×ˢ B).filter fun ⟨a₁, a₂⟩ ↦ a₁ - a₂ = a - c) :=
   many_pairs hac
 
 lemma quadruple_bound_other {a b c : G} {K : ℝ} {H : Finset (G × G)}
     (hac : (a, c) ∈ H) (hbc : (b, c) ∈ H)
-    (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) :
-    (A.card / (2 ^ 4 * K ^ 2)) ^ 2 ≤ (((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦
-        a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c).card := by
-  change (_ : ℝ) ≤ (((B ×ˢ B) ×ˢ B ×ˢ B).filter fun (z : (G × G) × G × G) ↦
-    z.1.1 - z.1.2 = a - c ∧ z.2.1 - z.2.2 = b - c).card
+    (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2)) :
+    (#A / (2 ^ 4 * K ^ 2)) ^ 2 ≤ #(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦
+        a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c) := by
+  change (_ : ℝ) ≤ #(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun (z : (G × G) × G × G) ↦
+    z.1.1 - z.1.2 = a - c ∧ z.2.1 - z.2.2 = b - c)
   rw [filter_product (s := B ×ˢ B) (t := B ×ˢ B) (fun z ↦ z.1 - z.2 = a - c)
     (fun z ↦ z.1 - z.2 = b - c), card_product, sq, Nat.cast_mul]
   gcongr ?_ * ?_
@@ -342,29 +324,29 @@ lemma quadruple_bound_other {a b c : G} {K : ℝ} {H : Finset (G × G)}
 
 lemma quadruple_bound_left {a b : G} {K : ℝ} {H : Finset (G × G)}
     (ha : a ∈ oneOfPair H X) (hb : b ∈ oneOfPair H X)
-    (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2))
+    (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2))
     (hH' : H ⊆ X ×ˢ X) :
-    ((X.card : ℝ) / 2) * (A.card / (2 ^ 4 * K ^ 2)) ^ 2 ≤
-      ((X.filter fun c ↦ (a, c) ∈ H ∧ (b, c) ∈ H).sigma fun c ↦
+    #X / 2 * (#A / (2 ^ 4 * K ^ 2)) ^ 2 ≤
+      #({c ∈ X | (a, c) ∈ H ∧ (b, c) ∈ H}.sigma fun c ↦
       ((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦
-        a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c).card :=
-  calc _ ≤ ∑ _x in X.filter fun c ↦ (a, c) ∈ H ∧ (b, c) ∈ H,
-            ((A.card / (2 ^ 4 * K ^ 2)) ^ 2 : ℝ) := by
-                rw [sum_const, nsmul_eq_mul]
-                gcongr ?_ * _
-                exact quadruple_bound_c ha hb hH'
-       _ ≤ ∑ c in X.filter fun c ↦ (a, c) ∈ H ∧ (b, c) ∈ H,
-            ((((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ((a₁, a₂), a₃, a₄) ↦
-                a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c).card : ℝ) := sum_le_sum <| fun i hi ↦ by
-            simp only [not_and, mem_filter] at hi
-            exact quadruple_bound_other hi.2.1 hi.2.2 hH
-       _ = _ := by rw [card_sigma, Nat.cast_sum]
+        a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c) :=
+  calc
+    _ ≤ ∑ c ∈ X with (a, c) ∈ H ∧ (b, c) ∈ H, ((#A / (2 ^ 4 * K ^ 2)) ^ 2 : ℝ) := by
+      rw [sum_const, nsmul_eq_mul]
+      gcongr ?_ * _
+      exact quadruple_bound_c ha hb hH'
+    _ ≤ ∑ c ∈ X with (a, c) ∈ H ∧ (b, c) ∈ H, (#(((B ×ˢ B) ×ˢ B ×ˢ B).filter
+        fun ((a₁, a₂), a₃, a₄) ↦ a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c) : ℝ) := by
+      gcongr with i hi
+      simp only [not_and, mem_filter] at hi
+      exact quadruple_bound_other hi.2.1 hi.2.2 hH
+    _ = _ := by rw [card_sigma, Nat.cast_sum]
 
 lemma quadruple_bound {K : ℝ} {x : G} (hx : x ∈ oneOfPair H X - oneOfPair H X)
-    (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2))
+    (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2))
     (hH' : H ⊆ X ×ˢ X) :
-    (A.card ^ 2 * X.card) / (2 ^ 9 * K ^ 4) ≤
-      (((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x).card := by
+    (#A ^ 2 * #X) / (2 ^ 9 * K ^ 4) ≤
+      #(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x) := by
   rw [mem_sub] at hx
   obtain ⟨a, ha, b, hb, rfl⟩ := hx
   refine (quadruple_bound_right H X rfl).trans' ?_
@@ -372,38 +354,35 @@ lemma quadruple_bound {K : ℝ} {x : G} (hx : x ∈ oneOfPair H X - oneOfPair H
   ring
 
 lemma big_quadruple_bound {K : ℝ}
-    (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2))
+    (hH : ∀ x ∈ H, (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (x.1 - x.2))
     (hH' : H ⊆ X ×ˢ X)
-    (hX : A.card / (2 * K) ≤ X.card) :
-    ((oneOfPair H X - oneOfPair H X).card) * (A.card ^ 3 / (2 ^ 10 * K ^ 5)) ≤
-      B.card ^ 4 :=
-  calc _ = ((oneOfPair H X - oneOfPair H X).card) *
-                ((A.card ^ 2 * (A.card / (2 * K))) / (2 ^ 9 * K ^ 4)) := by ring
-       _ ≤ ((oneOfPair H X - oneOfPair H X).card) *
-                ((A.card ^ 2 * X.card) / (2 ^ 9 * K ^ 4)) := by gcongr
-       _ = ∑ _x in oneOfPair H X - oneOfPair H X,
-            ((A.card ^ 2 * X.card) / (2 ^ 9 * K ^ 4) : ℝ) := by simp
-       _ ≤ ∑ x in oneOfPair H X - oneOfPair H X,
-          ((((B ×ˢ B) ×ˢ B ×ˢ B).filter
-            fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x).card : ℝ) :=
-              sum_le_sum fun x hx ↦ quadruple_bound hx hH hH'
-       _ ≤ ∑ x, ((((B ×ˢ B) ×ˢ B ×ˢ B).filter
-            fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x).card : ℝ) :=
-              sum_le_sum_of_subset_of_nonneg (subset_univ _) (fun _ _ _ ↦ by positivity)
-       _ = _ := by
-          rw [← Nat.cast_sum, ← card_eq_sum_card_fiberwise]
-          · simp only [card_product, Nat.cast_mul]
-            ring_nf
-          · simp
-
-theorem BSG_aux {K : ℝ} (hK : 0 < K) (hA : (0 : ℝ) < A.card) (hB : (0 : ℝ) < B.card)
-    (hAB : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B]) :
-    ∃ s : G, ∃ A' ⊆ A ∩ (s +ᵥ B), (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ A'.card ∧
-    (A' - A').card ≤ 2 ^ 10 * K ^ 5 * B.card ^ 4 / A.card ^ 3 := by
+    (hX : #A / (2 * K) ≤ #X) :
+    (#(oneOfPair H X - oneOfPair H X)) * (#A ^ 3 / (2 ^ 10 * K ^ 5)) ≤ #B ^ 4 :=
+  calc
+    _ = (#(oneOfPair H X - oneOfPair H X)) * ((#A ^ 2 * (#A / (2 * K))) / (2 ^ 9 * K ^ 4)) := by
+      ring
+    _ ≤ (#(oneOfPair H X - oneOfPair H X)) * ((#A ^ 2 * #X) / (2 ^ 9 * K ^ 4)) := by gcongr
+    _ = ∑ _x ∈ oneOfPair H X - oneOfPair H X, ((#A ^ 2 * #X) / (2 ^ 9 * K ^ 4) : ℝ) := by simp
+    _ ≤ ∑ x ∈ oneOfPair H X - oneOfPair H X,
+          (#(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x) : ℝ) :=
+      sum_le_sum fun x hx ↦ quadruple_bound hx hH hH'
+    _ ≤ ∑ x, (#(((B ×ˢ B) ×ˢ B ×ˢ B).filter
+          fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = x) : ℝ) := by
+      gcongr; exact subset_univ _
+    _ = _ := by
+      rw [← Nat.cast_sum, ← card_eq_sum_card_fiberwise]
+      · simp only [card_product, Nat.cast_mul]
+        ring_nf
+      · simp
+
+theorem BSG_aux {K : ℝ} (hK : 0 < K) (hA : (0 : ℝ) < #A) (hB : (0 : ℝ) < #B)
+    (hAB : K⁻¹ * (#A ^ 2 * #B) ≤ E[A, B]) :
+    ∃ s : G, ∃ A' ⊆ A ∩ (s +ᵥ B), (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #A' ∧
+    #(A' - A') ≤ 2 ^ 10 * K ^ 5 * #B ^ 4 / #A ^ 3 := by
   obtain ⟨s, X, hX₁, hX₂, hX₃⟩ := lemma_one' (c := 1 / 8) (by norm_num) hK hAB hA hB
   set H : Finset (G × G) := (X ×ˢ X).filter
-    fun ⟨a, b⟩ ↦ (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * A.card ≤ (𝟭 B ○ 𝟭 B) (a - b)
-  have : (0 : ℝ) < X.card := hX₂.trans_lt' (by positivity)
+    fun ⟨a, b⟩ ↦ (1 / 8 : ℝ) / 2 * (K ^ 2)⁻¹ * #A ≤ (𝟭 B ○ 𝟭 B) (a - b)
+  have : (0 : ℝ) < #X := hX₂.trans_lt' (by positivity)
   refine ⟨s, oneOfPair H X, (filter_subset _ _).trans hX₁, ?_, ?_⟩
   · rw [← mul_inv, inv_mul_eq_div]
     exact oneOfPair_bound (filter_subset _ _) this (hX₃.trans_eq' (by norm_num)) hX₂
@@ -412,9 +391,8 @@ theorem BSG_aux {K : ℝ} (hK : 0 < K) (hA : (0 : ℝ) < A.card) (hB : (0 : ℝ)
   rw [mul_div_assoc', div_le_iff₀ (by positivity)] at this
   exact this.trans_eq (by ring)
 
-theorem BSG {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B]) :
-    ∃ A' ⊆ A, (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ A'.card ∧
-      (A' - A').card ≤ 2 ^ 10 * K ^ 5 * B.card ^ 4 / A.card ^ 3 := by
+theorem BSG {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (#A ^ 2 * #B) ≤ E[A, B]) :
+    ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #A' ∧ #(A' - A') ≤ 2 ^ 10 * K ^ 5 * #B ^ 4 / #A ^ 3 := by
   obtain rfl | hA := A.eq_empty_or_nonempty
   · exact ⟨∅, by simp⟩
   obtain rfl | hK := eq_or_lt_of_le hK
@@ -422,10 +400,9 @@ theorem BSG {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.card ^
   · obtain ⟨s, A', hA, h⟩ := BSG_aux hK (by simpa [card_pos]) (by simpa [card_pos]) hAB
     exact ⟨A', hA.trans (inter_subset_left ..), h⟩
 
-theorem BSG₂ {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.card ^ 2 * B.card) ≤ E[A, B]) :
-    ∃ A' ⊆ A, ∃ B' ⊆ B, (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ A'.card ∧
-    (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ B'.card ∧
-      (A' - B').card ≤ 2 ^ 10 * K ^ 5 * B.card ^ 4 / A.card ^ 3 := by
+theorem BSG₂ {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (#A ^ 2 * #B) ≤ E[A, B]) :
+    ∃ A' ⊆ A, ∃ B' ⊆ B, (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #A' ∧
+      (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #B' ∧ #(A' - B') ≤ 2 ^ 10 * K ^ 5 * #B ^ 4 / #A ^ 3 := by
   obtain rfl | hA := A.eq_empty_or_nonempty
   · exact ⟨∅, by simp, ∅, by simp⟩
   obtain rfl | hK := eq_or_lt_of_le hK
@@ -442,9 +419,8 @@ theorem BSG₂ {K : ℝ} (hK : 0 ≤ K) (hB : B.Nonempty) (hAB : K⁻¹ * (A.car
     rw [add_vadd_comm]
     apply card_vadd_finset
 
-theorem BSG_self {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * A.card ^ 3 ≤ E[A]) :
-    ∃ A' ⊆ A, (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ A'.card ∧
-      (A' - A').card ≤ 2 ^ 10 * K ^ 5 * A.card := by
+theorem BSG_self {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * #A ^ 3 ≤ E[A]) :
+    ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #A' ∧ #(A' - A') ≤ 2 ^ 10 * K ^ 5 * #A := by
   convert BSG hK hA ?_ using 5
   · have := hA.card_pos
     field_simp
@@ -452,13 +428,12 @@ theorem BSG_self {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * A.ca
   · ring_nf
     assumption
 
-theorem BSG_self' {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * A.card ^ 3 ≤ E[A]) :
-    ∃ A' ⊆ A, (2 ^ 4 : ℝ)⁻¹ * K⁻¹ * A.card ≤ A'.card ∧
-      (A' - A').card ≤ 2 ^ 14 * K ^ 6 * A'.card := by
+theorem BSG_self' {K : ℝ} (hK : 0 ≤ K) (hA : A.Nonempty) (hAK : K⁻¹ * #A ^ 3 ≤ E[A]) :
+    ∃ A' ⊆ A, (2 ^ 4)⁻¹ * K⁻¹ * #A ≤ #A' ∧ #(A' - A') ≤ 2 ^ 14 * K ^ 6 * #A' := by
   obtain ⟨A', hA', hAA', hAK'⟩ := BSG_self hK hA hAK
   refine ⟨A', hA', hAA', hAK'.trans ?_⟩
   calc
-    _ = 2 ^ 14 * K ^ 6 * ((2 ^ 4)⁻¹ * K⁻¹ * A.card) := ?_
+    _ = 2 ^ 14 * K ^ 6 * ((2 ^ 4)⁻¹ * K⁻¹ * #A) := ?_
     _ ≤ _ := by gcongr
   obtain rfl | hK := hK.eq_or_lt
   · simp
diff --git a/LeanAPAP/FiniteField.lean b/LeanAPAP/FiniteField.lean
index 7de83ce29c..c38d97bfa7 100644
--- a/LeanAPAP/FiniteField.lean
+++ b/LeanAPAP/FiniteField.lean
@@ -158,7 +158,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
       _ ≤ 1 := by linarith
   obtain ⟨T, hTcard, hTε⟩ := AlmostPeriodicity.linfty_almost_periodicity_boosted ε hε₀ hε₁ k
     (by positivity) (le_inv_of_le_inv₀ (by positivity) hα₂) hA₁ univ_nonempty S A₂ hS hA₂
-  have hT : 0 < (T.card : ℝ) := hTcard.trans_lt' (by positivity)
+  have hT : 0 < (#T : ℝ) := hTcard.trans_lt' (by positivity)
   replace hT : T.Nonempty := by simpa using hT
   let Δ := largeSpec (μ T) 2⁻¹
   let V : Submodule (ZMod q) G := AddSubgroup.toZModSubmodule _ $ ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker
@@ -170,9 +170,9 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
     have hWV : W ≤ V := by sorry
     have :=
       calc
-        log T.dens⁻¹ ≤ log (α⁻¹ ^ (-4096 * ⌈𝓛 (min 1 (A₂.card / S.card))⌉ * k ^ 2 / ε ^ 2))⁻¹ := by
+        log T.dens⁻¹ ≤ log (α⁻¹ ^ (-4096 * ⌈𝓛 (min 1 (#A₂ / #S))⌉ * k ^ 2 / ε ^ 2))⁻¹ := by
           gcongr; rwa [nnratCast_dens, le_div_iff₀]; positivity
-        _ = 2 ^ 12 * log α⁻¹ * ⌈𝓛 (min 1 (A₂.card / S.card))⌉ * k ^ 2 / ε ^ 2 := by
+        _ = 2 ^ 12 * log α⁻¹ * ⌈𝓛 (min 1 (#A₂ / #S))⌉ * k ^ 2 / ε ^ 2 := by
           rw [log_inv, log_rpow (by positivity)]; ring_nf
         _ ≤ 2 ^ 12 * log α⁻¹ * ⌈𝓛 (min 1 A₂.dens)⌉ * k ^ 2 / ε ^ 2 := by
           rw [nnratCast_dens, ← card_univ]; gcongr; exact S.subset_univ
@@ -194,7 +194,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
       (↑(finrank (ZMod q) G - finrank (ZMod q) V) : ℝ)
         ≤ ↑(finrank (ZMod q) G - finrank (ZMod q) W) := by
         gcongr; exact Submodule.finrank_mono hWV
-      _ ≤ Δ'.card := sorry
+      _ ≤ #Δ' := sorry
       _ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖μ T‖_[1] ^ 2 / ‖μ T‖_[2] ^ 2 / card G)⌉₊ / 2⁻¹ ^ 2⌉₊ := by
         gcongr
       _ = ⌈2 ^ 7 * exp 1 ^ 2 * ⌈𝓛 T.dens⌉₊⌉₊ := by
diff --git a/LeanAPAP/Integer.lean b/LeanAPAP/Integer.lean
index 65123147ef..41af146e92 100644
--- a/LeanAPAP/Integer.lean
+++ b/LeanAPAP/Integer.lean
@@ -4,4 +4,4 @@ import Mathlib.Combinatorics.Additive.AP.Three.Defs
 open Finset Real
 
 theorem int {A : Finset ℕ} {N : ℕ} (hAN : A ⊆ range N) (hA : ThreeAPFree (α := ℕ) A) :
-    ∃ c > 0, A.card ≤ N / exp (- c * log N ^ (12⁻¹ : ℝ)) := sorry
+    ∃ c > 0, #A ≤ N / exp (- c * log N ^ (12⁻¹ : ℝ)) := sorry
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index 8aac4a5e15..9f010181f7 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -20,8 +20,8 @@ section Add
 variable [Add α]
 
 lemma big_shifts_step1 (L : Finset (Fin k → α)) (hk : k ≠ 0) :
-    ∑ x in L + s.piDiag (Fin k), ∑ l in L, ∑ s in s.piDiag (Fin k), (if l + s = x then 1 else 0)
-      = L.card * s.card := by
+    ∑ x ∈ L + s.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ s.piDiag (Fin k), (if l + s = x then 1 else 0)
+      = #L * #s := by
   simp only [@sum_comm _ _ _ _ (L + _), sum_ite_eq]
   rw [sum_const_nat]
   intro l hl
@@ -34,10 +34,9 @@ end Add
 variable [AddCommGroup α] [Fintype α]
 
 lemma reindex_count (L : Finset (Fin k → α)) (hk : k ≠ 0) (hL' : L.Nonempty) (l₁ : Fin k → α) :
-    ∑ l₂ in L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 =
-      (univ.filter fun t ↦ (l₁ - fun _ ↦ t) ∈ L).card :=
+    ∑ l₂ ∈ L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 = #{t | (l₁ - fun _ ↦ t) ∈ L} :=
   calc
-    _ = ∑ l₂ in L, ∑ t : α, ite ((l₁ - fun _ ↦ t) = l₂) 1 0 := by
+    _ = ∑ l₂ ∈ L, ∑ t : α, ite ((l₁ - fun _ ↦ t) = l₂) 1 0 := by
       refine sum_congr rfl fun l₂ hl₂ ↦ ?_
       rw [Fintype.sum_ite_eq_ite_exists]
       simp only [mem_piDiag, mem_univ, eq_sub_iff_add_eq, true_and, sub_eq_iff_eq_add',
@@ -47,7 +46,7 @@ lemma reindex_count (L : Finset (Fin k → α)) (hk : k ≠ 0) (hL' : L.Nonempty
       cases k
       · simp at hk
       · simpa using congr_fun h 0
-    _ = (univ.filter fun t ↦ (l₁ - fun _ ↦ t) ∈ L).card := by
+    _ = #{t | (l₁ - fun _ ↦ t) ∈ L} := by
       simp only [sum_comm, sum_ite_eq, card_eq_sum_ones, sum_filter]
 
 end Finset
@@ -56,8 +55,8 @@ section
 variable {α : Type*} {g : α → ℝ} {c ε : ℝ} {A : Finset α}
 
 open Finset
-lemma my_markov (hc : 0 < c) (hg : ∀ a ∈ A, 0 ≤ g a) (h : ∑ a in A, g a ≤ ε * c * A.card) :
-    (1 - ε) * A.card ≤ (A.filter (g · ≤ c)).card := by
+lemma my_markov (hc : 0 < c) (hg : ∀ a ∈ A, 0 ≤ g a) (h : ∑ a ∈ A, g a ≤ ε * c * #A) :
+    (1 - ε) * #A ≤ #{a ∈ A | g a ≤ c} := by
   classical
   have := h.trans'
     (sum_le_sum_of_subset_of_nonneg (filter_subset (¬g · ≤ c) A) fun i hi _ ↦ hg _ hi)
@@ -69,7 +68,7 @@ lemma my_markov (hc : 0 < c) (hg : ∀ a ∈ A, 0 ≤ g a) (h : ∑ a in A, g a
   linarith only [this]
 
 lemma my_other_markov (hc : 0 ≤ c) (hε : 0 ≤ ε) (hg : ∀ a ∈ A, 0 ≤ g a)
-    (h : ∑ a in A, g a ≤ ε * c * A.card) : (1 - ε) * A.card ≤ (A.filter (g · ≤ c)).card := by
+    (h : ∑ a ∈ A, g a ≤ ε * c * #A) : (1 - ε) * #A ≤ #{a ∈ A | g a ≤ c} := by
   rcases hc.lt_or_eq with (hc | rfl)
   · exact my_markov hc hg h
   simp only [mul_zero, zero_mul] at h
@@ -98,16 +97,16 @@ section
 variable [MeasurableSpace G] [DiscreteMeasurableSpace G]
 
 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
+    (8 * m) ^ m * k ^ (m - 1) * #A ^ k * k * (2 * ‖f‖_[2 * m] : ℝ) ^ (2 * m) ≤
+      1 / 2 * ((k * ε) ^ (2 * m) * ∑ i : G, ‖f i‖ ^ (2 * m)) * #A ^ k := by
   have hmeq : ((2 * m : ℕ) : ℝ≥0∞) = 2 * m := by rw [Nat.cast_mul, Nat.cast_two]
   have hm' : 2 * m ≠ 0 := by
     refine mul_ne_zero two_pos.ne' ?_
     rw [← pos_iff_ne_zero, ← Nat.succ_le_iff]
     exact hm
   rw [mul_pow (2 : ℝ), ← hmeq, ← dLpNorm_pow_eq_sum_norm hm' f, ← mul_assoc, ← mul_assoc,
-    mul_right_comm _ (A.card ^ k : ℝ), mul_right_comm _ (A.card ^ k : ℝ),
-    mul_right_comm _ (A.card ^ k : ℝ)]
+    mul_right_comm _ (#A ^ k : ℝ), mul_right_comm _ (#A ^ k : ℝ),
+    mul_right_comm _ (#A ^ k : ℝ)]
   gcongr ?_ * _ * _
   rw [mul_assoc (_ ^ m : ℝ), ← pow_succ, Nat.sub_add_cancel hm, pow_mul, pow_mul, ← mul_pow,
     ← mul_pow]
@@ -132,9 +131,9 @@ variable [DecidableEq G] [AddCommGroup G]
 local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
 
 lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
-    ∑ a in A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤
+    ∑ a ∈ A ^^ k, ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤
       (8 * m) ^ m * k ^ (m - 1) *
-        ∑ a in A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := by
+        ∑ a ∈ A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) := by
   let f' : G → ℂ := fun a ↦ f (x - a) - (mu A ∗ f) x
   refine (RCLike.marcinkiewicz_zygmund (by linarith only [hm]) f' ?_).trans_eq' ?_
   · intro i
@@ -147,22 +146,22 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
   simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin]
 
 lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) :
-    (∑ x in L + S.piDiag (Fin k), ∑ l in L, ∑ s in S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2
-      ≤ (L + S.piDiag (Fin k)).card * S.card *
-        ∑ l₁ in L, ∑ l₂ in L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by
+    (∑ x ∈ L + S.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2
+      ≤ #(L + S.piDiag (Fin k)) * #S *
+        ∑ l₁ ∈ L, ∑ l₂ ∈ L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by
   refine sq_sum_le_card_mul_sum_sq.trans ?_
   simp_rw [sq, sum_mul, @sum_comm _ _ _ _ (L + S.piDiag (Fin k)), boole_mul, sum_ite_eq, mul_assoc]
   refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg _)
   have : ∀ f : (Fin k → G) → (Fin k → G) → ℝ,
-    ∑ x in L, ∑ y in S.piDiag (Fin k), (if x + y ∈ L + S.piDiag (Fin k) then f x y else 0) =
-      ∑ x in L, ∑ y in S.piDiag (Fin k), f x y := by
+    ∑ x ∈ L, ∑ y ∈ S.piDiag (Fin k), (if x + y ∈ L + S.piDiag (Fin k) then f x y else 0) =
+      ∑ x ∈ L, ∑ y ∈ S.piDiag (Fin k), f x y := by
     refine fun f ↦ sum_congr rfl fun x hx ↦ ?_
     exact sum_congr rfl fun y hy ↦ if_pos $ add_mem_add hx hy
   rw [this]
   have (x y) :
-      ∑ s₁ in S.piDiag (Fin k), ∑ s₂ in S.piDiag (Fin k), ite (y + s₂ = x + s₁) (1 : ℝ) 0 =
+      ∑ s₁ ∈ S.piDiag (Fin k), ∑ s₂ ∈ S.piDiag (Fin k), ite (y + s₂ = x + s₁) (1 : ℝ) 0 =
         ite (x - y ∈ univ.piDiag (Fin k)) 1 0 *
-          ∑ s₁ in S.piDiag (Fin k), ∑ s₂ in S.piDiag (Fin k), ite (s₂ = x + s₁ - y) 1 0 := by
+          ∑ s₁ ∈ S.piDiag (Fin k), ∑ s₂ ∈ S.piDiag (Fin k), ite (s₂ = x + s₁ - y) 1 0 := by
     simp_rw [mul_sum, boole_mul, ← ite_and]
     refine sum_congr rfl fun s₁ hs₁ ↦ ?_
     refine sum_congr rfl fun s₂ hs₂ ↦ ?_
@@ -176,10 +175,10 @@ lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) :
     obtain ⟨j, -, rfl⟩ := hs₂
     exact mem_image.2 ⟨j - i, mem_univ _, rfl⟩
   simp_rw [@sum_comm _ _ _ _ (S.piDiag (Fin k)) L, this, sum_ite_eq']
-  have : ∑ x in L, ∑ y in L,
+  have : ∑ x ∈ L, ∑ y ∈ L,
         ite (x - y ∈ univ.piDiag (Fin k)) (1 : ℝ) 0 *
-          ∑ z in S.piDiag (Fin k), ite (x + z - y ∈ S.piDiag (Fin k)) 1 0 ≤
-      ∑ x in L, ∑ y in L, ite (x - y ∈ univ.piDiag (Fin k)) 1 0 * (S.card : ℝ) := by
+          ∑ z ∈ S.piDiag (Fin k), ite (x + z - y ∈ S.piDiag (Fin k)) 1 0 ≤
+      ∑ x ∈ L, ∑ y ∈ L, ite (x - y ∈ univ.piDiag (Fin k)) 1 0 * (#S : ℝ) := by
     refine sum_le_sum fun l₁ _ ↦ sum_le_sum fun l₂ _ ↦ ?_
     refine mul_le_mul_of_nonneg_left ?_ (by split_ifs <;> norm_num)
     refine (sum_le_card_nsmul _ _ 1 ?_).trans_eq ?_
@@ -196,11 +195,11 @@ lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) :
 lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0)
     (hL' : L.Nonempty) (hL : L ⊆ A ^^ k) :
     ∃ a : Fin k → G, a ∈ L ∧
-      L.card * S.card ≤ (A + S).card ^ k * (univ.filter fun t : G ↦ (a - fun _ ↦ t) ∈ L).card := by
+      #L * #S ≤ #(A + S) ^ k * #{t | (a - fun _ ↦ t) ∈ L} := by
   rcases S.eq_empty_or_nonempty with (rfl | hS)
   · simpa only [card_empty, mul_zero, zero_le', and_true] using hL'
-  have hS' : 0 < S.card := by rwa [card_pos]
-  have : (L + S.piDiag (Fin k)).card ≤ (A + S).card ^ k := by
+  have hS' : 0 < #S := by rwa [card_pos]
+  have : #(L + S.piDiag _) ≤ #(A + S) ^ k := by
     refine (card_le_card (add_subset_add_right hL)).trans ?_
     rw [← Fintype.card_piFinset_const]
     refine card_le_card fun i hi ↦ ?_
@@ -209,13 +208,11 @@ lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0)
     obtain ⟨y, hy, a, ha, rfl⟩ := hi
     intro j
     exact ⟨y j, hy _, a, ha, rfl⟩
-  rsuffices ⟨a, ha, h⟩ : ∃ a ∈ L,
-    L.card * S.card ≤ (L + S.piDiag (Fin k)).card * (univ.filter fun t ↦ (a - fun _ ↦ t) ∈ L).card
+  rsuffices ⟨a, ha, h⟩ : ∃ a ∈ L, #L * #S ≤ #(L + S.piDiag _) * #{t | (a - fun _ ↦ t) ∈ L}
   · exact ⟨a, ha, h.trans (Nat.mul_le_mul_right _ this)⟩
   clear! A
-  have : L.card ^ 2 * S.card ≤
-    (L + S.piDiag (Fin k)).card *
-      ∑ l₁ in L, ∑ l₂ in L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by
+  have : #L ^ 2 * #S ≤
+      #(L + S.piDiag _) * ∑ l₁ ∈ L, ∑ l₂ ∈ L, ite (l₁ - l₂ ∈ univ.piDiag (Fin k)) 1 0 := by
     refine Nat.le_of_mul_le_mul_left ?_ hS'
     rw [mul_comm, mul_assoc, ← sq, ← mul_pow, mul_left_comm, ← mul_assoc, ← big_shifts_step1 L hk]
     exact_mod_cast @big_shifts_step2 G _ _ _ _ _ L hk
@@ -235,13 +232,13 @@ def LProp (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) (a : Fin k → G
 noncomputable instance : DecidablePred (LProp k m ε f A) := Classical.decPred _
 
 noncomputable def l (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) : Finset (Fin k → G) :=
-  (A ^^ k).filter (LProp k m ε f A)
+  {x ∈ A ^^ k | LProp k m ε f A x}
 
 lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
-    (h : ∑ a in A ^^ k,
+    (h : ∑ a ∈ A ^^ k,
         (‖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
+      1 / 2 * (k * ε * ‖f‖_[2 * m]) ^ (2 * m) * #A ^ k) :
+    (#A ^ k : ℝ) / 2 ≤ #(l k m ε f A) := by
   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
@@ -254,8 +251,8 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
 variable [DiscreteMeasurableSpace G]
 
 lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) :
-    (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
-      (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i : Fin k, (2 * ‖f‖_[2 * m]) ^ (2 * m) := by
+    (8 * m) ^ m * k ^ (m - 1) * ∑ a ∈ A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
+      (8 * m) ^ m * k ^ (m - 1) * ∑ a ∈ A ^^ k, ∑ 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 := (Nat.mul_le_mul_left 2 hm).trans_lt' $ by norm_num1
@@ -273,7 +270,7 @@ lemma lemma28_part_two (hm : 1 ≤ m) (hA : A.Nonempty) :
   rw [dL1Norm_mu hA, mul_one]
 
 lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k) :
-    (A.card ^ k : ℝ) / 2 ≤ (l k m ε f A).card := by
+    (#A ^ k : ℝ) / 2 ≤ #(l k m ε f A) := by
   have : 0 < k := by
     rw [← @Nat.cast_pos ℝ]
     refine hk.trans_lt' ?_
@@ -288,10 +285,10 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k)
   rw [← hmeq, mul_pow]
   simp only [dLpNorm_pow_eq_sum_norm hm']
   rw [sum_comm]
-  have : ∀ x : G, ∑ a in A ^^ k,
+  have : ∀ x : G, ∑ a ∈ A ^^ k,
       ‖∑ i, f (x - a i) - (k • (mu A ∗ f)) x‖ ^ (2 * m) ≤
     (8 * m) ^ m * k ^ (m - 1) *
-      ∑ a in A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) :=
+      ∑ a ∈ A ^^ k, ∑ i, ‖f (x - a i) - (mu A ∗ f) x‖ ^ (2 * m) :=
     lemma28_part_one hm
   refine (sum_le_sum fun x _ ↦ this x).trans ?_
   rw [← mul_sum]
@@ -302,8 +299,8 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k)
     simp only [Pi.sub_apply, translate_apply]
   simp only [this]
   have :
-    (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
-      (8 * m) ^ m * k ^ (m - 1) * ∑ a in A ^^ k, ∑ i, (2 * ‖f‖_[2 * m]) ^ (2 * m) :=
+    (8 * m) ^ m * k ^ (m - 1) * ∑ a ∈ A ^^ k, ∑ i, ‖τ (a i) f - mu A ∗ f‖_[2 * m] ^ (2 * m) ≤
+      (8 * m) ^ m * k ^ (m - 1) * ∑ a ∈ A ^^ k, ∑ i, (2 * ‖f‖_[2 * m]) ^ (2 * m) :=
     lemma28_part_two hm hA
   refine le_trans (mod_cast this) ?_
   simp only [sum_const, Fintype.card_piFinset_const, nsmul_eq_mul, Nat.cast_pow]
@@ -391,7 +388,7 @@ lemma T_bound (hK₂ : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ)
 lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (f : G → ℂ)
     (hK₂ : 2 ≤ K) (hK : σ[A, S] ≤ K) :
     ∃ T : Finset G,
-      K ^ (-512 * m / ε ^ 2 : ℝ) * S.card ≤ T.card ∧
+      K ^ (-512 * m / ε ^ 2 : ℝ) * #S ≤ #T ∧
         ∀ t ∈ T, ‖τ t (mu A ∗ f) - mu A ∗ f‖_[2 * m] ≤ ε * ‖f‖_[2 * m] := by
   obtain rfl | hm := m.eq_zero_or_pos
   · exact ⟨S, by simp⟩
@@ -409,14 +406,14 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (
   let k := ⌈(64 : ℝ) * m / (ε / 2) ^ 2⌉₊
   have hk : k ≠ 0 := by positivity
   let L := l k m (ε / 2) f A
-  have : (A.card : ℝ) ^ k / 2 ≤ L.card := lemma28 (half_pos hε) hm (Nat.le_ceil _)
+  have : (#A : ℝ) ^ k / 2 ≤ #L := lemma28 (half_pos hε) hm (Nat.le_ceil _)
   have hL : L.Nonempty := by
     rw [← card_pos, ← @Nat.cast_pos ℝ]
     exact this.trans_lt' (by positivity)
   obtain ⟨a, ha, hL'⟩ := big_shifts S _ hk hL (filter_subset _ _)
-  refine ⟨univ.filter fun t : G ↦ (a + fun _ ↦ -t) ∈ L, ?_, ?_⟩
+  refine ⟨({t | (a + fun _ ↦ -t) ∈ L} : Finset _), ?_, ?_⟩
   · simp_rw [sub_eq_add_neg] at hL'
-    exact T_bound hK₂ L.card S.card A.card (A + S).card _ rfl hL' this
+    exact T_bound hK₂ #L #S #A #(A + S) _ rfl hL' this
       (by rw [← cast_addConst_mul_card]; gcongr) hA.card_pos hε hε' hm
   intro t ht
   simp only [exists_prop, exists_eq_right, mem_filter, mem_univ, true_and] at ht
@@ -426,10 +423,10 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (
 theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hK₂ : 2 ≤ K)
     (hK : σ[A, S] ≤ K) (B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) :
     ∃ T : Finset G,
-      K ^ (-4096 * ⌈𝓛 (C.card / B.card)⌉ / ε ^ 2) * S.card ≤ T.card ∧
+      K ^ (-4096 * ⌈𝓛 (#C / #B)⌉ / ε ^ 2) * #S ≤ #T ∧
       ∀ t ∈ T, ‖τ t (μ_[ℂ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by
-  let r : ℝ := min 1 (C.card / B.card)
-  set m : ℝ := 𝓛 (C.card / B.card)
+  let r : ℝ := min 1 (#C / #B)
+  set m : ℝ := 𝓛 (#C / #B)
   have hm₀ : 0 < m := curlog_pos (by positivity)
   have hm₁ : 1 ≤ ⌈m⌉₊ := Nat.one_le_iff_ne_zero.2 $ by positivity
   obtain ⟨T, hKT, hT⟩ := almost_periodicity (ε / exp 1) (by positivity)
@@ -441,9 +438,9 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
   have hM : (M : ℝ≥0).IsConjExponent _ := .conjExponent hM₁
   refine ⟨T, ?_, fun t ht ↦ ?_⟩
   · calc
-      _ = K ^(-(512 * 8) / ε ^ 2 * ⌈m⌉₊) * S.card := by
+      _ = K ^(-(512 * 8) / ε ^ 2 * ⌈m⌉₊) * #S := by
           rw [mul_div_right_comm, natCast_ceil_eq_intCast_ceil hm₀.le]; norm_num
-      _ ≤ K ^(-(512 * exp 1 ^ 2) / ε ^ 2 * ⌈m⌉₊) * S.card := by
+      _ ≤ K ^(-(512 * exp 1 ^ 2) / ε ^ 2 * ⌈m⌉₊) * #S := by
           gcongr
           · exact one_le_two.trans hK₂
           calc
@@ -466,10 +463,10 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
     _ ≤ ∑ y, ‖F y * μ (x +ᵥ -C) y‖ := norm_sum_le _ _
     _ = ‖F * μ (x +ᵥ -C)‖_[1] := by rw [dL1Norm_eq_sum_norm]; rfl
     _ ≤ ‖F‖_[M] * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := dL1Norm_mul_le hM _ _
-    _ ≤ ε / exp 1 * B.card ^ (M : ℝ)⁻¹ * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := by
+    _ ≤ ε / exp 1 * #B ^ (M : ℝ)⁻¹ * ‖μ_[ℂ] (x +ᵥ -C)‖_[NNReal.conjExponent M] := by
         gcongr
         simpa only [← ENNReal.coe_natCast, dLpNorm_indicate hM₀] using hT _ ht
-    _ = ε * ((C.card / B.card) ^ (-(M : ℝ)⁻¹) / exp 1) := by
+    _ = ε * ((#C / #B) ^ (-(M : ℝ)⁻¹) / exp 1) := by
         rw [← mul_comm_div, dLpNorm_mu hM.symm.one_le hC.neg.vadd_finset, card_vadd_finset,
           card_neg, hM.symm.coe.inv_sub_one, div_rpow, mul_assoc, NNReal.coe_natCast]
         push_cast
@@ -477,7 +474,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
         all_goals positivity
     _ ≤ ε := mul_le_of_le_one_right (by positivity) $ (div_le_one $ by positivity).2 ?_
   calc
-    (C.card / B.card : ℝ) ^ (-(M : ℝ)⁻¹)
+    (#C / #B : ℝ) ^ (-(M : ℝ)⁻¹)
       ≤ r ^ (-(M : ℝ)⁻¹) :=
         rpow_le_rpow_of_nonpos (by positivity) inf_le_right $ neg_nonpos.2 $ by positivity
     _ ≤ r ^ (-(1 + log r⁻¹)⁻¹) :=
@@ -496,7 +493,7 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
     (hK₂ : 2 ≤ K) (hK : σ[A, S] ≤ K) (hS : S.Nonempty)
     (B C : Finset G) (hB : B.Nonempty) (hC : C.Nonempty) :
     ∃ T : Finset G,
-      K ^ (-4096 * ⌈𝓛 (C.card / B.card)⌉ * k ^ 2/ ε ^ 2) * S.card ≤ T.card ∧
+      K ^ (-4096 * ⌈𝓛 (#C / #B)⌉ * k ^ 2/ ε ^ 2) * #S ≤ #T ∧
       ‖μ T ∗^ k ∗ (μ_[ℂ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by
   obtain ⟨T, hKT, hT⟩ := linfty_almost_periodicity (ε / k) (by positivity)
     (div_le_one_of_le₀ (hε₁.trans $ mod_cast Nat.one_le_iff_ne_zero.2 hk) $ by positivity) hK₂ hK
@@ -504,7 +501,7 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
   refine ⟨T, by simpa only [div_pow, div_div_eq_mul_div] using hKT, ?_⟩
   set F := μ_[ℂ] A ∗ 𝟭 B ∗ μ C
   have hT' : T.Nonempty := by
-    have : (0 : ℝ) < T.card := hKT.trans_lt' $ by positivity
+    have : (0 : ℝ) < #T := hKT.trans_lt' $ by positivity
     simpa [card_pos] using this
   calc
     (‖μ T ∗^ k ∗ F - F‖_[∞] : ℝ)
diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean
index b03234478a..14137d6101 100644
--- a/LeanAPAP/Physics/DRC.lean
+++ b/LeanAPAP/Physics/DRC.lean
@@ -20,7 +20,7 @@ private def c (p : ℕ) (A : Finset G) (s : Fin p → G) : Finset G := univ.inf
 
 private lemma lemma_0 (p : ℕ) (B₁ B₂ A : Finset G) (f : G → ℝ) :
     ∑ s, ⟪𝟭_[ℝ] (B₁ ∩ c p A s) ○ 𝟭 (B₂ ∩ c p A s), f⟫_[ℝ] =
-      (B₁.card * B₂.card) • ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by
+      (#B₁ * #B₂) • ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by
   simp_rw [mul_assoc]
   simp only [wInner_one_eq_sum, inner_apply, RCLike.conj_to_real, mul_sum, sum_mul, smul_sum,
     @sum_comm _ _ (Fin p → G), sum_dconv_mul, dconv_apply_sub, Fintype.sum_pow, map_indicate]
@@ -31,20 +31,20 @@ private lemma lemma_0 (p : ℕ) (B₁ B₂ A : Finset G) (f : G → ℝ) :
     indicate_inter_apply, indicate_inter_apply, mul_mul_mul_comm, prod_mul_distrib]
   simp [c, indicate_inf_apply, ← translate_indicate, sub_eq_add_neg, mul_assoc, add_comm]
 
-private lemma sum_c (p : ℕ) (B A : Finset G) : ∑ s, (B ∩ c p A s).card = A.card ^ p * B.card := by
+private lemma sum_c (p : ℕ) (B A : Finset G) : ∑ s, #(B ∩ c p A s) = #A ^ p * #B := by
   simp only [card_eq_sum_indicate, indicate_inter_apply, c, indicate_inf_apply, mul_sum, sum_mul,
     sum_pow', @sum_comm G, Fintype.piFinset_univ, ← translate_indicate, translate_apply]
   congr with x
   exact Fintype.sum_equiv (Equiv.subLeft fun _ ↦ x) _ _ fun s ↦ mul_comm _ _
 
 private lemma sum_cast_c (p : ℕ) (B A : Finset G) :
-    ∑ s, ((B ∩ c p A s).card : ℝ) = A.card ^ p * B.card := by
+    ∑ s, (#(B ∩ c p A s) : ℝ) = #A ^ p * #B := by
   rw [← Nat.cast_sum, sum_c]; norm_cast
 
 variable [MeasurableSpace G]
 
 noncomputable def s (p : ℝ≥0) (ε : ℝ) (B₁ B₂ A : Finset G) : Finset G :=
-  univ.filter fun x ↦ (1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] < (𝟭 A ○ 𝟭 A) x
+  {x | (1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] < (𝟭 A ○ 𝟭 A) x}
 
 @[simp]
 lemma mem_s {p : ℝ≥0} {ε : ℝ} {B₁ B₂ A : Finset G} {x : G} :
@@ -76,16 +76,16 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     ∃ A₁, A₁ ⊆ B₁ ∧ ∃ A₂, A₂ ⊆ B₂ ∧
       ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ f⟫_[ℝ] * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p
         ≤ 2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭_[ℝ] A ○ 𝟭 A) x ^ p * f x ∧
-      (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p)
-        ≤ A₁.card / B₁.card ∧
-      (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p)
-        ≤ A₂.card / B₂.card := by
+      (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p)
+        ≤ #A₁ / #B₁ ∧
+      (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p)
+        ≤ #A₂ / #B₂ := by
   have := hB.mono inter_subset_left
   have := hB.mono inter_subset_right
   have hp₀ : p ≠ 0 := by positivity
   have := dLpNorm_conv_pos hp₀ hB hA
   set M : ℝ :=
-    2 ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p * (sqrt B₁.card * sqrt B₂.card) / A.card ^ p
+    2 ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p * (sqrt #B₁ * sqrt #B₂) / #A ^ p
       with hM_def
   have hM : 0 < M := by rw [hM_def]; positivity
   replace hf : 0 < ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by
@@ -98,16 +98,16 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
       forall_const, Set.mem_inter_iff, ← coe_sub, mem_coe, support_pow' _ hp₀, hf]
   set A₁ := fun s ↦ B₁ ∩ c p A s
   set A₂ := fun s ↦ B₂ ∩ c p A s
-  set g : (Fin p → G) → ℝ := fun s ↦ (A₁ s).card * (A₂ s).card with hg_def
+  set g : (Fin p → G) → ℝ := fun s ↦ #(A₁ s) * #(A₂ s) with hg_def
   have hg : ∀ s, 0 ≤ g s := fun s ↦ by rw [hg_def]; dsimp; positivity
-  have hgB : ∑ s, g s = B₁.card * B₂.card * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by
+  have hgB : ∑ s, g s = #B₁ * #B₂ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p := by
     have hAdconv : 0 ≤ 𝟭_[ℝ] A ○ 𝟭 A := dconv_nonneg indicate_nonneg indicate_nonneg
     simpa only [wLpNorm_pow_eq_sum_norm hp₀, wInner_one_eq_sum, sum_dconv, sum_indicate, Pi.one_apply,
       RCLike.inner_apply, RCLike.conj_to_real, norm_of_nonneg (hAdconv _), mul_one, nsmul_eq_mul,
       Nat.cast_mul, ← hg_def, NNReal.smul_def, NNReal.coe_dconv, NNReal.coe_comp_mu]
         using lemma_0 p B₁ B₂ A 1
   suffices ∑ s, ⟪𝟭_[ℝ] (A₁ s) ○ 𝟭 (A₂ s), (↑) ∘ f⟫_[ℝ] * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p
-    < ∑ s, 𝟭 (univ.filter fun s ↦ M ^ 2 ≤ g s) s * g s *
+    < ∑ s, 𝟭 ({s | M ^ 2 ≤ g s} : Finset _) s * g s *
         (2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭_[ℝ] A ○ 𝟭 A) x ^ p * f x) by
     obtain ⟨s, -, hs⟩ := exists_lt_of_sum_lt this
     refine ⟨_, inter_subset_left (s₂ := c p A s), _, inter_subset_left (s₂ := c p A s), ?_⟩
@@ -119,8 +119,8 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
       -- positivity
       cases hs.not_le $ mul_nonneg (sum_nonneg fun x _ ↦ mul_nonneg (this _) $ by positivity) $ by
         positivity
-    have : (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p)
-      ≤ (A₁ s).card / B₁.card * ((A₂ s).card / B₂.card) := by
+    have : (4 : ℝ) ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p)
+      ≤ #(A₁ s) / #B₁ * (#(A₂ s) / #B₂) := by
       rw [div_mul_div_comm, le_div_iff₀]
       simpa [hg_def, hM_def, mul_pow, div_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num,
         mul_div_right_comm] using h
@@ -152,15 +152,14 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
   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]
-      _ < ∑ s with g s < M ^ 2 ∧ g s ≠ 0, M * sqrt (g s)
-          := sum_lt_sum_of_nonempty ⟨s, mem_filter.2 ⟨mem_univ _, hs.symm⟩⟩ ?_
-      _ ≤ ∑ s, M * sqrt (g s) := sum_le_univ_sum_of_nonneg fun s ↦ by positivity
-      _ = M * (∑ s, sqrt (A₁ s).card * sqrt (A₂ s).card)
-          := by simp_rw [mul_sum, sqrt_mul $ Nat.cast_nonneg _]
-      _ ≤ M * (sqrt (∑ s, (A₁ s).card) * sqrt (∑ s, (A₂ s).card))
-          := mul_le_mul_of_nonneg_left
-            (sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity) hM.le
-      _ = _ := ?_
+    _ < ∑ s with g s < M ^ 2 ∧ g s ≠ 0, M * sqrt (g s)
+        := sum_lt_sum_of_nonempty ⟨s, mem_filter.2 ⟨mem_univ _, hs.symm⟩⟩ ?_
+    _ ≤ ∑ s, M * sqrt (g s) := sum_le_univ_sum_of_nonneg fun s ↦ by positivity
+    _ = M * (∑ s, sqrt #(A₁ s) * sqrt #(A₂ s))
+        := by simp_rw [mul_sum, sqrt_mul $ Nat.cast_nonneg _]
+    _ ≤ M * (sqrt (∑ s, #(A₁ s)) * sqrt (∑ s, #(A₂ s))) := by
+      gcongr; exact sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity
+    _ = _ := ?_
   · simp only [mem_filter, mem_univ, true_and, Nat.cast_nonneg, and_imp]
     exact fun s hsM hs ↦ mul_lt_mul_of_pos_right ((sqrt_lt' hM).2 hsM) $
       sqrt_pos.2 $ (hg _).lt_of_ne' hs
@@ -174,21 +173,20 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
     (hp₂ : 2 ≤ p) (hpε : ε⁻¹ * log (2 / δ) ≤ p) (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty)
     (hf : ∃ x, x ∈ B₁ - B₂ ∧ x ∈ A - A ∧ x ∉ s p ε B₁ B₂ A) :
     ∃ A₁, A₁ ⊆ B₁ ∧ ∃ A₂, A₂ ⊆ B₂ ∧ 1 - δ ≤ ∑ x in s p ε B₁ B₂ A, (μ A₁ ○ μ A₂) x ∧
-        (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p) ≤
-            A₁.card / B₁.card ∧
-          (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p) ≤
-            A₂.card / B₂.card := by
+        (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) ≤
+            #A₁ / #B₁ ∧
+          (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) ≤
+            #A₂ / #B₂ := by
   obtain ⟨A₁, hAB₁, A₂, hAB₂, h, hcard₁, hcard₂⟩ :=
     drc hp₂ (𝟭 (s p ε B₁ B₂ A)ᶜ)
       (by simpa only [support_indicate, coe_compl, Set.mem_compl_iff, mem_coe]) hB hA
   refine ⟨A₁, hAB₁, A₂, hAB₂, ?_, hcard₁, hcard₂⟩
   have hp₀ : 0 < p := by positivity
-  have aux :
-    ∀ (c : Finset G) (r),
-      (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / A.card ^ (2 * p) ≤ c.card / r →
-        c.Nonempty := by
+  have aux (c : Finset G) (r)
+    (h : (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) ≤ #c / r) :
+    c.Nonempty := by
     simp_rw [nonempty_iff_ne_empty]
-    rintro c r h rfl
+    rintro rfl
     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
@@ -247,7 +245,7 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p
   · have hp₀ : p ≠ 0 := by positivity
     have :
       (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤
-        4⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ] ^ (2 * p) / A.card ^ (2 * p) := by
+        4⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ] ^ (2 * p) / #A ^ (2 * p) := by
       rw [mul_div_assoc, ← div_pow]
       refine mul_le_mul_of_nonneg_left (pow_le_pow_left (by positivity) ?_ _) (by norm_num)
       rw [nnratCast_dens, le_div_iff₀, ← mul_div_right_comm]
diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
index 1582476ae4..487c5df1d6 100644
--- a/LeanAPAP/Physics/Unbalancing.lean
+++ b/LeanAPAP/Physics/Unbalancing.lean
@@ -28,7 +28,7 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : g ○ g = f) (hν : h ○ h = (↑
   simp only [WithLp.equiv_symm_pi_apply, Pi.pow_apply, RCLike.inner_apply, map_pow]
   simp_rw [dconv_apply h, mul_sum]
   --TODO: Please make `conv` work here :(
-  have : ∀ x, ∀ yz ∈ univ.filter fun yz : G × G ↦ yz.1 - yz.2 = x,
+  have : ∀ x, ∀ yz ∈ ({yz : G × G | yz.1 - yz.2 = x} : Finset _),
     conj ((g ○ g) x) ^ k * (h yz.1 * conj (h yz.2)) =
       conj ((g ○ g) (yz.1 - yz.2)) ^ k * (h yz.1 * conj (h yz.2)) := by
     simp only [mem_filter, mem_univ, true_and]
@@ -100,8 +100,8 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
         pow_sub_one_mul hp₁.pos.ne', NNReal.smul_def, smul_eq_mul]
     · simp [wInner_one_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
-  set T := univ.filter fun i ↦ 3 / 4 * ε ≤ f i
+  set P : Finset _ := {i | 0 ≤ f i}
+  set T : Finset _ := {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]
diff --git a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
index e22240be06..b3b2127eac 100644
--- a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
+++ b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
@@ -101,7 +101,7 @@ def mkZModAux {ι : Type} [DecidableEq ι] (n : ι → ℕ) (u : ∀ i, ZMod (n
 
 lemma mkZModAux_injective {ι : Type} [DecidableEq ι] {n : ι → ℕ} (hn : ∀ i, n i ≠ 0) :
     Injective (mkZModAux n) :=
-  AddChar.directSum_injective.comp fun f g h ↦ by simpa [Function.funext_iff, hn] using h
+  AddChar.directSum_injective.comp fun f g h ↦ by simpa [funext_iff, hn] using h
 
 /-- The circle-valued characters of a finite abelian group are the same as its complex-valued
 characters. -/
diff --git a/LeanAPAP/Prereqs/Bohr/Basic.lean b/LeanAPAP/Prereqs/Bohr/Basic.lean
index 5844c931d8..5b0d6320af 100644
--- a/LeanAPAP/Prereqs/Bohr/Basic.lean
+++ b/LeanAPAP/Prereqs/Bohr/Basic.lean
@@ -2,7 +2,7 @@ import Mathlib.Analysis.Complex.Basic
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 
 open AddChar Function
-open scoped NNReal ENNReal
+open scoped NNReal ENNReal Finset
 
 /-- A *Bohr set* `B` on an additive group `G` is a finite set of characters of `G`, called the
 *frequencies*, along with an extended non-negative real number for each frequency `ψ`, called the
@@ -233,9 +233,9 @@ noncomputable instance [Finite G] : CompletelyDistribLattice (BohrSet G) :=
 /-! ### Width, frequencies, rank -/
 
 /-- The rank of a Bohr set is the number of characters which have finite width. -/
-def rank (B : BohrSet G) : ℕ := B.frequencies.card
+def rank (B : BohrSet G) : ℕ := #B.frequencies
 
-@[simp] lemma card_frequencies (B : BohrSet G) : B.frequencies.card = B.rank := rfl
+@[simp] lemma card_frequencies (B : BohrSet G) : #B.frequencies = B.rank := rfl
 
 /-! ### Dilation -/
 
diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean
index 31f47c7b37..89275b97cd 100644
--- a/LeanAPAP/Prereqs/Chang.lean
+++ b/LeanAPAP/Prereqs/Chang.lean
@@ -55,7 +55,7 @@ end Mathlib.Meta.Positivity
 
 lemma AddDissociated.boringEnergy_le [DecidableEq G] {s : Finset G}
     (hs : AddDissociated (s : Set G)) (n : ℕ) :
-    boringEnergy n s ≤ changConst ^ n * n ^ n * s.card ^ n := by
+    boringEnergy n s ≤ changConst ^ n * n ^ n * #s ^ n := by
   obtain rfl | hn := eq_or_ne n 0
   · simp
   calc
@@ -87,14 +87,14 @@ private lemma α_le_one (f : G → ℂ) : ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / ca
 
 lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x ≠ 0 → 1 ≤ ν x)
     (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0) :
-    ↑Δ.card ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2)) ≤
+    #Δ ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2)) ≤
       energy m Δ (dft fun a ↦ ν a) := by
   obtain rfl | hf := eq_or_ne f 0
   · simp
   choose c norm_c hc using fun γ ↦ RCLike.exists_norm_eq_mul_self (dft f γ)
   have :=
     calc
-      η * ‖f‖_[1] * Δ.card ≤ ∑ γ in Δ, ‖dft f γ‖ := ?_
+      η * ‖f‖_[1] * #Δ ≤ ∑ γ in Δ, ‖dft f γ‖ := ?_
       _ ≤ ‖∑ x, f x * ∑ γ in Δ, c γ * conj (γ x)‖ := ?_
       _ ≤ ∑ x, ‖f x * ∑ γ in Δ, c γ * conj (γ x)‖ := (norm_sum_le _ _)
       _ = ∑ x, ‖f x‖ * ‖∑ γ in Δ, c γ * conj (γ x)‖ := by simp_rw [norm_mul]
@@ -156,7 +156,7 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x 
 open scoped ComplexOrder
 
 lemma spec_hoelder (hη : 0 ≤ η) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0) :
-    Δ.card ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)) ≤ boringEnergy m Δ := by
+    #Δ ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)) ≤ boringEnergy m Δ := by
   have hG : (0 : ℝ) < card G := by positivity
   simpa [boringEnergy, mul_assoc, ← Pi.one_def, ← mul_div_right_comm, ← mul_div_assoc,
     div_le_iff₀ hG, energy_nsmul, -nsmul_eq_mul, ← nsmul_eq_mul'] using
@@ -165,10 +165,10 @@ lemma spec_hoelder (hη : 0 ≤ η) (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0)
 /-- **Chang's lemma**. -/
 lemma chang (hf : f ≠ 0) (hη : 0 < η) :
     ∃ Δ, Δ ⊆ largeSpec f η ∧
-      Δ.card ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)⌉₊ / η ^ 2⌉₊ ∧
+      #Δ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)⌉₊ / η ^ 2⌉₊ ∧
       largeSpec f η ⊆ Δ.addSpan := by
   refine exists_subset_addSpan_card_le_of_forall_addDissociated fun Δ hΔη hΔ ↦ ?_
-  obtain hΔ' | hΔ' := @eq_zero_or_pos _ _ Δ.card
+  obtain hΔ' | hΔ' := @eq_zero_or_pos _ _ #Δ
   · simp [hΔ']
   let α := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G
   have : 0 < α := by positivity
@@ -176,16 +176,16 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
   have hβ : 0 < β := Nat.ceil_pos.2 (curlog_pos (by positivity) $ α_le_one _)
   have : 0 < ‖f‖_[1] := by positivity
   refine le_of_pow_le_pow_left hβ.ne' zero_le' $ Nat.cast_le.1 $ le_of_mul_le_mul_right ?_
-    (by positivity : 0 < Δ.card ^ β * (η ^ (2 * β) * α))
+    (by positivity : 0 < #Δ ^ β * (η ^ (2 * β) * α))
   push_cast
   rw [← mul_assoc, ← pow_add, ← two_mul]
   refine ((spec_hoelder hη.le hΔη hβ.ne').trans $ hΔ.boringEnergy_le _).trans ?_
   refine le_trans ?_ $ mul_le_mul_of_nonneg_right (pow_le_pow_left ?_ (Nat.le_ceil _) _) ?_
   rw [mul_right_comm, div_pow, mul_pow, mul_pow, exp_one_pow, ← pow_mul, mul_div_assoc]
   calc
-    _ = (changConst * Δ.card * β) ^ β := by ring
-    _ ≤ (changConst * Δ.card * β) ^ β * (α * exp β) := ?_
-    _ ≤ (changConst * Δ.card * β) ^ β * ((η / η) ^ (2 * β) * α * exp β) := by
+    _ = (changConst * #Δ * β) ^ β := by ring
+    _ ≤ (changConst * #Δ * β) ^ β * (α * exp β) := ?_
+    _ ≤ (changConst * #Δ * β) ^ β * ((η / η) ^ (2 * β) * α * exp β) := by
       rw [div_self hη.ne', one_pow, one_mul]
     _ = _ := by ring
   refine le_mul_of_one_le_right (by positivity) ?_
diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
index 22245f4799..1a343be73b 100644
--- a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
+++ b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
@@ -52,7 +52,7 @@ section CommSemiring
 variable [CommSemiring R] {f g : G → R}
 
 lemma indicate_conv_indicate_eq_sum (s t : Finset G) (a : G) :
-    (𝟭_[R] s ∗ 𝟭 t) a = ((s ×ˢ t).filter fun x : G × G ↦ x.1 + x.2 = a).card := by
+    (𝟭_[R] s ∗ 𝟭 t) a = #{x ∈ s ×ˢ t | x.1 + x.2 = a} := by
   simp only [conv_apply, indicate_apply, ← ite_and, filter_comm, boole_mul, sum_boole]
   simp_rw [← mem_product, filter_univ_mem]
 
@@ -63,7 +63,7 @@ lemma conv_indicate (f : G → R) (s : Finset G) : f ∗ 𝟭 s = ∑ a ∈ s, 
   ext; simp [conv_eq_sum_sub, indicate_apply]
 
 lemma indicate_conv_indicate_eq_card_vadd_inter_neg (s t : Finset G) (a : G) :
-    (𝟭_[R] s ∗ 𝟭 t) a = ((-a +ᵥ s) ∩ -t).card := by
+    (𝟭_[R] s ∗ 𝟭 t) a = #((-a +ᵥ s) ∩ -t) := by
   rw [← card_neg, neg_inter]
   simp [conv_indicate, indicate, inter_comm, ← filter_mem_eq_inter, ← neg_vadd_mem_iff,
     ← sub_eq_add_neg]
@@ -71,7 +71,7 @@ lemma indicate_conv_indicate_eq_card_vadd_inter_neg (s t : Finset G) (a : G) :
 variable [StarRing R]
 
 lemma indicate_dconv_indicate_apply (s t : Finset G) (a : G) :
-    (𝟭_[R] s ○ 𝟭 t) a = ((s ×ˢ t).filter fun x : G × G ↦ x.1 - x.2 = a).card := by
+    (𝟭_[R] s ○ 𝟭 t) a = #{x ∈ s ×ˢ t | x.1 - x.2 = a} := by
   simp only [dconv_apply, indicate_apply, ← ite_and, filter_comm, boole_mul, sum_boole,
     apply_ite conj, map_one, map_zero, Pi.conj_apply]
   simp_rw [← mem_product, filter_univ_mem]
@@ -90,10 +90,10 @@ variable [Semifield R]
 @[simp] lemma mu_univ_conv_mu_univ : μ_[R] (univ : Finset G) ∗ μ univ = μ univ := by
   ext; cases eq_or_ne (card G : R) 0 <;> simp [mu_apply, conv_eq_sum_add, card_univ, *]
 
-lemma mu_conv (s : Finset G) (f : G → R) : μ s ∗ f = (s.card : R)⁻¹ • ∑ a ∈ s, τ a f := by
+lemma mu_conv (s : Finset G) (f : G → R) : μ s ∗ f = (#s : R)⁻¹ • ∑ a ∈ s, τ a f := by
   simp [mu, indicate_conv, smul_conv]
 
-lemma conv_mu (f : G → R) (s : Finset G) : f ∗ μ s = (s.card : R)⁻¹ • ∑ a ∈ s, τ a f := by
+lemma conv_mu (f : G → R) (s : Finset G) : f ∗ μ s = (#s : R)⁻¹ • ∑ a ∈ s, τ a f := by
   simp [mu, conv_indicate, conv_smul]
 
 variable [StarRing R]
@@ -102,10 +102,10 @@ variable [StarRing R]
   ext; cases eq_or_ne (card G : R) 0 <;> simp [mu_apply, dconv_eq_sum_add, card_univ, *]
 
 lemma mu_dconv (s : Finset G) (f : G → R) :
-    μ s ○ f = (s.card : R)⁻¹ • ∑ a ∈ s, τ a (conjneg f) := by
+    μ s ○ f = (#s : R)⁻¹ • ∑ a ∈ s, τ a (conjneg f) := by
   simp [mu, indicate_dconv, smul_dconv]
 
-lemma dconv_mu (f : G → R) (s : Finset G) : f ○ μ s = (s.card : R)⁻¹ • ∑ a ∈ s, τ (-a) f := by
+lemma dconv_mu (f : G → R) (s : Finset G) : f ○ μ s = (#s : R)⁻¹ • ∑ a ∈ s, τ (-a) f := by
   simp [mu, dconv_indicate, dconv_smul]
 
 end Semifield
@@ -150,7 +150,7 @@ section CommSemiring
 variable [CommSemiring R] {f g : G → R} {n : ℕ}
 
 lemma indicate_iterConv_apply (s : Finset G) (n : ℕ) (a : G) :
-    (𝟭_[R] s ∗^ n) a = ((s ^^ n).filter fun x : Fin n → G ↦ ∑ i, x i = a).card := by
+    (𝟭_[R] s ∗^ n) a = #{x ∈ s ^^ n | ∑ i, x i = a} := by
   induction' n with n ih generalizing a
   · simp [apply_ite card, eq_comm]
   simp_rw [iterConv_succ', conv_eq_sum_sub', ih, indicate_apply, boole_mul, sum_ite,
diff --git a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
index fcf911c061..ea0c1a1e86 100644
--- a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
+++ b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
@@ -15,12 +15,12 @@ variable {G : Type*} [AddCommGroup G] [DecidableEq G] [Fintype G] {s : Finset G}
 
 lemma ThreeAPFree.wInner_one_mu_conv_mu_mu_two_smul_mu (hG : Odd (card G))
     (hs : ThreeAPFree (s : Set G)) :
-    ⟪μ_[ℝ] s ∗ μ s, μ (s.image (2 • ·))⟫_[ℝ] = (s.card ^ 2 : ℝ)⁻¹ := by
+    ⟪μ_[ℝ] s ∗ μ s, μ (s.image (2 • ·))⟫_[ℝ] = (#s ^ 2 : ℝ)⁻¹ := by
   obtain rfl | hs' := s.eq_empty_or_nonempty
   · simp
   simp only [wInner_one_eq_sum, inner_apply, sum_conv_mul, ← sum_product', RCLike.conj_to_real]
   rw [← diag_union_offDiag univ, sum_union (disjoint_diag_offDiag _), sum_diag, ←
-    sum_add_sum_compl s, @sum_eq_card_nsmul _ _ _ _ _ (s.card ^ 3 : ℝ)⁻¹, nsmul_eq_mul,
+    sum_add_sum_compl s, @sum_eq_card_nsmul _ _ _ _ _ (#s ^ 3 : ℝ)⁻¹, nsmul_eq_mul,
     Finset.sum_eq_zero, Finset.sum_eq_zero, add_zero, add_zero, pow_succ', mul_inv,
     mul_inv_cancel_left₀]
   · exact Nat.cast_ne_zero.2 hs'.card_pos.ne'
diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean
index 8a48e2ebdc..c4722564be 100644
--- a/LeanAPAP/Prereqs/Energy.lean
+++ b/LeanAPAP/Prereqs/Energy.lean
@@ -42,7 +42,7 @@ lemma boringEnergy_eq (n : ℕ) (s : Finset G) : boringEnergy n s = ∑ x, (𝟭
   refine sum_congr rfl fun f hf ↦ ?_
   simp_rw [(mem_filter.1 hf).2, eq_comm]
 
-@[simp] lemma boringEnergy_one (s : Finset G) : boringEnergy 1 s = s.card := by
+@[simp] lemma boringEnergy_one (s : Finset G) : boringEnergy 1 s = #s := by
   simp [boringEnergy_eq, indicate_apply]
 
 lemma cLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) :
@@ -63,7 +63,7 @@ lemma cLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) :
       Nat.cast_eq_zero, Fintype.card_ne_zero, or_false, sq, Complex.ofReal_iterConv,
       (((indicate_isSelfAdjoint _).iterConv _).apply _).conj_eq, Complex.ofReal_comp_indicate]
 
-lemma cL2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt s.card := by
+lemma cL2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt #s := by
   rw [eq_comm, sqrt_eq_iff_eq_sq, eq_comm]
   simpa using cLpNorm_dft_indicate_pow 1 s
   all_goals positivity
diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
index 0c21e5a123..0a677f1897 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
@@ -119,7 +119,7 @@ lemma dft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime
 
 variable [DecidableEq α]
 
-@[simp] lemma dft_indicate_zero (A : Finset α) : dft (𝟭 A) 0 = A.card := by
+@[simp] lemma dft_indicate_zero (A : Finset α) : dft (𝟭 A) 0 = #A := by
   simp only [dft_apply, wInner_one_eq_sum, inner_apply, sum_indicate, AddChar.zero_apply, map_one,
     one_mul]
 
diff --git a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
index 43343ab2f2..2807a8554e 100644
--- a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
+++ b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
@@ -36,7 +36,7 @@ end CommSemiring
 section Semifield
 variable [Fintype ι] [DecidableEq ι] [Semiring β] [Module ℚ≥0 β]
 
-lemma expect_indicate (s : Finset ι) : 𝔼 x, 𝟭_[β] s x = s.card /ℚ Fintype.card ι := by
+lemma expect_indicate (s : Finset ι) : 𝔼 x, 𝟭_[β] s x = #s /ℚ Fintype.card ι := by
   simp only [expect_univ, indicate]
   rw [← sum_filter, filter_mem_eq_inter, univ_inter, sum_const, Nat.smul_one_eq_cast]
 
diff --git a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean
index bbc1199109..3aad71670b 100644
--- a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean
+++ b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean
@@ -61,9 +61,9 @@ variable (β)
 
 end Nontrivial
 
-lemma sum_indicate [Fintype α] (s : Finset α) : ∑ x, 𝟭_[β] s x = s.card := by simp [indicate_apply]
+lemma sum_indicate [Fintype α] (s : Finset α) : ∑ x, 𝟭_[β] s x = #s := by simp [indicate_apply]
 
-lemma card_eq_sum_indicate [Fintype α] (s : Finset α) : s.card = ∑ x, 𝟭_[ℕ] s x :=
+lemma card_eq_sum_indicate [Fintype α] (s : Finset α) : #s = ∑ x, 𝟭_[ℕ] s x :=
   (sum_indicate _ _).symm
 
 section AddGroup
@@ -126,7 +126,7 @@ variable [OrderedSemiring β] {s : Finset α}
 @[simp] lemma indicate_nonneg : 0 ≤ 𝟭_[β] s := fun a ↦ by rw [indicate_apply]; split_ifs <;> simp
 
 @[simp] lemma indicate_pos [Nontrivial β] : 0 < 𝟭_[β] s ↔ s.Nonempty := by
-  simp [indicate_apply, Pi.lt_def, Function.funext_iff, lt_iff_le_and_ne, @eq_comm β 0,
+  simp [indicate_apply, Pi.lt_def, funext_iff, lt_iff_le_and_ne, @eq_comm β 0,
     Finset.Nonempty]
 
 protected alias ⟨_, Finset.Nonempty.indicate_pos⟩ := indicate_pos
@@ -139,13 +139,13 @@ section DivisionSemiring
 variable [DivisionSemiring β] [DivisionSemiring γ] {s : Finset α}
 
 /-- The normalised indicate of a set. -/
-def mu (s : Finset α) : α → β := (s.card : β)⁻¹ • 𝟭 s
+def mu (s : Finset α) : α → β := (#s : β)⁻¹ • 𝟭 s
 
 notation "μ " => mu
 
 notation "μ_[" β "] " => @mu _ β _ _
 
-lemma mu_apply (x : α) : μ s x = (s.card : β)⁻¹ * ite (x ∈ s) 1 0 := rfl
+lemma mu_apply (x : α) : μ s x = (#s : β)⁻¹ * ite (x ∈ s) 1 0 := rfl
 
 @[simp] lemma mu_empty : (μ ∅ : α → β) = 0 := by ext; simp [mu]
 
@@ -166,7 +166,7 @@ variable [CharZero β] {a : α}
 lemma mu_apply_ne_zero : μ_[β] s a ≠ 0 ↔ a ∈ s := mu_apply_eq_zero.not_left
 
 @[simp] lemma mu_eq_zero : μ_[β] s = 0 ↔ s = ∅ := by
-  simp [Function.funext_iff, eq_empty_iff_forall_not_mem]
+  simp [funext_iff, eq_empty_iff_forall_not_mem]
 
 lemma mu_ne_zero : μ_[β] s ≠ 0 ↔ s.Nonempty := mu_eq_zero.not.trans nonempty_iff_ne_empty.symm
 
@@ -179,7 +179,7 @@ end Nontrivial
 
 variable (β)
 
-lemma card_smul_mu [CharZero β] (s : Finset α) : s.card • μ_[β] s = 𝟭 s := by
+lemma card_smul_mu [CharZero β] (s : Finset α) : #s • μ_[β] s = 𝟭 s := by
   ext x : 1
   rw [Pi.smul_apply, mu_apply, indicate_apply, nsmul_eq_mul]
   split_ifs with h
@@ -188,7 +188,7 @@ lemma card_smul_mu [CharZero β] (s : Finset α) : s.card • μ_[β] s = 𝟭 s
     exact ⟨_, h⟩
   · rw [mul_zero, mul_zero]
 
-lemma card_smul_mu_apply [CharZero β] (s : Finset α) (x : α) : s.card • μ_[β] s x = 𝟭 s x :=
+lemma card_smul_mu_apply [CharZero β] (s : Finset α) (x : α) : #s • μ_[β] s x = 𝟭 s x :=
   congr_fun (card_smul_mu β _) _
 
 @[simp] lemma sum_mu [CharZero β] [Fintype α] (hs : s.Nonempty) : ∑ x, μ_[β] s x = 1 := by
diff --git a/LeanAPAP/Prereqs/LargeSpec.lean b/LeanAPAP/Prereqs/LargeSpec.lean
index c45bda0642..56fe40b1d7 100644
--- a/LeanAPAP/Prereqs/LargeSpec.lean
+++ b/LeanAPAP/Prereqs/LargeSpec.lean
@@ -12,7 +12,7 @@ variable {G : Type*} [AddCommGroup G] [Fintype G] [MeasurableSpace G] {f : G →
 
 /-- The `η`-large spectrum of a function. -/
 noncomputable def largeSpec (f : G → ℂ) (η : ℝ) : Finset (AddChar G ℂ) :=
-  univ.filter fun ψ ↦ η * ‖f‖_[1] ≤ ‖dft f ψ‖
+  {ψ | η * ‖f‖_[1] ≤ ‖dft f ψ‖}
 
 @[simp] lemma mem_largeSpec : ψ ∈ largeSpec f η ↔ η * ‖f‖_[1] ≤ ‖dft f ψ‖ := by simp [largeSpec]
 
diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean
index ea19dd2c7e..610ebb43c4 100644
--- a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean
@@ -18,33 +18,33 @@ variable {ι G 𝕜 E R : Type*} [Fintype ι] {mι : MeasurableSpace ι} [Discre
 section Indicator
 variable [RCLike R] [DecidableEq ι] {s : Finset ι} {p : ℝ≥0}
 
-lemma dLpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset ι) : ‖𝟭_[R] s‖_[p] ^ (p : ℝ) = s.card := by
+lemma dLpNorm_rpow_indicate (hp : p ≠ 0) (s : Finset ι) : ‖𝟭_[R] s‖_[p] ^ (p : ℝ) = #s := by
   have : ∀ x, (ite (x ∈ s) 1 0 : ℝ) ^ (p : ℝ) =
     ite (x ∈ s) (1 ^ (p : ℝ)) (0 ^ (p : ℝ)) := fun x ↦ by split_ifs <;> simp
   simp [dLpNorm_rpow_eq_sum_nnnorm, hp, indicate_apply, apply_ite nnnorm, -sum_const, card_eq_sum_ones,
     sum_boole, this, zero_rpow, filter_mem_eq_inter]
 
-lemma dLpNorm_indicate (hp : p ≠ 0) (s : Finset ι) : ‖𝟭_[R] s‖_[p] = s.card ^ (p⁻¹ : ℝ) := by
+lemma dLpNorm_indicate (hp : p ≠ 0) (s : Finset ι) : ‖𝟭_[R] s‖_[p] = #s ^ (p⁻¹ : ℝ) := by
   refine (NNReal.eq_rpow_inv_iff ?_).2 (dLpNorm_rpow_indicate ?_ _) <;> positivity
 
 lemma dLpNorm_pow_indicate {p : ℕ} (hp : p ≠ 0) (s : Finset ι) :
-    ‖𝟭_[R] s‖_[p] ^ (p : ℝ) = s.card := by
+    ‖𝟭_[R] s‖_[p] ^ (p : ℝ) = #s := by
   simpa using dLpNorm_rpow_indicate (Nat.cast_ne_zero.2 hp) s
 
-lemma dL2Norm_sq_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[2] ^ 2 = s.card := by
+lemma dL2Norm_sq_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[2] ^ 2 = #s := by
   simpa using dLpNorm_pow_indicate two_ne_zero s
 
-@[simp] lemma dL2Norm_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[2] = NNReal.sqrt s.card := by
+@[simp] lemma dL2Norm_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[2] = NNReal.sqrt #s := by
   rw [eq_comm, NNReal.sqrt_eq_iff_eq_sq, dL2Norm_sq_indicate]
 
-@[simp] lemma dL1Norm_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[1] = s.card := by
+@[simp] lemma dL1Norm_indicate (s : Finset ι) : ‖𝟭_[R] s‖_[1] = #s := by
   simpa using dLpNorm_pow_indicate one_ne_zero s
 
-lemma dLpNorm_mu (hp : 1 ≤ p) (hs : s.Nonempty) : ‖μ_[R] s‖_[p] = s.card ^ ((p : ℝ)⁻¹ - 1) := by
-  rw [mu, dLpNorm_const_smul (s.card⁻¹ : R) (𝟭_[R] s), dLpNorm_indicate, nnnorm_inv,
+lemma dLpNorm_mu (hp : 1 ≤ p) (hs : s.Nonempty) : ‖μ_[R] s‖_[p] = #s ^ ((p : ℝ)⁻¹ - 1) := by
+  rw [mu, dLpNorm_const_smul ((#s)⁻¹ : R) (𝟭_[R] s), dLpNorm_indicate, nnnorm_inv,
     RCLike.nnnorm_natCast, inv_mul_eq_div, ← NNReal.rpow_sub_one] <;> positivity
 
-lemma dLpNorm_mu_le (hp : 1 ≤ p) : ‖μ_[R] s‖_[p] ≤ s.card ^ (p⁻¹ - 1 : ℝ) := by
+lemma dLpNorm_mu_le (hp : 1 ≤ p) : ‖μ_[R] s‖_[p] ≤ #s ^ (p⁻¹ - 1 : ℝ) := by
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
   · exact (dLpNorm_mu hp hs).le
@@ -54,7 +54,7 @@ lemma dLpNorm_mu_le (hp : 1 ≤ p) : ‖μ_[R] s‖_[p] ≤ s.card ^ (p⁻¹ - 1
 
 lemma dL1Norm_mu_le_one : ‖μ_[R] s‖_[1] ≤ 1 := by simpa using dLpNorm_mu_le le_rfl
 
-@[simp] lemma dL2Norm_mu (hs : s.Nonempty) : ‖μ_[R] s‖_[2] = s.card ^ (-2⁻¹ : ℝ) := by
+@[simp] lemma dL2Norm_mu (hs : s.Nonempty) : ‖μ_[R] s‖_[2] = #s ^ (-2⁻¹ : ℝ) := by
   have : (2⁻¹ - 1 : ℝ) = -2⁻¹ := by norm_num
   simpa [sqrt_eq_rpow, this] using dLpNorm_mu one_le_two (R := R) hs
 
diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
index 96d1c94d22..a1d3d70b3a 100644
--- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
+++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
@@ -22,30 +22,30 @@ local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
 private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι)
     (hf : ∀ i, ∑ 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 := by
+      (∑ b in A ^^ n, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / #A ^ n := by
   let B := A ^^ n
   calc
     |∑ i, f (a i)| ^ (m + 1)
-      = |∑ i, (f (a i) - (∑ b in B, f (b i)) / B.card)| ^ (m + 1) := by
+      = |∑ i, (f (a i) - (∑ b in B, f (b i)) / #B)| ^ (m + 1) := by
       simp only [hf, sub_zero, zero_div]
-    _ = |(∑ b in B, ∑ i, (f (a i) - f (b i))) / B.card| ^ (m + 1) := by
+    _ = |(∑ b in B, ∑ i, (f (a i) - f (b i))) / #B| ^ (m + 1) := by
       simp only [sum_sub_distrib]
       rw [sum_const, sub_div, sum_comm, sum_div, nsmul_eq_mul, card_piFinset, prod_const,
         Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀]
       positivity
-    _ = |∑ b in B, ∑ i, (f (a i) - f (b i))| ^ (m + 1) / B.card ^ (m + 1) := by
+    _ = |∑ b in B, ∑ i, (f (a i) - f (b i))| ^ (m + 1) / #B ^ (m + 1) := by
       rw [abs_div, div_pow, Nat.abs_cast]
-    _ ≤ (∑ b in B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / B.card ^ (m + 1) := by
+    _ ≤ (∑ b in B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / #B ^ (m + 1) := by
       gcongr; exact IsAbsoluteValue.abv_sum _ _ _
-    _ = (∑ b in B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / B.card ^ m / B.card := by
+    _ = (∑ b in B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / #B ^ m / #B := by
       rw [div_div, ← _root_.pow_succ]
-    _ ≤ (∑ b in B, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / B.card := by
+    _ ≤ (∑ b in B, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / #B := by
       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 : ℕ)
     (a : Fin n → ι) :
-    |∑ i, f (a i)| ^ m ≤ (∑ b in A ^^ n, |∑ i, (f (a i) - f (b i))| ^ m) / A.card ^ n := by
+    |∑ i, f (a i)| ^ m ≤ (∑ b in A ^^ n, |∑ i, (f (a i) - f (b i))| ^ m) / #A ^ n := by
   cases m
   · simp only [_root_.pow_zero, sum_const, prod_const, Nat.smul_one_eq_cast, Finset.card_fin,
       card_piFinset, ← Nat.cast_pow]
@@ -162,14 +162,14 @@ private lemma step_eight {f : ι → ℝ} {a b : Fin n → ι} :
 
 private lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) :
     (∑ a in A ^^ n, ∑ b in A ^^ n, ∑ k in piAntidiag univ m,
-      ↑(multinomial univ fun i ↦ 2 * k i) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / A.card ^ n
+      ↑(multinomial univ fun i ↦ 2 * k i) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / #A ^ n
         ≤ (4 * m) ^ m * ∑ a in A ^^ n, (∑ i, f (a i) ^ 2) ^ m := by
   let B := A ^^ n
   calc
     (∑ a in B, ∑ b in B, ∑ k : Fin n → ℕ in piAntidiag univ m,
-      (multinomial univ fun i ↦ 2 * k i : ℝ) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / A.card ^ n
+      (multinomial univ fun i ↦ 2 * k i : ℝ) * ∏ t, (f (a t) - f (b t)) ^ (2 * k t)) / #A ^ n
     _ ≤ (∑ a in B, ∑ b in B, m ^ m * 2 ^ (m + (m - 1)) *
-          ((∑ i, f (a i) ^ 2) ^ m + (∑ i, f (b i) ^ 2) ^ m) : ℝ) / A.card ^ n := by
+          ((∑ i, f (a i) ^ 2) ^ m + (∑ i, f (b i) ^ 2) ^ m) : ℝ) / #A ^ n := by
       gcongr; exact step_six.trans $ step_seven.trans step_eight
     _ = _ := by
       simp only [mul_add, sum_add_distrib, sum_const, nsmul_eq_mul, ← mul_sum]
@@ -194,7 +194,7 @@ theorem marcinkiewicz_zygmund' (m : ℕ) (f : ι → ℝ) (hf : ∀ i, ∑ a in
   let B := A ^^ n
   calc
     ∑ a in B, (∑ i, f (a i)) ^ (2 * m)
-      ≤ ∑ a in A ^^ n, (∑ b in B, |∑ i, (f (a i) - f (b i))| ^ (2 * m))/ A.card ^ n := by
+      ≤ ∑ a in A ^^ n, (∑ b in B, |∑ i, (f (a i) - f (b i))| ^ (2 * m))/ #A ^ n := by
       gcongr; simpa [pow_mul, sq_abs] using step_one' hA f hf (2 * m) _
     _ ≤ _ := ?_
   rw [← sum_div]
diff --git a/lake-manifest.json b/lake-manifest.json
index d9cf40a63c..8a42ca0cbc 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cc0bc876eeef0518ddc1c8d3bd6f48cc83e68901",
+   "rev": "dc72dcdb8e97b3c56bd70f06f043ed2dee3258e6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa3d73a2cf077f4b14c7840352ac7b08aeb6eb41",
+   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
+   "rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
+   "rev": "0ea83a676d288220ba227808568cbb80fe43ace0",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d951eef6bb39b3b78cbd1fba9c515c3770a9d20a",
+   "rev": "8c2c97e8beb66d75f3ddc8d4c6878cd4dca30f2d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,