classical
rw [Finsupp.mapDomain]
refine' Finset.Subset.trans Finsupp.support_sum _
simp only [Finsupp.mem_support_iff, Finset.biUnion_subset_iff_forall_subset, Ne]
intro x hx
apply Finset.Subset.trans Finsupp.support_single_subset
simp [hx]
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
⊢ (Finsupp.mapDomain (⇑f) v).support ⊆ Finset.map f v.support
no goals