no goals
α : Type u_1
β : Type ?u.16657
γ : Type ?u.16660
ι : Type ?u.16663
M : Type u_2
M' : Type ?u.16669
N : Type ?u.16672
P : Type ?u.16675
G : Type ?u.16678
H : Type ?u.16681
R : Type ?u.16684
S : Type ?u.16687
inst✝ : Zero M
f : α →₀ M
⊢ Finset.Nonempty f.support ↔ f ≠ 0
simp only [Finsupp.support_eq_empty, Finset.nonempty_iff_ne_empty, Ne.def]