no goals
α : Type u_1
β : Type ?u.275665
γ : Type ?u.275668
ι : Type ?u.275671
M : Type u_3
M' : Type ?u.275677
N : Type u_4
P : Type u_2
G : Type ?u.275686
H : Type ?u.275689
R : Type ?u.275692
S : Type ?u.275695
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
D : DecidableEq α
f : M → N → P
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
⊢ (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support
rw [Subsingleton.elim D] <;> exact support_onFinset_subset