case h
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a✝ : List (ι →₀ M)
⊢ (sum (Quot.mk Setoid.r a✝)).support ⊆ sup (map Finsupp.support (Quot.mk Setoid.r a✝))
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
⊢ (sum s).support ⊆ sup (map Finsupp.support s)
induction s using Quot.inductionOn
no goals
case h
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a✝ : List (ι →₀ M)
⊢ (sum (Quot.mk Setoid.r a✝)).support ⊆ sup (map Finsupp.support (Quot.mk Setoid.r a✝))
simpa only [Multiset.quot_mk_to_coe'', Multiset.coe_sum, Multiset.coe_map, Multiset.sup_coe,
  List.foldr_map] using List.support_sum_subset _