chore(Combinatorics): use newly introduced finset notation (#18055)

For `s : Finset α`, replace `s.card` with `#s`, `s.filter p` with `{x ∈ s | p x}`, `∑ x ∈ s.filter p, f x` with `∑ x ∈ s with p x, f x`. Rewrap lines around and open the `Finset` locale where necessary.

Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

@@ -92,15 +92,14 @@ def box (n d : ℕ) : Finset (Fin n → ℕ) :=
 theorem mem_box : x ∈ box n d ↔ ∀ i, x i < d := by simp only [box, Fintype.mem_piFinset, mem_range]
 
 @[simp]
-theorem card_box : (box n d).card = d ^ n := by simp [box]
+theorem card_box : #(box n d) = d ^ n := by simp [box]
 
 @[simp]
 theorem box_zero : box (n + 1) 0 = ∅ := by simp [box]
 
 /-- The intersection of the sphere of radius `√k` with the integer points in the positive
 quadrant. -/
-def sphere (n d k : ℕ) : Finset (Fin n → ℕ) :=
-  (box n d).filter fun x => ∑ i, x i ^ 2 = k
+def sphere (n d k : ℕ) : Finset (Fin n → ℕ) := {x ∈ box n d | ∑ i, x i ^ 2 = k}
 
 theorem sphere_zero_subset : sphere n d 0 ⊆ 0 := fun x => by simp [sphere, funext_iff]
 
@@ -204,7 +203,7 @@ theorem sum_lt : (∑ i : Fin n, d * (2 * d + 1) ^ (i : ℕ)) < (2 * d + 1) ^ n
   sum_eq.trans_lt <| (Nat.div_le_self _ 2).trans_lt <| pred_lt (pow_pos (succ_pos _) _).ne'
 
 theorem card_sphere_le_rothNumberNat (n d k : ℕ) :
-    (sphere n d k).card ≤ rothNumberNat ((2 * d - 1) ^ n) := by
+    #(sphere n d k) ≤ rothNumberNat ((2 * d - 1) ^ n) := by
   cases n
   · dsimp; refine (card_le_univ _).trans_eq ?_; rfl
   cases d
@@ -229,7 +228,7 @@ that we then optimize by tweaking the parameters. The (almost) optimal parameter
 
 
 theorem exists_large_sphere_aux (n d : ℕ) : ∃ k ∈ range (n * (d - 1) ^ 2 + 1),
-    (↑(d ^ n) / ((n * (d - 1) ^ 2 :) + 1) : ℝ) ≤ (sphere n d k).card := by
+    (↑(d ^ n) / ((n * (d - 1) ^ 2 :) + 1) : ℝ) ≤ #(sphere n d k) := by
   refine exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => ?_) nonempty_range_succ ?_
   · rw [mem_range, Nat.lt_succ_iff]
     exact sum_sq_le_of_mem_box hx
@@ -238,7 +237,7 @@ theorem exists_large_sphere_aux (n d : ℕ) : ∃ k ∈ range (n * (d - 1) ^ 2 +
     exact (cast_add_one_pos _).ne'
 
 theorem exists_large_sphere (n d : ℕ) :
-    ∃ k, ((d ^ n :) / (n * d ^ 2 :) : ℝ) ≤ (sphere n d k).card := by
+    ∃ k, ((d ^ n :) / (n * d ^ 2 :) : ℝ) ≤ #(sphere n d k) := by
   obtain ⟨k, -, hk⟩ := exists_large_sphere_aux n d
   refine ⟨k, ?_⟩
   obtain rfl | hn := n.eq_zero_or_pos

Mathlib/Combinatorics/Additive/AP/Three/Defs.lean

@@ -253,31 +253,31 @@ subset.
 
 The usual Roth number corresponds to `addRothNumber (Finset.range n)`, see `rothNumberNat`."]
 def mulRothNumber : Finset α →o ℕ :=
-  ⟨fun s ↦ Nat.findGreatest (fun m ↦ ∃ t ⊆ s, t.card = m ∧ ThreeGPFree (t : Set α)) s.card, by
+  ⟨fun s ↦ Nat.findGreatest (fun m ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (t : Set α)) #s, by
     rintro t u htu
     refine Nat.findGreatest_mono (fun m => ?_) (card_le_card htu)
     rintro ⟨v, hvt, hv⟩
     exact ⟨v, hvt.trans htu, hv⟩⟩
 
 @[to_additive]
-theorem mulRothNumber_le : mulRothNumber s ≤ s.card := Nat.findGreatest_le s.card
+theorem mulRothNumber_le : mulRothNumber s ≤ #s := Nat.findGreatest_le #s
 
 @[to_additive]
 theorem mulRothNumber_spec :
-    ∃ t ⊆ s, t.card = mulRothNumber s ∧ ThreeGPFree (t : Set α) :=
-  Nat.findGreatest_spec (P := fun m ↦ ∃ t ⊆ s, t.card = m ∧ ThreeGPFree (t : Set α))
+    ∃ t ⊆ s, #t = mulRothNumber s ∧ ThreeGPFree (t : Set α) :=
+  Nat.findGreatest_spec (P := fun m ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (t : Set α))
     (Nat.zero_le _) ⟨∅, empty_subset _, card_empty, by norm_cast; exact threeGPFree_empty⟩
 
 variable {s t} {n : ℕ}
 
 @[to_additive]
 theorem ThreeGPFree.le_mulRothNumber (hs : ThreeGPFree (s : Set α)) (h : s ⊆ t) :
-    s.card ≤ mulRothNumber t :=
+    #s ≤ mulRothNumber t :=
   Nat.le_findGreatest (card_le_card h) ⟨s, h, rfl, hs⟩
 
 @[to_additive]
 theorem ThreeGPFree.mulRothNumber_eq (hs : ThreeGPFree (s : Set α)) :
-    mulRothNumber s = s.card :=
+    mulRothNumber s = #s :=
   (mulRothNumber_le _).antisymm <| hs.le_mulRothNumber <| Subset.refl _
 
 @[to_additive (attr := simp)]
@@ -295,9 +295,9 @@ theorem mulRothNumber_union_le (s t : Finset α) :
     mulRothNumber (s ∪ t) ≤ mulRothNumber s + mulRothNumber t :=
   let ⟨u, hus, hcard, hu⟩ := mulRothNumber_spec (s ∪ t)
   calc
-    mulRothNumber (s ∪ t) = u.card := hcard.symm
-    _ = (u ∩ s ∪ u ∩ t).card := by rw [← inter_union_distrib_left, inter_eq_left.2 hus]
-    _ ≤ (u ∩ s).card + (u ∩ t).card := card_union_le _ _
+    mulRothNumber (s ∪ t) = #u := hcard.symm
+    _ = #(u ∩ s ∪ u ∩ t) := by rw [← inter_union_distrib_left, inter_eq_left.2 hus]
+    _ ≤ #(u ∩ s) + #(u ∩ t) := card_union_le _ _
     _ ≤ mulRothNumber s + mulRothNumber t := _root_.add_le_add
       ((hu.mono inter_subset_left).le_mulRothNumber inter_subset_right)
       ((hu.mono inter_subset_left).le_mulRothNumber inter_subset_right)
@@ -407,13 +407,13 @@ theorem rothNumberNat_le (N : ℕ) : rothNumberNat N ≤ N :=
   (addRothNumber_le _).trans (card_range _).le
 
 theorem rothNumberNat_spec (n : ℕ) :
-    ∃ t ⊆ range n, t.card = rothNumberNat n ∧ ThreeAPFree (t : Set ℕ) :=
+    ∃ t ⊆ range n, #t = rothNumberNat n ∧ ThreeAPFree (t : Set ℕ) :=
   addRothNumber_spec _
 
 /-- A verbose specialization of `threeAPFree.le_addRothNumber`, sometimes convenient in
 practice. -/
 theorem ThreeAPFree.le_rothNumberNat (s : Finset ℕ) (hs : ThreeAPFree (s : Set ℕ))
-    (hsn : ∀ x ∈ s, x < n) (hsk : s.card = k) : k ≤ rothNumberNat n :=
+    (hsn : ∀ x ∈ s, x < n) (hsk : #s = k) : k ≤ rothNumberNat n :=
   hsk.ge.trans <| hs.le_addRothNumber fun x hx => mem_range.2 <| hsn x hx
 
 /-- The Roth number is a subadditive function. Note that by Fekete's lemma this shows that

Mathlib/Combinatorics/Additive/Corner/Roth.lean

@@ -40,7 +40,7 @@ private lemma mk_mem_triangleIndices : (a, b, c) ∈ triangleIndices A ↔ (a, b
   rintro ⟨_, _, h₁, rfl, rfl, h₂⟩
   exact ⟨h₁, h₂⟩
 
-@[simp] private lemma card_triangleIndices : (triangleIndices A).card = A.card := card_map _
+@[simp] private lemma card_triangleIndices : #(triangleIndices A) = #A := card_map _
 
 private instance triangleIndices.instExplicitDisjoint : ExplicitDisjoint (triangleIndices A) := by
   constructor
@@ -55,7 +55,7 @@ private lemma noAccidental (hs : IsCornerFree (A : Set (G × G))) :
     simp only [mk_mem_triangleIndices] at ha hb hc
     exact .inl <| hs ⟨hc.1, hb.1, ha.1, hb.2.symm.trans ha.2⟩
 
-private lemma farFromTriangleFree_graph [Fintype G] [DecidableEq G] (hε : ε * card G ^ 2 ≤ A.card) :
+private lemma farFromTriangleFree_graph [Fintype G] [DecidableEq G] (hε : ε * card G ^ 2 ≤ #A) :
     (graph <| triangleIndices A).FarFromTriangleFree (ε / 9) := by
   refine farFromTriangleFree _ ?_
   simp_rw [card_triangleIndices, mul_comm_div, Nat.cast_pow, Nat.cast_add]
@@ -79,7 +79,7 @@ noncomputable def cornersTheoremBound (ε : ℝ) : ℕ := ⌊(triangleRemovalBou
 
 The maximum density of a corner-free set in `G × G` goes to zero as `|G|` tends to infinity. -/
 theorem corners_theorem (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound ε ≤ card G)
-    (A : Finset (G × G)) (hAε : ε * card G ^ 2 ≤ A.card) : ¬ IsCornerFree (A : Set (G × G)) := by
+    (A : Finset (G × G)) (hAε : ε * card G ^ 2 ≤ #A) : ¬ IsCornerFree (A : Set (G × G)) := by
   rintro hA
   rw [cornersTheoremBound, Nat.add_one_le_iff] at hG
   have hε₁ : ε ≤ 1 := by
@@ -103,7 +103,7 @@ theorem corners_theorem (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound ε 
 The maximum density of a corner-free set in `{1, ..., n} × {1, ..., n}` goes to zero as `n` tends to
 infinity. -/
 theorem corners_theorem_nat (hε : 0 < ε) (hn : cornersTheoremBound (ε / 9) ≤ n)
-    (A : Finset (ℕ × ℕ)) (hAn : A ⊆ range n ×ˢ range n) (hAε : ε * n ^ 2 ≤ A.card) :
+    (A : Finset (ℕ × ℕ)) (hAn : A ⊆ range n ×ˢ range n) (hAε : ε * n ^ 2 ≤ #A) :
     ¬ IsCornerFree (A : Set (ℕ × ℕ)) := by
   rintro hA
   rw [← coe_subset, coe_product] at hAn
@@ -128,7 +128,7 @@ theorem corners_theorem_nat (hε : 0 < ε) (hn : cornersTheoremBound (ε / 9) 
     _ = ε / 9 * (2 * n + 1) ^ 2 := by simp
     _ ≤ ε / 9 * (2 * n + n) ^ 2 := by gcongr; simp; unfold cornersTheoremBound at hn; omega
     _ = ε * n ^ 2 := by ring
-    _ ≤ A.card := hAε
+    _ ≤ #A := hAε
     _ = _ := by
       rw [card_image_of_injOn]
       have : Set.InjOn Nat.cast (range n) :=
@@ -139,15 +139,15 @@ theorem corners_theorem_nat (hε : 0 < ε) (hn : cornersTheoremBound (ε / 9) 
 
 The maximum density of a 3AP-free set in `G` goes to zero as `|G|` tends to infinity. -/
 theorem roth_3ap_theorem (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound ε ≤ card G)
-    (A : Finset G) (hAε : ε * card G ≤ A.card) : ¬ ThreeAPFree (A : Set G) := by
+    (A : Finset G) (hAε : ε * card G ≤ #A) : ¬ ThreeAPFree (A : Set G) := by
   rintro hA
   classical
   let B : Finset (G × G) := univ.filter fun (x, y) ↦ y - x ∈ A
-  have : ε * card G ^ 2 ≤ B.card := by
+  have : ε * card G ^ 2 ≤ #B := by
     calc
       _ = card G * (ε * card G) := by ring
-      _ ≤ card G * A.card := by gcongr
-      _ = B.card := ?_
+      _ ≤ card G * #A := by gcongr
+      _ = #B := ?_
     norm_cast
     rw [← card_univ, ← card_product]
     exact card_equiv ((Equiv.refl _).prodShear fun a ↦ Equiv.addLeft a) (by simp [B])
@@ -164,7 +164,7 @@ theorem roth_3ap_theorem (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound ε
 
 The maximum density of a 3AP-free set in `{1, ..., n}` goes to zero as `n` tends to infinity. -/
 theorem roth_3ap_theorem_nat (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound (ε / 3) ≤ n)
-    (A : Finset ℕ) (hAn : A ⊆ range n) (hAε : ε * n ≤ A.card) : ¬ ThreeAPFree (A : Set ℕ) := by
+    (A : Finset ℕ) (hAn : A ⊆ range n) (hAε : ε * n ≤ #A) : ¬ ThreeAPFree (A : Set ℕ) := by
   rintro hA
   rw [← coe_subset, coe_range] at hAn
   have : A = Fin.val '' (Nat.cast '' A : Set (Fin (2 * n).succ)) := by
@@ -185,7 +185,7 @@ theorem roth_3ap_theorem_nat (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound
     _ = ε / 3 * (2 * n + 1) := by simp
     _ ≤ ε / 3 * (2 * n + n) := by gcongr; simp; unfold cornersTheoremBound at hG; omega
     _ = ε * n := by ring
-    _ ≤ A.card := hAε
+    _ ≤ #A := hAε
     _ = _ := by
       rw [card_image_of_injOn]
       exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by

Mathlib/Combinatorics/Additive/DoublingConst.lean

@@ -30,7 +30,7 @@ The notation `σₘ[A, B]` is available in scope `Combinatorics.Additive`. -/
 "The doubling constant `σ[A, B]` of two finsets `A` and `B` in a group is `|A + B| / |A|`.
 
 The notation `σ[A, B]` is available in scope `Combinatorics.Additive`."]
-def mulConst (A B : Finset G) : ℚ≥0 := (A * B).card / A.card
+def mulConst (A B : Finset G) : ℚ≥0 := #(A * B) / #A
 
 /-- The difference constant `δₘ[A, B]` of two finsets `A` and `B` in a group is `|A / B| / |A|`.
 
@@ -39,7 +39,7 @@ The notation `δₘ[A, B]` is available in scope `Combinatorics.Additive`. -/
 "The difference constant `σ[A, B]` of two finsets `A` and `B` in a group is `|A - B| / |A|`.
 
 The notation `δ[A, B]` is available in scope `Combinatorics.Additive`."]
-def divConst (A B : Finset G) : ℚ≥0 := (A / B).card / A.card
+def divConst (A B : Finset G) : ℚ≥0 := #(A / B) / #A
 
 /-- The doubling constant `σₘ[A, B]` of two finsets `A` and `B` in a group is `|A * B| / |A|`. -/
 scoped[Combinatorics.Additive] notation3:max "σₘ[" A ", " B "]" => Finset.mulConst A B
@@ -68,23 +68,23 @@ scoped[Combinatorics.Additive] notation3:max "δ[" A "]" => Finset.subConst A A
 open scoped Combinatorics.Additive
 
 @[to_additive (attr := simp) addConst_mul_card]
-lemma mulConst_mul_card (A B : Finset G) : σₘ[A, B] * A.card = (A * B).card := by
+lemma mulConst_mul_card (A B : Finset G) : σₘ[A, B] * #A = #(A * B) := by
   obtain rfl | hA := A.eq_empty_or_nonempty
   · simp
   · exact div_mul_cancel₀ _ (by positivity)
 
 @[to_additive (attr := simp) subConst_mul_card]
-lemma divConst_mul_card (A B : Finset G) : δₘ[A, B] * A.card = (A / B).card := by
+lemma divConst_mul_card (A B : Finset G) : δₘ[A, B] * #A = #(A / B) := by
   obtain rfl | hA := A.eq_empty_or_nonempty
   · simp
   · exact div_mul_cancel₀ _ (by positivity)
 
 @[to_additive (attr := simp) card_mul_addConst]
-lemma card_mul_mulConst (A B : Finset G) : A.card * σₘ[A, B] = (A * B).card := by
+lemma card_mul_mulConst (A B : Finset G) : #A * σₘ[A, B] = #(A * B) := by
   rw [mul_comm, mulConst_mul_card]
 
 @[to_additive (attr := simp) card_mul_subConst]
-lemma card_mul_divConst (A B : Finset G) : A.card * δₘ[A, B] = (A / B).card := by
+lemma card_mul_divConst (A B : Finset G) : #A * δₘ[A, B] = #(A / B) := by
   rw [mul_comm, divConst_mul_card]
 
 @[to_additive (attr := simp)]
@@ -124,44 +124,44 @@ end Fintype
 
 variable {𝕜 : Type*} [Semifield 𝕜] [CharZero 𝕜]
 
-lemma cast_addConst (A B : Finset G') : (σ[A, B] : 𝕜) = (A + B).card / A.card := by
+lemma cast_addConst (A B : Finset G') : (σ[A, B] : 𝕜) = #(A + B) / #A := by
   simp [addConst]
 
-lemma cast_subConst (A B : Finset G') : (δ[A, B] : 𝕜) = (A - B).card / A.card := by
+lemma cast_subConst (A B : Finset G') : (δ[A, B] : 𝕜) = #(A - B) / #A := by
   simp [subConst]
 
 @[to_additive existing]
-lemma cast_mulConst (A B : Finset G) : (σₘ[A, B] : 𝕜) = (A * B).card / A.card := by simp [mulConst]
+lemma cast_mulConst (A B : Finset G) : (σₘ[A, B] : 𝕜) = #(A * B) / #A := by simp [mulConst]
 
 @[to_additive existing]
-lemma cast_divConst (A B : Finset G) : (δₘ[A, B] : 𝕜) = (A / B).card / A.card := by simp [divConst]
+lemma cast_divConst (A B : Finset G) : (δₘ[A, B] : 𝕜) = #(A / B) / #A := by simp [divConst]
 
-lemma cast_addConst_mul_card (A B : Finset G') : (σ[A, B] * A.card : 𝕜) = (A + B).card := by
+lemma cast_addConst_mul_card (A B : Finset G') : (σ[A, B] * #A : 𝕜) = #(A + B) := by
   norm_cast; exact addConst_mul_card _ _
 
-lemma cast_subConst_mul_card (A B : Finset G') : (δ[A, B] * A.card : 𝕜) = (A - B).card := by
+lemma cast_subConst_mul_card (A B : Finset G') : (δ[A, B] * #A : 𝕜) = #(A - B) := by
   norm_cast; exact subConst_mul_card _ _
 
-lemma card_mul_cast_addConst (A B : Finset G') : (A.card * σ[A, B] : 𝕜) = (A + B).card := by
+lemma card_mul_cast_addConst (A B : Finset G') : (#A * σ[A, B] : 𝕜) = #(A + B) := by
   norm_cast; exact card_mul_addConst _ _
 
-lemma card_mul_cast_subConst (A B : Finset G') : (A.card * δ[A, B] : 𝕜) = (A - B).card := by
+lemma card_mul_cast_subConst (A B : Finset G') : (#A * δ[A, B] : 𝕜) = #(A - B) := by
   norm_cast; exact card_mul_subConst _ _
 
 @[to_additive (attr := simp) existing cast_addConst_mul_card]
-lemma cast_mulConst_mul_card (A B : Finset G) : (σₘ[A, B] * A.card : 𝕜) = (A * B).card := by
+lemma cast_mulConst_mul_card (A B : Finset G) : (σₘ[A, B] * #A : 𝕜) = #(A * B) := by
   norm_cast; exact mulConst_mul_card _ _
 
 @[to_additive (attr := simp) existing cast_subConst_mul_card]
-lemma cast_divConst_mul_card (A B : Finset G) : (δₘ[A, B] * A.card : 𝕜) = (A / B).card := by
+lemma cast_divConst_mul_card (A B : Finset G) : (δₘ[A, B] * #A : 𝕜) = #(A / B) := by
   norm_cast; exact divConst_mul_card _ _
 
 @[to_additive (attr := simp) existing card_mul_cast_addConst]
-lemma card_mul_cast_mulConst (A B : Finset G) : (A.card * σₘ[A, B] : 𝕜) = (A * B).card := by
+lemma card_mul_cast_mulConst (A B : Finset G) : (#A * σₘ[A, B] : 𝕜) = #(A * B) := by
   norm_cast; exact card_mul_mulConst _ _
 
 @[to_additive (attr := simp) existing card_mul_cast_subConst]
-lemma card_mul_cast_divConst (A B : Finset G) : (A.card * δₘ[A, B] : 𝕜) = (A / B).card := by
+lemma card_mul_cast_divConst (A B : Finset G) : (#A * δₘ[A, B] : 𝕜) = #(A / B) := by
   norm_cast; exact card_mul_divConst _ _
 
 end Group
@@ -189,10 +189,10 @@ This is a consequence of the Ruzsa triangle inequality."]
 lemma mulConst_le_divConst_sq : σₘ[A] ≤ δₘ[A] ^ 2 := by
   obtain rfl | hA' := A.eq_empty_or_nonempty
   · simp
-  refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < A.card * A.card)
+  refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)
   calc
-    _ = (A * A).card * (A.card : ℚ≥0) := by rw [← mul_assoc, mulConst_mul_card]
-    _ ≤ (A / A).card * (A / A).card := by norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..
+    _ = #(A * A) * (#A : ℚ≥0) := by rw [← mul_assoc, mulConst_mul_card]
+    _ ≤ #(A / A) * #(A / A) := by norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..
     _ = _ := by rw [← divConst_mul_card]; ring
 
 /-- If `A` has small doubling, then it has small difference, with the constant squared.
@@ -205,10 +205,10 @@ This is a consequence of the Ruzsa triangle inequality."]
 lemma divConst_le_mulConst_sq : δₘ[A] ≤ σₘ[A] ^ 2 := by
   obtain rfl | hA' := A.eq_empty_or_nonempty
   · simp
-  refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < A.card * A.card)
+  refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)
   calc
-    _ = (A / A).card * (A.card : ℚ≥0) := by rw [← mul_assoc, divConst_mul_card]
-    _ ≤ (A * A).card * (A * A).card := by norm_cast; exact ruzsa_triangle_inequality_div_mul_mul ..
+    _ = #(A / A) * (#A : ℚ≥0) := by rw [← mul_assoc, divConst_mul_card]
+    _ ≤ #(A * A) * #(A * A) := by norm_cast; exact ruzsa_triangle_inequality_div_mul_mul ..
     _ = _ := by rw [← mulConst_mul_card]; ring
 
 end CommGroup