no goals
α : Type u_1
β : Type ?u.17001
γ : Type ?u.17004
ι : Type ?u.17007
M : Type u_2
M' : Type ?u.17013
N : Type ?u.17016
P : Type ?u.17019
G : Type ?u.17022
H : Type ?u.17025
R : Type ?u.17028
S : Type ?u.17031
inst✝ : Zero M
f : α →₀ M
⊢ f ≠ 0 ↔ ∃ a, ↑f a ≠ 0
simp [← Finsupp.support_eq_empty, Finset.eq_empty_iff_forall_not_mem]