no goals
α : Type u_1
β : Type ?u.137292
γ : Type ?u.137295
ι : Type ?u.137298
M : Type u_2
M' : Type ?u.137304
N : Type ?u.137307
P : Type ?u.137310
G : Type ?u.137313
H : Type ?u.137316
R : Type ?u.137319
S : Type ?u.137322
inst✝¹ : Zero M
a a' : α
b : M
inst✝ : Nonempty α
f : α →₀ M
⊢ card f.support ≤ 1 ↔ ∃ a, f = single a (↑f a)
simp only [card_le_one_iff_subset_singleton, support_subset_singleton]