no goals
α : Type u_1
β : Type ?u.175978
γ : Type ?u.175981
ι : Type ?u.175984
M : Type u_2
M' : Type ?u.175990
N : Type ?u.175993
P : Type ?u.175996
G : Type ?u.175999
H : Type ?u.176002
R : Type ?u.176005
S : Type ?u.176008
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
⊢ a ∈ (onFinset s f hf).support ↔ f a ≠ 0
rw [Finsupp.mem_support_iff, Finsupp.onFinset_apply]