no goals
α : Type u_1
β : Type ?u.38587
γ : Type ?u.38590
s t : Finset α
a b : α
m : Multiset α
hm : Nodup m
⊢ Finset.Nonempty { val := m, nodup := hm } ↔ m ≠ 0
induction m using Multiset.induction_on <;> simp