[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
⊢ (sum l).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ l
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
⊢ (sum []).support ⊆ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
M : Type u_2
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)
[PROOFSTEP]
simp only [List.sum_cons, Finset.union_comm]
[GOAL]
case cons
ι : Type u_1
M : Type u_2
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)
[PROOFSTEP]
refine' Finsupp.support_add.trans (Finset.union_subset_union _ IH)
[GOAL]
case cons
ι : Type u_1
M : Type u_2
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
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
⊢ (sum s).support ⊆ sup (map Finsupp.support s)
[PROOFSTEP]
induction s using Quot.inductionOn
[GOAL]
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a✝ : List (ι →₀ M)
⊢ (sum (Quot.mk Setoid.r a✝)).support ⊆ sup (map Finsupp.support (Quot.mk Setoid.r a✝))
[PROOFSTEP]
simpa only [Multiset.quot_mk_to_coe'', Multiset.coe_sum, Multiset.coe_map, Multiset.sup_coe, List.foldr_map] using
  List.support_sum_subset _
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (Finset.sum s id).support ⊆ sup s Finsupp.support
[PROOFSTEP]
classical convert Multiset.support_sum_subset s.1; simp
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (Finset.sum s id).support ⊆ sup s Finsupp.support
[PROOFSTEP]
convert Multiset.support_sum_subset s.1
[GOAL]
case h.e'_3.h.e'_4
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ Finset.sum s id = Multiset.sum s.val
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ l ↔ ∃ f x_1, x ∈ f.support
[PROOFSTEP]
simp only [Finset.sup_eq_union, List.foldr_map, Finsupp.mem_support_iff, exists_prop]
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
l : List (ι →₀ M)
x : ι
⊢ x ∈ foldr ((fun x x_1 => x ∪ x_1) ∘ Finsupp.support) ∅ l ↔ ∃ f, f ∈ l ∧ ↑f x ≠ 0
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
⊢ x ∈ foldr ((fun x x_1 => x ∪ x_1) ∘ Finsupp.support) ∅ [] ↔ ∃ f, f ∈ [] ∧ ↑f x ≠ 0
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
hd : ι →₀ M
tl : List (ι →₀ M)
IH : x ∈ foldr ((fun x x_1 => x ∪ x_1) ∘ Finsupp.support) ∅ tl ↔ ∃ f, f ∈ tl ∧ ↑f x ≠ 0
⊢ x ∈ foldr ((fun x x_1 => x ∪ x_1) ∘ Finsupp.support) ∅ (hd :: tl) ↔ ∃ f, f ∈ hd :: tl ∧ ↑f x ≠ 0
[PROOFSTEP]
simp only [foldr, Function.comp_apply, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH, find?, mem_cons,
  exists_eq_or_imp]
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
s : Multiset (ι →₀ M)
x : ι
x✝ : List (ι →₀ M)
⊢ x ∈ sup (map Finsupp.support (Quot.mk Setoid.r x✝)) ↔ ∃ f x_1, x ∈ f.support
[PROOFSTEP]
simpa only [Multiset.quot_mk_to_coe'', Multiset.coe_map, Multiset.sup_coe, List.foldr_map] using
  List.mem_foldr_sup_support_iff
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl : Pairwise (_root_.Disjoint on Finsupp.support) l
⊢ (sum l).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ l
[PROOFSTEP]
induction' l with hd tl IH
[GOAL]
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hl : Pairwise (_root_.Disjoint on Finsupp.support) []
⊢ (sum []).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ []
[PROOFSTEP]
simp
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl : Pairwise (_root_.Disjoint on Finsupp.support) (hd :: tl)
⊢ (sum (hd :: tl)).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ (hd :: tl)
[PROOFSTEP]
simp only [List.pairwise_cons] at hl 
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ (sum (hd :: tl)).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ (hd :: tl)
[PROOFSTEP]
simp only [List.sum_cons, List.foldr_cons, Function.comp_apply]
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ (hd + sum tl).support = hd.support ⊔ foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
[PROOFSTEP]
rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support (sum tl).support
[PROOFSTEP]
suffices _root_.Disjoint hd.support (tl.foldr (fun x y ↦ (Finsupp.support x ⊔ y)) ∅) by
  exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
this : _root_.Disjoint hd.support (foldr (fun x y => x.support ⊔ y) ∅ tl)
⊢ _root_.Disjoint hd.support (sum tl).support
[PROOFSTEP]
exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support (foldr (fun x y => x.support ⊔ y) ∅ tl)
[PROOFSTEP]
rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset, Finset.disjoint_sup_right]
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ ∀ ⦃i : Finset ι⦄, i ∈ toFinset (map (fun x => x.support) tl) → _root_.Disjoint hd.support (id i)
[PROOFSTEP]
intro f hf
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
hf : f ∈ toFinset (map (fun x => x.support) tl)
⊢ _root_.Disjoint hd.support (id f)
[PROOFSTEP]
simp only [List.mem_toFinset, List.mem_map] at hf 
[GOAL]
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
hf : ∃ a, a ∈ tl ∧ a.support = f
⊢ _root_.Disjoint hd.support (id f)
[PROOFSTEP]
obtain ⟨f, hf, rfl⟩ := hf
[GOAL]
case cons.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl✝ : Pairwise (_root_.Disjoint on Finsupp.support) l
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Pairwise (_root_.Disjoint on Finsupp.support) tl →
    (sum tl).support = foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ tl
hl :
  (∀ (a' : ι →₀ M), a' ∈ tl → (_root_.Disjoint on Finsupp.support) hd a') ∧
    Pairwise (_root_.Disjoint on Finsupp.support) tl
f : ι →₀ M
hf : f ∈ tl
⊢ _root_.Disjoint hd.support (id f.support)
[PROOFSTEP]
exact hl.left _ hf
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
⊢ (sum s).support = sup (map Finsupp.support s)
[PROOFSTEP]
induction' s using Quot.inductionOn with a
[GOAL]
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs✝ : Pairwise (_root_.Disjoint on Finsupp.support) s
a : List (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) (Quot.mk Setoid.r a)
⊢ (sum (Quot.mk Setoid.r a)).support = sup (map Finsupp.support (Quot.mk Setoid.r a))
[PROOFSTEP]
obtain ⟨l, hl, hd⟩ := hs
[GOAL]
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
⊢ (sum (Quot.mk Setoid.r a)).support = sup (map Finsupp.support (Quot.mk Setoid.r a))
[PROOFSTEP]
suffices : a.Pairwise (_root_.Disjoint on Finsupp.support)
[GOAL]
case h.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
this : List.Pairwise (_root_.Disjoint on Finsupp.support) a
⊢ (sum (Quot.mk Setoid.r a)).support = sup (map Finsupp.support (Quot.mk Setoid.r a))
[PROOFSTEP]
convert List.support_sum_eq a this
[GOAL]
case h.e'_2.h.e'_4
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
this : List.Pairwise (_root_.Disjoint on Finsupp.support) a
⊢ sum (Quot.mk Setoid.r a) = List.sum a
[PROOFSTEP]
simp only [Multiset.quot_mk_to_coe'', Multiset.coe_sum]
[GOAL]
case h.e'_3
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
this : List.Pairwise (_root_.Disjoint on Finsupp.support) a
⊢ sup (map Finsupp.support (Quot.mk Setoid.r a)) = List.foldr ((fun x x_1 => x ⊔ x_1) ∘ Finsupp.support) ∅ a
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case h.e'_3
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
this : List.Pairwise (_root_.Disjoint on Finsupp.support) a
⊢ sup (map Finsupp.support (Quot.mk Setoid.r a)) = List.foldr (fun x x_1 => x.support ⊔ x_1) ∅ a
[PROOFSTEP]
simp only [quot_mk_to_coe'', coe_map, sup_coe, ge_iff_le, Finset.le_eq_subset, Finset.sup_eq_union, Finset.bot_eq_empty,
  List.foldr_map]
[GOAL]
case this
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hl : Quot.mk Setoid.r a = ↑l
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
⊢ List.Pairwise (_root_.Disjoint on Finsupp.support) a
[PROOFSTEP]
simp only [Multiset.quot_mk_to_coe'', Multiset.coe_map, Multiset.coe_eq_coe] at hl 
[GOAL]
case this
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (_root_.Disjoint on Finsupp.support) s
a l : List (ι →₀ M)
hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l
hl : a ~ l
⊢ List.Pairwise (_root_.Disjoint on Finsupp.support) a
[PROOFSTEP]
exact hl.symm.pairwise hd fun _ _ h ↦ _root_.Disjoint.symm h
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ (Finset.sum s id).support = sup s Finsupp.support
[PROOFSTEP]
classical
suffices : s.1.Pairwise (_root_.Disjoint on Finsupp.support)
· convert Multiset.support_sum_eq s.1 this
  · exact (Finset.sum_val _).symm
· obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup :=
    by
    refine' ⟨s.toList, _, Finset.nodup_toList _⟩
    simp
  subst hl
  rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise, ←
    List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]
  intro x y hxy
  exact symmetric_disjoint hxy
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ (Finset.sum s id).support = sup s Finsupp.support
[PROOFSTEP]
suffices : s.1.Pairwise (_root_.Disjoint on Finsupp.support)
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ (Finset.sum s id).support = sup s Finsupp.support
[PROOFSTEP]
convert Multiset.support_sum_eq s.1 this
[GOAL]
case h.e'_2.h.e'_4
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ Finset.sum s id = Multiset.sum s.val
[PROOFSTEP]
exact (Finset.sum_val _).symm
[GOAL]
case this
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val
[PROOFSTEP]
obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup :=
  by
  refine' ⟨s.toList, _, Finset.nodup_toList _⟩
  simp
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ ∃ l, List.toFinset l = s ∧ List.Nodup l
[PROOFSTEP]
refine' ⟨s.toList, _, Finset.nodup_toList _⟩
[GOAL]
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ List.toFinset (toList s) = s
[PROOFSTEP]
simp
[GOAL]
case this.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
l : List (ι →₀ M)
hl : List.toFinset l = s
hn : List.Nodup l
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val
[PROOFSTEP]
subst hl
[GOAL]
case this.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : List.Nodup l
hs : Set.PairwiseDisjoint (↑(List.toFinset l)) Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) (List.toFinset l).val
[PROOFSTEP]
rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise, ←
  List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]
[GOAL]
case this.intro.intro.hr
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : List.Nodup l
hs : Set.PairwiseDisjoint (↑(List.toFinset l)) Finsupp.support
⊢ Symmetric (Disjoint on Finsupp.support)
[PROOFSTEP]
intro x y hxy
[GOAL]
case this.intro.intro.hr
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : List.Nodup l
hs : Set.PairwiseDisjoint (↑(List.toFinset l)) Finsupp.support
x y : ι →₀ M
hxy : (Disjoint on Finsupp.support) x y
⊢ (Disjoint on Finsupp.support) y x
[PROOFSTEP]
exact symmetric_disjoint hxy
