no goals
α : Type u_1
β : Type ?u.6628
s t : Set α
a b x y : α
f : α → β
hs : autoParam (Set.Finite s) _auto✝
⊢ 0 < ncard s ↔ Set.Nonempty s
rw [pos_iff_ne_zero, Ne.def, ncard_eq_zero hs, nonempty_iff_ne_empty]