refine' Finset.Subset.trans Finsupp.support_sum _
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (v.sum fun a => Finsupp.single (f a)).support ⊆ Finset.map f v.support
R : Type ?u.8691
ι : Type ?u.8694
inst✝¹ : CommSemiring R
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
⊢ (v.support.biUnion fun a => (Finsupp.single (f a) (v a)).support) ⊆ Finset.map f v.support