rw [← Fintype.card_subtype]
α : Type u_1
inst : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ Nat.card { x // p x } = (Finset.filter p Finset.univ).card
α : Type u_1
inst : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ Nat.card { x // p x } = Fintype.card { x // p x }