no goals
α : Type u_1
β : Type ?u.2365
s✝ t : Set α
a b x y : α
f : α → β
s : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s = Finset.card (Finite.toFinset hs)
rw [ncard_def, @Nat.card_eq_fintype_card _ hs.fintype, @Finite.card_toFinset _ _ hs.fintype hs]