no goals
α : Type u_1
β : Type ?u.136560
γ : Type ?u.136563
ι : Type ?u.136566
M : Type u_2
M' : Type ?u.136572
N : Type ?u.136575
P : Type ?u.136578
G : Type ?u.136581
H : Type ?u.136584
R : Type ?u.136587
S : Type ?u.136590
inst✝ : Zero M
a✝ a' : α
b✝ : M
f : α →₀ M
a : α
x✝ : ∃ b, f = single a b
b : M
hb : f = single a b
⊢ f.support ⊆ {a}
rw [hb, support_subset_singleton, single_eq_same]