awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
t : β
h : ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M) → ∃ a ∈ x.support, f a = t
h₁ :
  (∃ a ∈ x.support, f a = t) →
    ∀ (i : α) (i_in : i ∈ x.support) (hi : f i = t),
      ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M)
⊢ ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M) ↔ ∃ a ∈ x.support, f a = t

Tactic:
refine ⟨?_, fun ⟨i, i_in, hi⟩ ↦ ?_⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
t : β
⊢ ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M) → ∃ a ∈ x.support, f a = t

Tactic:
simpa [mapDomain, sum, single_apply] using fun i h h' _ ↦ ⟨i, h, h'⟩

Premises used: Finsupp.mapDomain, Finsupp.sum, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
t : β
h : ∃ a ∈ x.support, f a = t
i : α
i_in : i ∈ x.support
hi : f i = t
⊢ ¬Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) (0 : M) ∧
    f i = f i ∧ ¬Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) (0 : M)

Tactic:
simp [mem_support_iff.mp i_in]

Premises used: Finsupp.mem_support_iff, Iff.mp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
t : β
h : ∃ a ∈ x.support, f a = t
i : α
i_in : i ∈ x.support
hi : f i = t
⊢ ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M)

Tactic:
simpa [mapDomain, sum, ← hi, single_apply] using ⟨i, by simp [mem_support_iff.mp i_in]⟩

Premises used: Finsupp.mapDomain, Finsupp.sum, Finsupp.single_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
x : α →₀ M
a : α
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M)
    (∑ i ∈ x.support with f i = f a, (x : (a : α) → M) i : M)

Tactic:
simp [mapDomain, sum, single_apply, Finset.sum_ite]

Premises used: Finsupp.mapDomain, Finsupp.sum, Finsupp.single_apply, Finset.sum_ite
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
h : x = 0
rw : Eq (α := β →₀ M) (mapDomain f 0) 0
rw₁ rw₂ : Eq (α := β →₀ M) 0 0
⊢ mapDomain f x = 0

Tactic:
rw [h, mapDomain_zero]

Premises used: Finsupp.mapDomain_zero
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
refine : ∀ (h : mapDomain f x = 0) (i : α), Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
⊢ mapDomain f x = 0 ↔ x = 0

Tactic:
refine ⟨fun h ↦ Finsupp.ext (fun i ↦ ?_), fun h ↦ by rw [h, mapDomain_zero]⟩
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
h : mapDomain f x = 0
i : α
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f i) : M) ((0 : (a : β) → M) (f i) : M)

Tactic:
replace h := Finsupp.ext_iff.mp h (f i)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
i : α
h : Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f i) : M) ((0 : (a : β) → M) (f i) : M)
⊢ ∀ (i_1 : α),
    ¬Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i_1 : M) (0 : M) →
      f i_1 = f i → Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i_1 : M) (0 : M)

Tactic:
simp [mapDomain_apply_eq_sum] at h

Premises used: Finsupp.mapDomain_apply_eq_sum
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
i : α
h :
  ∀ (i_1 : α),
    ¬Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i_1 : M) (0 : M) →
      f i_1 = f i → Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i_1 : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
refine : ∀ (h : mapDomain f x = 0) (i : α), Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
refine₁ :
  ∀ (i : α) (h : Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f i) : M) ((0 : (a : β) → M) (f i) : M)),
    Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
refine₂ refine₃ :
  ∀ (i : α)
    (h :
      ∀ (i_1 : α),
        ¬Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i_1 : M) (0 : M) →
          f i_1 = f i → Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i_1 : M) (0 : M)),
    Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
⊢ mapDomain f x = 0 ↔ x = 0

Tactic:
classical
  refine ⟨fun h ↦ Finsupp.ext (fun i ↦ ?_), fun h ↦ by rw [h, mapDomain_zero]⟩
  replace h := Finsupp.ext_iff.mp h (f i)
  simp [mapDomain_apply_eq_sum] at h; grind

Premises used: Finsupp.mapDomain_apply_eq_sum
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
⊢ Subset.{u_1} (α := Finset ι) (Finsupp.support.{u_1, u_2} (M := M) (sum []))
    (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ [])

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
cons : (hd + tl.sum).support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)
⊢ (hd :: tl).sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
simp only [List.sum_cons]

Premises used: List.sum_cons
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
⊢ (hd + tl.sum).support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
Finsupp.support_add.trans (Finset.union_subset_union Finset.Subset.rfl IH)

Premises used: Finset.Subset.rfl, Finset.union_subset_union, HasSubset.Subset.trans, Finsupp.support_add
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
⊢ (hd + tl.sum).support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
exact Finsupp.support_add.trans (Finset.union_subset_union Finset.Subset.rfl IH)

Premises used: Finset.Subset.rfl, Finset.union_subset_union, HasSubset.Subset.trans, Finsupp.support_add
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
l : List (ι →₀ M)
nil :
  Subset.{u_1} (α := Finset ι) (Finsupp.support.{u_1, u_2} (M := M) (sum []))
    (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ [])
cons :
  ∀ (hd : ι →₀ M) (tl : List (ι →₀ M))
    (IH : tl.sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl),
    (hd :: tl).sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)
⊢ l.sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ l

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH =>
    simp only [List.sum_cons]
    exact Finsupp.support_add.trans (Finset.union_subset_union Finset.Subset.rfl IH)

Premises used: List.cons, List.sum_cons, List.nil
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Multiset (ι →₀ M)
h :
  ∀ (a : List (ι →₀ M)),
    (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).support ⊆
      (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).sup
⊢ s.sum.support ⊆ (map Finsupp.support s).sup

Tactic:
induction s using Quot.inductionOn
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a : List (ι →₀ M)
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).support ⊆
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).sup

Tactic:
simpa only [Multiset.quot_mk_to_coe'', Multiset.sum_coe, Multiset.map_coe, Multiset.sup_coe,
    List.foldr_map] using List.support_sum_subset _

Premises used: Multiset.sup_coe, Multiset.sum_coe, List.support_sum_subset, List.foldr_map, Multiset.map_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ s.val.sum.support ⊆ (Multiset.map Finsupp.support s.val).sup

Tactic:
Multiset.support_sum_subset s.1

Premises used: Multiset.support_sum_subset, Finset.val
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
h : s.sum id = s.val.sum
⊢ (s.sum id).support ⊆ s.sup Finsupp.support

Tactic:
convert! Multiset.support_sum_subset s.1

Premises used: Multiset.support_sum_subset, Finset.val
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ s.sum id = s.val.sum

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
h h₁ : s.sum id = s.val.sum
⊢ (s.sum id).support ⊆ s.sup Finsupp.support

Tactic:
classical convert! Multiset.support_sum_subset s.1; simp

Premises used: Multiset.support_sum_subset, Finset.val
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : Zero M
l : List (ι →₀ M)
x : ι
simp :
  Membership.mem (γ := Finset ι) (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ∪ x2) ∅ l) x ↔
    ∃ f ∈ l, Ne.{u_2 + 1} (α := M) ((f : (a : ι) → M) x : M) (0 : M)
⊢ Membership.mem (γ := Finset ι) (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ l) x ↔
    ∃ f ∈ l, x ∈ f.support

Tactic:
simp only [Finset.sup_eq_union, Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff, Finset.sup_eq_union
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : Zero M
x : ι
⊢ Membership.mem (γ := Finset ι) (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ∪ x2) ∅ []) x ↔
    ∃ (f : ι →₀ M), Membership.mem (γ := List (ι →₀ M)) [] f ∧ Ne.{u_2 + 1} (α := M) ((f : (a : ι) → M) x : M) (0 : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : Zero M
x : ι
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  Membership.mem (γ := Finset ι) (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ∪ x2) ∅ tl) x ↔
    ∃ f ∈ tl, Ne.{u_2 + 1} (α := M) ((f : (a : ι) → M) x : M) (0 : M)
⊢ Membership.mem (γ := Finset ι) (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ∪ x2) ∅ (hd :: tl)) x ↔
    ∃ f ∈ hd :: tl, Ne.{u_2 + 1} (α := M) ((f : (a : ι) → M) x : M) (0 : M)

Tactic:
simp only [foldr, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH,
      mem_cons, exists_eq_or_imp]

Premises used: Finsupp.mem_support_iff, ne_eq, exists_eq_or_imp, Finset.mem_union, List.mem_cons, List.foldr
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : Zero M
l : List (ι →₀ M)
x : ι
nil :
  Membership.mem (γ := Finset ι) (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ∪ x2) ∅ []) x ↔
    ∃ (f : ι →₀ M), Membership.mem (γ := List (ι →₀ M)) [] f ∧ Ne.{u_2 + 1} (α := M) ((f : (a : ι) → M) x : M) (0 : M)
cons :
  ∀ (hd : ι →₀ M) (tl : List (ι →₀ M))
    (IH :
      Membership.mem (γ := Finset ι) (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ∪ x2) ∅ tl) x ↔
        ∃ f ∈ tl, Ne.{u_2 + 1} (α := M) ((f : (a : ι) → M) x : M) (0 : M)),
    Membership.mem (γ := Finset ι) (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ∪ x2) ∅ (hd :: tl)) x ↔
      ∃ f ∈ hd :: tl, Ne.{u_2 + 1} (α := M) ((f : (a : ι) → M) x : M) (0 : M)
⊢ Membership.mem (γ := Finset ι) (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ∪ x2) ∅ l) x ↔
    ∃ f ∈ l, Ne.{u_2 + 1} (α := M) ((f : (a : ι) → M) x : M) (0 : M)

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH =>
    simp only [foldr, Finset.mem_union, Finsupp.mem_support_iff, ne_eq, IH,
      mem_cons, exists_eq_or_imp]

Premises used: Finsupp.mem_support_iff, ne_eq, List.cons, exists_eq_or_imp, Finset.mem_union, List.mem_cons, List.foldr, List.nil
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : Zero M
s : Multiset (ι →₀ M)
x : ι
x_1 : List (ι →₀ M)
⊢ x ∈ (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) x_1)).sup ↔
    ∃ (f : ι →₀ M),
      Membership.mem (γ := Multiset (ι →₀ M))
          (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) x_1) f ∧
        x ∈ f.support

Tactic:
simpa only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sup_coe, List.foldr_map]
    using List.mem_foldr_sup_support_iff

Premises used: Multiset.sup_coe, List.mem_foldr_sup_support_iff, List.foldr_map, Multiset.map_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : Zero M
s : Finset (ι →₀ M)
x : ι
⊢ x ∈ s.sup Finsupp.support ↔ ∃ f ∈ s, x ∈ f.support

Tactic:
Multiset.mem_sup_map_support_iff

Premises used: Set.Mem, setOf, Multiset.mem_sup_map_support_iff, Multiset.Mem
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hl : Pairwise (α := ι →₀ M) (_root_.Disjoint on Finsupp.support) []
⊢ Eq.{u_1 + 1} (α := Finset ι) (Finsupp.support.{u_1, u_2} (M := M) (sum []))
    (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ [])

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
hl : Pairwise (_root_.Disjoint on Finsupp.support) (hd :: tl)
⊢ (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl

Tactic:
simp only [List.pairwise_cons] at hl

Premises used: List.pairwise_cons
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
cons : (hd + tl.sum).support = hd.support ⊔ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
⊢ (hd :: tl).sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)

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

Premises used: List.foldr_cons, List.sum_cons
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
cons : _root_.Disjoint hd.support tl.sum.support
⊢ (hd + tl.sum).support = hd.support ⊔ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl

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

Premises used: Finsupp.support_add_eq, And.right, Finset.sup_eq_union
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ 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 : ι →₀ M) (y : Finset ι) ↦ x.support ⊔ y) ∅ tl)
⊢ _root_.Disjoint hd.support tl.sum.support

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

Premises used: List.support_sum_subset, Finset.disjoint_of_subset_right
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ 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 : ι →₀ M) (y : Finset ι) ↦ x.support ⊔ y) ∅ tl)
⊢ _root_.Disjoint hd.support tl.sum.support

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

Premises used: List.support_sum_subset, Finset.disjoint_of_subset_right
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
cons : _root_.Disjoint hd.support (foldr (fun (x : ι →₀ M) (y : Finset ι) ↦ x.support ⊔ y) ∅ 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
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
cons : ∀ ⦃i : Finset ι⦄, i ∈ (map Finsupp.support tl).toFinset → _root_.Disjoint hd.support (id i)
⊢ _root_.Disjoint hd.support (foldr (fun (x : ι →₀ M) (y : Finset ι) ↦ x.support ⊔ y) ∅ tl)

Tactic:
rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
      Finset.disjoint_sup_right]

Premises used: Finset.bot_eq_empty, Finset.disjoint_sup_right, List.foldr_sup_eq_sup_toFinset, List.foldr_map
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ 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
⊢ ∃ a ∈ tl, a.support = f

Tactic:
simp only [List.mem_toFinset, List.mem_map] at hf

Premises used: List.mem_toFinset, List.mem_map
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ 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
cons : ∀ (f : ι →₀ M) (hf : f ∈ tl), _root_.Disjoint hd.support (id f.support)
⊢ _root_.Disjoint hd.support (id f)

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

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ 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:
hl.left _ hf

Premises used: And.left
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH :
  ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
    tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ 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

Premises used: And.left
-- Module: Mathlib.Data.Finsupp.BigOperators
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
l : List (ι →₀ M)
hl : Pairwise (_root_.Disjoint on Finsupp.support) l
nil :
  ∀ (hl : Pairwise (α := ι →₀ M) (_root_.Disjoint on Finsupp.support) []),
    Eq.{u_1 + 1} (α := Finset ι) (Finsupp.support.{u_1, u_2} (M := M) (sum []))
      (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ [])
cons :
  ∀ (hd : ι →₀ M) (tl : List (ι →₀ M))
    (IH :
      ∀ (hl : Pairwise (_root_.Disjoint on Finsupp.support) tl),
        tl.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl)
    (hl : Pairwise (_root_.Disjoint on Finsupp.support) (hd :: tl)),
    (hd :: tl).sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)
⊢ l.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ l

Tactic:
induction l with
  | nil => simp
  | cons hd tl IH =>
    simp only [List.pairwise_cons] at hl
    simp only [List.sum_cons, List.foldr_cons]
    rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]
    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
    rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
      Finset.disjoint_sup_right]
    intro f hf
    simp only [List.mem_toFinset, List.mem_map] at hf
    obtain ⟨f, hf, rfl⟩ := hf
    exact hl.left _ hf

Premises used: List.mem_toFinset, Finset.bot_eq_empty, List.foldr_cons, Finsupp.support_add_eq, List.cons, List.pairwise_cons, Finset.disjoint_sup_right, List.sum_cons, List.foldr_sup_eq_sup_toFinset, List.foldr_map, Finset.sup_eq_union, List.mem_map, rfl, List.nil