no goals
α : Type u_1
β : Type ?u.135476
γ : Type ?u.135479
ι : Type ?u.135482
M : Type u_2
M' : Type ?u.135488
N : Type ?u.135491
P : Type ?u.135494
G : Type ?u.135497
H : Type ?u.135500
R : Type ?u.135503
S : Type ?u.135506
inst✝ : Zero M
a a' : α
b : M
f : α →₀ M
⊢ card f.support = 1 ↔ ∃ a b x, f = single a b
simp only [card_eq_one, support_eq_singleton']