no goals
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (Finset.sum s id).support ⊆ sup s Finsupp.support
classical convert Multiset.support_sum_subset s.1 ; simp
case h.e'_3.h.e'_4
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ Finset.sum s id = Multiset.sum s.val
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (Finset.sum s id).support ⊆ sup s Finsupp.support
convert Multiset.support_sum_subset s.1
no goals
case h.e'_3.h.e'_4
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ Finset.sum s id = Multiset.sum s.val
simp