case nil
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
⊢ (sum []).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ []

case cons
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : (sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
⊢ (sum (hd :: tl)).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ (hd :: tl)
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
⊢ (sum l).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ l
induction' l with hd tl IH
no goals
case nil
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
⊢ (sum []).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ []
simp
case cons
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : (sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
⊢ (hd + sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ (hd :: tl)
case cons
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : (sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
⊢ (sum (hd :: tl)).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ (hd :: tl)
simp only [List.sum_cons, Finset.union_comm]
case cons
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : (sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
⊢ hd.support ⊆ hd.support
case cons
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : (sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
⊢ (hd + sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ (hd :: tl)
refine' Finsupp.support_add.trans (Finset.union_subset_union _ IH)
no goals
case cons
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : (sum tl).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
⊢ hd.support ⊆ hd.support
rfl