ι : Type u_2
M : Type u_1
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

case this
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ (Finset.sum s id).support = sup s Finsupp.support
suffices : s.1.Pairwise (_root_.Disjoint on Finsupp.support)
case h.e'_2.h.e'_4
ι : Type u_2
M : Type u_1
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
ι : Type u_2
M : Type u_1
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
convert Multiset.support_sum_eq s.1 this
no goals
case h.e'_2.h.e'_4
ι : Type u_2
M : Type u_1
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
exact (Finset.sum_val _).symm
case this.intro.intro
ι : Type u_2
M : Type u_1
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
case this
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val
obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup := by
  refine' ⟨s.toList, _, Finset.nodup_toList _⟩
  simp
case this.intro.intro
ι : Type u_2
M : Type u_1
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
case this.intro.intro
ι : Type u_2
M : Type u_1
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
subst hl
case this.intro.intro.hr
ι : Type u_2
M : Type u_1
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)
case this.intro.intro
ι : Type u_2
M : Type u_1
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
rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise, ←
  List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]
case this.intro.intro.hr
ι : Type u_2
M : Type u_1
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
case this.intro.intro.hr
ι : Type u_2
M : Type u_1
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)
intro x y hxy
no goals
case this.intro.intro.hr
ι : Type u_2
M : Type u_1
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
exact symmetric_disjoint hxy
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ List.toFinset (toList s) = s
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ ∃ l, List.toFinset l = s ∧ List.Nodup l
refine' ⟨s.toList, _, Finset.nodup_toList _⟩
no goals
ι : Type u_2
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Finset (ι →₀ M)
hs : Set.PairwiseDisjoint (↑s) Finsupp.support
⊢ List.toFinset (toList s) = s
simp