chore: use newly introduced finset notation

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/AlgebraicTopology/SimplicialSet/Basic.lean

@@ -221,8 +221,7 @@ def const (n : ℕ) (i k : Fin (n+3)) (m : SimplexCategoryᵒᵖ) : Λ[n+2, i].o
 
 This edge only exists if `{i, a, b}` has cardinality less than `n`. -/
 @[simps]
-def edge (n : ℕ) (i a b : Fin (n+1)) (hab : a ≤ b) (H : Finset.card {i, a, b} ≤ n) :
-    Λ[n, i] _[1] := by
+def edge (n : ℕ) (i a b : Fin (n+1)) (hab : a ≤ b) (H : #{i, a, b} ≤ n) : Λ[n, i] _[1] := by
   refine ⟨standardSimplex.edge n a b hab, ?range⟩
   case range =>
     suffices ∃ x, ¬i = x ∧ ¬a = x ∧ ¬b = x by

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -512,8 +512,8 @@ theorem dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq (h : Integra
   -- Let us prove that the distance is less than or equal to `ε + δ` for all positive `δ`.
   refine le_of_forall_pos_le_add fun δ δ0 => ?_
   -- First we choose some constants.
-  set δ' : ℝ := δ / (π₀.boxes.card + 1)
-  have H0 : 0 < (π₀.boxes.card + 1 : ℝ) := Nat.cast_add_one_pos _
+  set δ' : ℝ := δ / (#π₀.boxes + 1)
+  have H0 : 0 < (#π₀.boxes + 1 : ℝ) := Nat.cast_add_one_pos _
   have δ'0 : 0 < δ' := div_pos δ0 H0
   set C := max π₀.distortion π₀.compl.distortion
   /- Next we choose a tagged partition of each `J ∈ π₀` such that the integral sum of `f` over this
@@ -665,7 +665,7 @@ theorem integrable_of_bounded_and_ae_continuousWithinAt [CompleteSpace E] {I : B
   let t₂ (J : Box ι) : ℝⁿ := (π₂.infPrepartition π₁.toPrepartition).tag J
   let B := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
   classical
-  let B' := B.filter (fun J ↦ J.toSet ⊆ U)
+  let B' := {J ∈ B | J.toSet ⊆ U}
   have hB' : B' ⊆ B := B.filter_subset (fun J ↦ J.toSet ⊆ U)
   have μJ_ne_top : ∀ J ∈ B, μ J ≠ ⊤ :=
     fun J hJ ↦ lt_top_iff_ne_top.1 <| lt_of_le_of_lt (μ.mono (Prepartition.le_of_mem' _ J hJ)) μI
@@ -795,7 +795,7 @@ theorem HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (hl : l.bRiemann =
     /- For the boxes such that `π.tag J ∈ s`, we use the fact that at most `2 ^ #ι` boxes have the
         same tag. -/
     specialize hlH hsne
-    have : ∀ J ∈ π.boxes.filter fun J => π.tag J ∈ s,
+    have : ∀ J ∈ {J ∈ π.boxes | π.tag J ∈ s},
         dist (vol J (f <| π.tag J)) (g J) ≤ εs (π.tag J) := fun J hJ ↦ by
       rw [Finset.mem_filter] at hJ; cases' hJ with hJ hJs
       refine Hδ₁ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ (hεs0 _) _ (π.le_of_mem' _ hJ) ?_
@@ -815,9 +815,9 @@ theorem HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (hl : l.bRiemann =
     In this case the estimate is straightforward. -/
   -- Porting note: avoided strange elaboration issues by rewriting using `calc`
   calc
-    dist (∑ J ∈ π.boxes.filter (¬tag π · ∈ s), vol J (f (tag π J)))
-      (∑ J ∈ π.boxes.filter (¬tag π · ∈ s), g J)
-      ≤ ∑ J ∈ π.boxes.filter (¬tag π · ∈ s), ε' * B J := dist_sum_sum_le_of_le _ fun J hJ ↦ by
+    dist (∑ J ∈ π.boxes with ¬tag π J ∈ s, vol J (f (tag π J)))
+      (∑ J ∈ π.boxes with ¬tag π J ∈ s, g J)
+      ≤ ∑ J ∈ π.boxes with ¬tag π J ∈ s, ε' * B J := dist_sum_sum_le_of_le _ fun J hJ ↦ by
       rw [Finset.mem_filter] at hJ; cases' hJ with hJ hJs
       refine Hδ₂ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ ε'0 _ (π.le_of_mem' _ hJ) ?_ (fun hH => hπδ.2 hH J hJ)
         fun hD => (Finset.le_sup hJ).trans (hπδ.3 hD)

Mathlib/Analysis/BoxIntegral/Partition/Basic.lean

@@ -177,7 +177,7 @@ theorem injOn_setOf_mem_Icc_setOf_lower_eq (x : ι → ℝ) :
 /-- The set of boxes of a prepartition that contain `x` in their closures has cardinality
 at most `2 ^ Fintype.card ι`. -/
 theorem card_filter_mem_Icc_le [Fintype ι] (x : ι → ℝ) :
-    (π.boxes.filter fun J : Box ι => x ∈ Box.Icc J).card ≤ 2 ^ Fintype.card ι := by
+    #{J ∈ π.boxes | x ∈ Box.Icc J} ≤ 2 ^ Fintype.card ι := by
   rw [← Fintype.card_set]
   refine Finset.card_le_card_of_injOn (fun J : Box ι => { i | J.lower i = x i })
     (fun _ _ => Finset.mem_univ _) ?_
@@ -517,7 +517,7 @@ instance : SemilatticeInf (Prepartition I) :=
 /-- The prepartition with boxes `{J ∈ π | p J}`. -/
 @[simps]
 def filter (π : Prepartition I) (p : Box ι → Prop) : Prepartition I where
-  boxes := π.boxes.filter p
+  boxes := {J ∈ π.boxes | p J}
   le_of_mem' _ hJ := π.le_of_mem (mem_filter.1 hJ).1
   pairwiseDisjoint _ h₁ _ h₂ := π.disjoint_coe_of_mem (mem_filter.1 h₁).1 (mem_filter.1 h₂).1
 

Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean

@@ -25,10 +25,8 @@ rectangular box, box partition
 
 noncomputable section
 
+open Finset Function ENNReal NNReal Set
 open scoped Classical
-open ENNReal NNReal
-
-open Set Function
 
 namespace BoxIntegral
 
@@ -204,10 +202,9 @@ theorem isHenstock_biUnionTagged {π : Prepartition I} {πi : ∀ J, TaggedPrepa
 
 /-- In a Henstock prepartition, there are at most `2 ^ Fintype.card ι` boxes with a given tag. -/
 theorem IsHenstock.card_filter_tag_eq_le [Fintype ι] (h : π.IsHenstock) (x : ι → ℝ) :
-    (π.boxes.filter fun J => π.tag J = x).card ≤ 2 ^ Fintype.card ι :=
+    #{J ∈ π.boxes | π.tag J = x} ≤ 2 ^ Fintype.card ι :=
   calc
-    (π.boxes.filter fun J => π.tag J = x).card ≤
-        (π.boxes.filter fun J : Box ι => x ∈ Box.Icc J).card := by
+    #{J ∈ π.boxes | π.tag J = x} ≤ #{J ∈ π.boxes | x ∈ Box.Icc J} := by
       refine Finset.card_le_card fun J hJ => ?_
       rw [Finset.mem_filter] at hJ ⊢; rcases hJ with ⟨hJ, rfl⟩
       exact ⟨hJ, h J hJ⟩

Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

@@ -619,7 +619,7 @@ theorem changeOrigin_toFormalMultilinearSeries [DecidableEq ι] :
       rw [card_compl, Fintype.card_fin, Finset.card_singleton, Nat.add_sub_cancel_left]⟩)
   · use fun _ _ ↦ (singleton_injective <| compl_injective <| Subtype.ext_iff.mp ·)
     intro ⟨s, hs⟩
-    have h : sᶜ.card = 1 := by rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]
+    have h : #sᶜ = 1 := by rw [card_compl, hs, Fintype.card_fin, Nat.add_sub_cancel]
     obtain ⟨a, ha⟩ := card_eq_one.mp h
     exact ⟨a, Subtype.ext (compl_eq_comm.mp ha)⟩
   rw [Function.comp_apply, Subtype.coe_mk, compl_singleton, piecewise_erase_univ,

Mathlib/Analysis/Convex/Birkhoff.lean

@@ -46,13 +46,13 @@ private lemma exists_perm_eq_zero_implies_eq_zero [Nonempty n] {s : R} (hs : 0 <
     (hM : ∃ M' ∈ doublyStochastic R n, M = s • M') :
     ∃ σ : Equiv.Perm n, ∀ i j, M i j = 0 → σ.permMatrix R i j = 0 := by
   rw [exists_mem_doublyStochastic_eq_smul_iff hs.le] at hM
-  let f (i : n) : Finset n := univ.filter (M i · ≠ 0)
-  have hf (A : Finset n) : A.card ≤ (A.biUnion f).card := by
+  let f (i : n) : Finset n := {j | M i j ≠ 0}
+  have hf (A : Finset n) : #A ≤ #(A.biUnion f) := by
     have (i) : ∑ j ∈ f i, M i j = s := by simp [sum_subset (filter_subset _ _), hM.2.1]
-    have h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = A.card * s := by simp [this]
-    have h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = (A.biUnion f).card * s := by
+    have h₁ : ∑ i ∈ A, ∑ j ∈ f i, M i j = #A * s := by simp [this]
+    have h₂ : ∑ i, ∑ j ∈ A.biUnion f, M i j = #(A.biUnion f) * s := by
       simp [sum_comm (t := A.biUnion f), hM.2.2, mul_comm s]
-    suffices A.card * s ≤ (A.biUnion f).card * s by exact_mod_cast le_of_mul_le_mul_right this hs
+    suffices #A * s ≤ #(A.biUnion f) * s by exact_mod_cast le_of_mul_le_mul_right this hs
     rw [← h₁, ← h₂]
     trans ∑ i ∈ A, ∑ j ∈ A.biUnion f, M i j
     · refine sum_le_sum fun i hi => ?_
@@ -86,7 +86,7 @@ private lemma doublyStochastic_sum_perm_aux (M : Matrix n n R)
     ∃ w : Equiv.Perm n → R, (∀ σ, 0 ≤ w σ) ∧ ∑ σ, w σ • σ.permMatrix R = M := by
   rcases isEmpty_or_nonempty n
   case inl => exact ⟨1, by simp, Subsingleton.elim _ _⟩
-  set d : ℕ := (Finset.univ.filter fun i : n × n => M i.1 i.2 ≠ 0).card with ← hd
+  set d : ℕ := #{i : n × n | M i.1 i.2 ≠ 0} with ← hd
   clear_value d
   induction d using Nat.strongRecOn generalizing M s
   case ind d ih =>
@@ -114,7 +114,7 @@ private lemma doublyStochastic_sum_perm_aux (M : Matrix n n R)
     split
     case isTrue h => exact (hi' i' (by simp)).trans_eq (by rw [h])
     case isFalse h => exact hM.1 _ _
-  have hd' : (univ.filter fun i : n × n => N i.1 i.2 ≠ 0).card < d := by
+  have hd' : #{i : n × n | N i.1 i.2 ≠ 0} < d := by
     rw [← hd]
     refine card_lt_card ?_
     rw [ssubset_iff_of_subset (monotone_filter_right _ _)]

Mathlib/Analysis/Convex/Caratheodory.lean

@@ -55,7 +55,7 @@ theorem mem_convexHull_erase [DecidableEq E] {t : Finset E} (h : ¬AffineIndepen
   obtain ⟨g, gcombo, gsum, gpos⟩ := exists_nontrivial_relation_sum_zero_of_not_affine_ind h
   replace gpos := exists_pos_of_sum_zero_of_exists_nonzero g gsum gpos
   clear h
-  let s := @Finset.filter _ (fun z => 0 < g z) (fun _ => LinearOrder.decidableLT _ _) t
+  let s := {z ∈ t | 0 < g z}
   obtain ⟨i₀, mem, w⟩ : ∃ i₀ ∈ s, ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i := by
     apply s.exists_min_image fun z => f z / g z
     obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos
@@ -117,13 +117,13 @@ theorem minCardFinsetOfMemConvexHull_nonempty : (minCardFinsetOfMemConvexHull hx
   exact ⟨x, mem_minCardFinsetOfMemConvexHull hx⟩
 
 theorem minCardFinsetOfMemConvexHull_card_le_card {t : Finset E} (ht₁ : ↑t ⊆ s)
-    (ht₂ : x ∈ convexHull 𝕜 (t : Set E)) : (minCardFinsetOfMemConvexHull hx).card ≤ t.card :=
+    (ht₂ : x ∈ convexHull 𝕜 (t : Set E)) : #(minCardFinsetOfMemConvexHull hx) ≤ #t :=
   Function.argminOn_le _ _ _ (by exact ⟨ht₁, ht₂⟩)
 
 theorem affineIndependent_minCardFinsetOfMemConvexHull :
     AffineIndependent 𝕜 ((↑) : minCardFinsetOfMemConvexHull hx → E) := by
-  let k := (minCardFinsetOfMemConvexHull hx).card - 1
-  have hk : (minCardFinsetOfMemConvexHull hx).card = k + 1 :=
+  let k := #(minCardFinsetOfMemConvexHull hx) - 1
+  have hk : #(minCardFinsetOfMemConvexHull hx) = k + 1 :=
     (Nat.succ_pred_eq_of_pos (Finset.card_pos.mpr (minCardFinsetOfMemConvexHull_nonempty hx))).symm
   classical
   by_contra h
@@ -163,7 +163,7 @@ theorem eq_pos_convex_span_of_mem_convexHull {x : E} (hx : x ∈ convexHull 𝕜
   obtain ⟨t, ht₁, ht₂, ht₃⟩ := hx
   simp only [t.convexHull_eq, exists_prop, Set.mem_setOf_eq] at ht₃
   obtain ⟨w, hw₁, hw₂, hw₃⟩ := ht₃
-  let t' := t.filter fun i => w i ≠ 0
+  let t' := {i ∈ t | w i ≠ 0}
   refine ⟨t', t'.fintypeCoeSort, ((↑) : t' → E), w ∘ ((↑) : t' → E), ?_, ?_, ?_, ?_, ?_⟩
   · rw [Subtype.range_coe_subtype]
     exact Subset.trans (Finset.filter_subset _ t) ht₁

Mathlib/Analysis/Convex/Combination.lean

@@ -124,8 +124,7 @@ theorem Finset.centerMass_subset {t' : Finset ι} (ht : t ⊆ t') (h : ∀ i ∈
   intro i hit' hit
   rw [h i hit' hit, zero_smul, smul_zero]
 
-theorem Finset.centerMass_filter_ne_zero :
-    (t.filter fun i => w i ≠ 0).centerMass w z = t.centerMass w z :=
+theorem Finset.centerMass_filter_ne_zero : {i ∈ t | w i ≠ 0}.centerMass w z = t.centerMass w z :=
   Finset.centerMass_subset z (filter_subset _ _) fun i hit hit' => by
     simpa only [hit, mem_filter, true_and, Ne, Classical.not_not] using hit'
 
@@ -264,7 +263,7 @@ theorem Finset.centroid_mem_convexHull (s : Finset E) (hs : s.Nonempty) :
   rw [s.centroid_eq_centerMass hs]
   apply s.centerMass_id_mem_convexHull
   · simp only [inv_nonneg, imp_true_iff, Nat.cast_nonneg, Finset.centroidWeights_apply]
-  · have hs_card : (s.card : R) ≠ 0 := by simp [Finset.nonempty_iff_ne_empty.mp hs]
+  · have hs_card : (#s : R) ≠ 0 := by simp [Finset.nonempty_iff_ne_empty.mp hs]
     simp only [hs_card, Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀, Ne, not_false_iff,
       Finset.centroidWeights_apply, zero_lt_one]
 

Mathlib/Analysis/Convex/Jensen.lean

@@ -271,8 +271,8 @@ lemma ConvexOn.exists_ge_of_centerMass {t : Finset ι} (h : ConvexOn 𝕜 s f)
     ∃ i ∈ t, f (t.centerMass w p) ≤ f (p i) := by
   set y := t.centerMass w p
   -- TODO: can `rsuffices` be used to write the `exact` first, then the proof of this obtain?
-  obtain ⟨i, hi, hfi⟩ : ∃ i ∈ t.filter fun i => w i ≠ 0, w i • f y ≤ w i • (f ∘ p) i := by
-    have hw' : (0 : 𝕜) < ∑ i ∈ filter (fun i => w i ≠ 0) t, w i := by rwa [sum_filter_ne_zero]
+  obtain ⟨i, hi, hfi⟩ : ∃ i ∈ {i ∈ t | w i ≠ 0}, w i • f y ≤ w i • (f ∘ p) i := by
+    have hw' : (0 : 𝕜) < ∑ i ∈ t with w i ≠ 0, w i := by rwa [sum_filter_ne_zero]
     refine exists_le_of_sum_le (nonempty_of_sum_ne_zero hw'.ne') ?_
     rw [← sum_smul, ← smul_le_smul_iff_of_pos_left (inv_pos.2 hw'), inv_smul_smul₀ hw'.ne', ←
       centerMass, centerMass_filter_ne_zero]

Mathlib/Analysis/Convex/Radon.lean

@@ -41,8 +41,8 @@ theorem radon_partition {f : ι → E} (h : ¬ AffineIndependent 𝕜 f) :
   rw [affineIndependent_iff] at h
   push_neg at h
   obtain ⟨s, w, h_wsum, h_vsum, nonzero_w_index, h1, h2⟩ := h
-  let I : Finset ι := s.filter fun i ↦ 0 ≤ w i
-  let J : Finset ι := s.filter fun i ↦ w i < 0
+  let I : Finset ι := {i ∈ s | 0 ≤ w i}
+  let J : Finset ι := {i ∈ s | w i < 0}
   let p : E := centerMass I w f -- point of intersection
   have hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0 := by
     simpa only [h_wsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) w
@@ -66,8 +66,8 @@ open Module
 
 /-- Corner case for `helly_theorem'`. -/
 private lemma helly_theorem_corner {F : ι → Set E} {s : Finset ι}
-    (h_card_small : s.card ≤ finrank 𝕜 E + 1)
-    (h_inter : ∀ I ⊆ s, I.card ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
+    (h_card_small : #s ≤ finrank 𝕜 E + 1)
+    (h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
     (⋂ i ∈ s, F i).Nonempty := h_inter s (by simp) h_card_small
 
 variable [FiniteDimensional 𝕜 E]
@@ -78,12 +78,12 @@ If `F` is a finite family of convex sets in a vector space of finite dimension `
 `k ≤ d + 1` sets of `F` intersect nontrivially, then all sets of `F` intersect nontrivially. -/
 theorem helly_theorem' {F : ι → Set E} {s : Finset ι}
     (h_convex : ∀ i ∈ s, Convex 𝕜 (F i))
-    (h_inter : ∀ I ⊆ s, I.card ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
+    (h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
     (⋂ i ∈ s, F i).Nonempty := by
   classical
-  obtain h_card | h_card := lt_or_le s.card (finrank 𝕜 E + 1)
+  obtain h_card | h_card := lt_or_le #s (finrank 𝕜 E + 1)
   · exact helly_theorem_corner (le_of_lt h_card) h_inter
-  generalize hn : s.card = n
+  generalize hn : #s = n
   rw [hn] at h_card
   induction' n, h_card using Nat.le_induction with k h_card hk generalizing ι
   · exact helly_theorem_corner (le_of_eq hn) h_inter
@@ -137,9 +137,9 @@ theorem helly_theorem' {F : ι → Set E} {s : Finset ι}
 If `F` is a family of `n` convex sets in a vector space of finite dimension `d`, with `n ≥ d + 1`,
 and any `d + 1` sets of `F` intersect nontrivially, then all sets of `F` intersect nontrivially. -/
 theorem helly_theorem {F : ι → Set E} {s : Finset ι}
-    (h_card : finrank 𝕜 E + 1 ≤ s.card)
+    (h_card : finrank 𝕜 E + 1 ≤ #s)
     (h_convex : ∀ i ∈ s, Convex 𝕜 (F i))
-    (h_inter : ∀ I ⊆ s, I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
+    (h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
     (⋂ i ∈ s, F i).Nonempty := by
   apply helly_theorem' h_convex
   intro I hI_ss hI_card
@@ -153,7 +153,7 @@ If `F` is a finite set of convex sets in a vector space of finite dimension `d`,
 sets from `F` intersect nontrivially, then all sets from `F` intersect nontrivially. -/
 theorem helly_theorem_set' {F : Finset (Set E)}
     (h_convex : ∀ X ∈ F, Convex 𝕜 X)
-    (h_inter : ∀ G : Finset (Set E), G ⊆ F → G.card ≤ finrank 𝕜 E + 1 → (⋂₀ G : Set E).Nonempty) :
+    (h_inter : ∀ G : Finset (Set E), G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ G : Set E).Nonempty) :
     (⋂₀ (F : Set (Set E))).Nonempty := by
   classical -- for DecidableEq, required for the family version
   rw [show ⋂₀ F = ⋂ X ∈ F, (X : Set E) by ext; simp]
@@ -168,9 +168,9 @@ If `F` is a finite set of convex sets in a vector space of finite dimension `d`,
 and any `d + 1` sets from `F` intersect nontrivially,
 then all sets from `F` intersect nontrivially. -/
 theorem helly_theorem_set {F : Finset (Set E)}
-    (h_card : finrank 𝕜 E + 1 ≤ F.card)
+    (h_card : finrank 𝕜 E + 1 ≤ #F)
     (h_convex : ∀ X ∈ F, Convex 𝕜 X)
-    (h_inter : ∀ G : Finset (Set E), G ⊆ F → G.card = finrank 𝕜 E + 1 → (⋂₀ G : Set E).Nonempty) :
+    (h_inter : ∀ G : Finset (Set E), G ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ G : Set E).Nonempty) :
     (⋂₀ (F : Set (Set E))).Nonempty := by
   apply helly_theorem_set' h_convex
   intro I hI_ss hI_card
@@ -185,7 +185,7 @@ If `F` is a family of compact convex sets in a vector space of finite dimension
 `k ≤ d + 1` sets of `F` intersect nontrivially, then all sets of `F` intersect nontrivially. -/
 theorem helly_theorem_compact' [TopologicalSpace E] [T2Space E] {F : ι → Set E}
     (h_convex : ∀ i, Convex 𝕜 (F i)) (h_compact : ∀ i, IsCompact (F i))
-    (h_inter : ∀ I : Finset ι, I.card ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
+    (h_inter : ∀ I : Finset ι, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
     (⋂ i, F i).Nonempty := by
   classical
   /- If `ι` is empty the statement is trivial. -/
@@ -214,11 +214,11 @@ then all sets of `F` intersect nontrivially. -/
 theorem helly_theorem_compact [TopologicalSpace E] [T2Space E] {F : ι → Set E}
     (h_card : finrank 𝕜 E + 1 ≤ PartENat.card ι)
     (h_convex : ∀ i, Convex 𝕜 (F i)) (h_compact : ∀ i, IsCompact (F i))
-    (h_inter : ∀ I : Finset ι, I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
+    (h_inter : ∀ I : Finset ι, #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) :
     (⋂ i, F i).Nonempty := by
   apply helly_theorem_compact' h_convex h_compact
   intro I hI_card
-  have hJ : ∃ J : Finset ι, I ⊆ J ∧ J.card = finrank 𝕜 E + 1 := by
+  have hJ : ∃ J : Finset ι, I ⊆ J ∧ #J = finrank 𝕜 E + 1 := by
     by_cases h : Infinite ι
     · exact Infinite.exists_superset_card_eq _ _ hI_card
     · have : Finite ι := Finite.of_not_infinite h
@@ -236,7 +236,7 @@ If `F` is a set of compact convex sets in a vector space of finite dimension `d`
 `k ≤ d + 1` sets from `F` intersect nontrivially, then all sets from `F` intersect nontrivially. -/
 theorem helly_theorem_set_compact' [TopologicalSpace E] [T2Space E] {F : Set (Set E)}
     (h_convex : ∀ X ∈ F, Convex 𝕜 X) (h_compact : ∀ X ∈ F, IsCompact X)
-    (h_inter : ∀ G : Finset (Set E), (G : Set (Set E)) ⊆ F → G.card ≤ finrank 𝕜 E + 1 →
+    (h_inter : ∀ G : Finset (Set E), (G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 →
     (⋂₀ G : Set E).Nonempty) :
     (⋂₀ (F : Set (Set E))).Nonempty := by
   classical -- for DecidableEq, required for the family version
@@ -259,7 +259,7 @@ then all sets from `F` intersect nontrivially. -/
 theorem helly_theorem_set_compact [TopologicalSpace E] [T2Space E] {F : Set (Set E)}
     (h_card : finrank 𝕜 E + 1 ≤ F.encard)
     (h_convex : ∀ X ∈ F, Convex 𝕜 X) (h_compact : ∀ X ∈ F, IsCompact X)
-    (h_inter : ∀ G : Finset (Set E), (G : Set (Set E)) ⊆ F → G.card = finrank 𝕜 E + 1 →
+    (h_inter : ∀ G : Finset (Set E), (G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 →
     (⋂₀ G : Set E).Nonempty) :
     (⋂₀ (F : Set (Set E))).Nonempty := by
   apply helly_theorem_set_compact' h_convex h_compact