no goals
α : Type u_1
β : Type ?u.137863
γ : Type ?u.137866
ι : Type ?u.137869
M : Type u_2
M' : Type ?u.137875
N : Type ?u.137878
P : Type ?u.137881
G : Type ?u.137884
H : Type ?u.137887
R : Type ?u.137890
S : Type ?u.137893
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Nonempty α
f : α →₀ M
⊢ card f.support ≤ 1 ↔ ∃ a b, f = single a b
simp only [card_le_one_iff_subset_singleton, support_subset_singleton']