case nil
ι : Type u_2
M : Type u_1
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) ∅ []

case cons
ι : Type u_2
M : Type u_1
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)
ι : Type u_2
M : Type u_1
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
induction' l with hd tl IH
no goals
case nil
ι : Type u_2
M : Type u_1
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) ∅ []
simp
case cons
ι : Type u_2
M : Type u_1
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)
case cons
ι : Type u_2
M : Type u_1
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)
simp only [List.pairwise_cons] at hl
case cons
ι : Type u_2
M : Type u_1
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
case cons
ι : Type u_2
M : Type u_1
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)
simp only [List.sum_cons, List.foldr_cons, Function.comp_apply]
case cons
ι : Type u_2
M : Type u_1
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
case cons
ι : Type u_2
M : Type u_1
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
rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]
case cons
ι : Type u_2
M : Type u_1
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)
case cons
ι : Type u_2
M : Type u_1
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
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
no goals
ι : Type u_2
M : Type u_1
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
exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this
case cons
ι : Type u_2
M : Type u_1
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)
case cons
ι : Type u_2
M : Type u_1
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)
rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
  Finset.disjoint_sup_right]
case cons
ι : Type u_2
M : Type u_1
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)
case cons
ι : Type u_2
M : Type u_1
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)
intro f hf
case cons
ι : Type u_2
M : Type u_1
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)
case cons
ι : Type u_2
M : Type u_1
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)
simp only [List.mem_toFinset, List.mem_map] at hf
case cons.intro.intro
ι : Type u_2
M : Type u_1
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)
case cons
ι : Type u_2
M : Type u_1
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)
obtain ⟨f, hf, rfl⟩ := hf
no goals
case cons.intro.intro
ι : Type u_2
M : Type u_1
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)
exact hl.left _ hf