no goals
α : Type u_1
β : Type ?u.3963
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s = 0 ↔ s = ∅
rw [ncard_def, @Finite.card_eq_zero_iff _ hs.to_subtype, isEmpty_subtype,
  eq_empty_iff_forall_not_mem]