-- Mathlib/Data/Finsupp/BigOperators.lean
theorem List.support_sum_eq [AddMonoid M] (l : List (ι →₀ M))
    (hl : l.Pairwise (_root_.Disjoint on Finsupp.support)) :
    l.sum.support = l.foldr (Finsupp.support · ⊔ ·) ∅

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
hl : Pairwise (_root_.Disjoint on Finsupp.support) l
⊢ l.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ l

Tactic:
induction' l with hd tl IH

Result:
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hl : Pairwise (_root_.Disjoint on Finsupp.support) []
⊢ [].sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ []

case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : Pairwise (_root_.Disjoint on Finsupp.support) (hd :: tl)
⊢ (hd :: tl).sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ (hd :: tl)

Proof state:
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hl : Pairwise (_root_.Disjoint on Finsupp.support) []
⊢ [].sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ []

Tactic:
simp

Result:
no goals

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support tl.sum.support

Tactic:
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

Result:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ 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)

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ 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 tl.sum.support

Tactic:
exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this

Result:
no goals

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ ∀ ⦃i : Finset ι⦄, i ∈ (map Finsupp.support tl).toFinset → _root_.Disjoint hd.support (id i)

Tactic:
intro f hf

Result:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
hf : f ∈ (map Finsupp.support tl).toFinset
⊢ _root_.Disjoint hd.support (id f)

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : Pairwise (_root_.Disjoint on Finsupp.support) (hd :: tl)
⊢ (hd :: tl).sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
simp only [List.pairwise_cons] at hl

Result:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ (hd :: tl).sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ (hd :: tl)

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
f : Finset ι
hf : ∃ a ∈ tl, a.support = f
⊢ _root_.Disjoint hd.support (id f)

Tactic:
obtain ⟨f, hf, rfl⟩ := hf

Result:
case cons.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ 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)

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ (hd :: tl).sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
simp only [List.sum_cons, List.foldr_cons, Function.comp_apply]

Result:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ (hd + tl.sum).support = hd.support ⊔ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ (hd + tl.sum).support = hd.support ⊔ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl

Tactic:
rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]

Result:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support tl.sum.support

Proof state:
case cons.intro.intro
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
hl : (∀ 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)

Tactic:
exact hl.left _ hf

Result:
no goals