awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
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) ∅ [])
⊢ l.sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ l
have 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)
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)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Multiset (ι →₀ M)
⊢ s.sum.support ⊆ (map Finsupp.support s).sup
have 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
Tactic: induction s using Quot.inductionOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (s.sum id).support ⊆ s.sup Finsupp.support
have h : s.sum id = s.val.sum
Tactic: convert! Multiset.support_sum_subset s.1
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
⊢ (s.sum id).support ⊆ s.sup Finsupp.support
have h : s.sum id = s.val.sum
Tactic: classical convert! Multiset.support_sum_subset s.1; simp
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : Zero M
l : List (ι →₀ M)
x : ι
⊢ Membership.mem (γ := Finset ι) (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ l) x ↔
    ∃ f ∈ l, x ∈ f.support
have 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)
Tactic: simp only [Finset.sup_eq_union, Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : Zero M
l : List (ι →₀ M)
x : ι
⊢ 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)
have 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)
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
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)
⊢ 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)
have 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)
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (hypothesis)
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)
⊢ (hd :: tl).sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)
have hl₁ : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
Tactic: simp only [List.pairwise_cons] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
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
⊢ (hd :: tl).sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)
have cons : (hd + tl.sum).support = hd.support ⊔ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
Tactic: simp only [List.sum_cons, List.foldr_cons]
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
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
⊢ (hd + tl.sum).support = hd.support ⊔ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
have cons : _root_.Disjoint hd.support tl.sum.support
Tactic: rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
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
⊢ _root_.Disjoint hd.support tl.sum.support
have cons : _root_.Disjoint hd.support (foldr (fun (x : ι →₀ M) (y : Finset ι) ↦ x.support ⊔ y) ∅ tl)
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
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
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
⊢ _root_.Disjoint hd.support (foldr (fun (x : ι →₀ M) (y : Finset ι) ↦ x.support ⊔ y) ∅ tl)
have cons : ∀ ⦃i : Finset ι⦄, i ∈ (map Finsupp.support tl).toFinset → _root_.Disjoint hd.support (id i)
Tactic: rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
      Finset.disjoint_sup_right]
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (hypothesis)
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
⊢ _root_.Disjoint hd.support (id f)
have hf₁ : ∃ a ∈ tl, a.support = f
Tactic: simp only [List.mem_toFinset, List.mem_map] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
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
⊢ _root_.Disjoint hd.support (id f)
have cons : ∀ (f : ι →₀ M) (hf : f ∈ tl), _root_.Disjoint hd.support (id f.support)
Tactic: obtain ⟨f, hf, rfl⟩ := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
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
⊢ l.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ l
have 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) ∅ [])
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
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
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) ∅ [])
⊢ l.sum.support = foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ l
have 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)
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
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Multiset (ι →₀ M)
hs : Pairwise (Disjoint on Finsupp.support) s
⊢ s.sum.support = (map Finsupp.support s).sup
have h : ∀ (a : List (ι →₀ M))
  (hs :
    Pairwise (Disjoint on Finsupp.support)
      (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)),
  (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: induction s using Quot.inductionOn with | _ a
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a : List (ι →₀ M)
hs :
  Pairwise (Disjoint on Finsupp.support) (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)
⊢ (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
have h : ∀ (l : List (ι →₀ M))
  (hl : Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a = (↑l : Multiset (ι →₀ M)))
  (hd : List.Pairwise (Disjoint on Finsupp.support) l),
  (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: obtain ⟨l, hl, hd⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a = (↑l : Multiset (ι →₀ M))
hd : List.Pairwise (Disjoint on Finsupp.support) l
this : List.Pairwise (Disjoint on Finsupp.support) a
⊢ (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
have h : (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a)).sup =
  List.foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ a
Tactic: convert! List.support_sum_eq a this
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a = (↑l : Multiset (ι →₀ M))
hd : List.Pairwise (Disjoint on Finsupp.support) l
⊢ (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
have h : List.Pairwise (Disjoint on Finsupp.support) a
Tactic: suffices a.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! List.support_sum_eq a this
    dsimp only [Function.comp_def]
    simp only [quot_mk_to_coe'', map_coe, sup_coe,
      Finset.sup_eq_union, Finset.bot_eq_empty, List.foldr_map]
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (hypothesis)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
a l : List (ι →₀ M)
hl : Quot.mk (⇑(List.isSetoid (ι →₀ M)) : List (ι →₀ M) → List (ι →₀ M) → Prop) a = (↑l : Multiset (ι →₀ M))
hd : List.Pairwise (Disjoint on Finsupp.support) l
⊢ List.Pairwise (Disjoint on Finsupp.support) a
have hl₁ : a.Perm l
Tactic: simp only [Multiset.quot_mk_to_coe'', Multiset.coe_eq_coe] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
this : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ (s.sum id).support = s.sup Finsupp.support
have h : s.sum id = s.val.sum
Tactic: convert! Multiset.support_sum_eq s.1 this
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
⊢ (s.sum id).support = s.sup Finsupp.support
have suffices : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
Tactic: suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    convert! Multiset.support_sum_eq s.1 this
    exact (Finset.sum_val _).symm
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
⊢ ∃ (l : List (ι →₀ M)), l.toFinset = s ∧ l.Nodup
have refine : s.toList.toFinset = s
Tactic: refine ⟨s.toList, ?_, Finset.nodup_toList _⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val
have obtain : ∀ (l : List (ι →₀ M)) (hl : l.toFinset = s) (hn : l.Nodup), Multiset.Pairwise (Disjoint on Finsupp.support) s.val
Tactic: obtain ⟨l, hl, hn⟩ : ∃ l : List (ι →₀ M), l.toFinset = s ∧ l.Nodup := by
    refine ⟨s.toList, ?_, Finset.nodup_toList _⟩
    simp
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
l : List (ι →₀ M)
hl : l.toFinset = s
hn : l.Nodup
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) s.val
have subst : ∀ (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support),
  Multiset.Pairwise (Disjoint on Finsupp.support) l.toFinset.val
Tactic: subst hl
Cleared hypotheses: s, hs, hl
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) l.toFinset.val
have hr : Symmetric (α := ι →₀ M) (Disjoint on Finsupp.support)
Tactic: rwa [List.toFinset_val, List.dedup_eq_self.mpr hn, Multiset.pairwise_coe_iff_pairwise, ←
    List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn]
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
⊢ (s.sum id).support = s.sup Finsupp.support
have suffices : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
Tactic: classical
  suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    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
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
suffices suffices₁ suffices₂ : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ (s.sum id).support = s.sup Finsupp.support
have suffices₃ : ∀ (l : List (ι →₀ M)) (hl : l.toFinset = s) (hn : l.Nodup), Multiset.Pairwise (Disjoint on Finsupp.support) s.val
Tactic: classical
  suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    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
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
suffices suffices₁ suffices₂ : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
suffices₃ :
  ∀ (l : List (ι →₀ M)) (hl : l.toFinset = s) (hn : l.Nodup), Multiset.Pairwise (Disjoint on Finsupp.support) s.val
⊢ (s.sum id).support = s.sup Finsupp.support
have suffices₄ : ∀ (l : List (ι →₀ M)) (hn : l.Nodup) (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support),
  Multiset.Pairwise (Disjoint on Finsupp.support) l.toFinset.val
Tactic: classical
  suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    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
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddCommMonoid M
s : Finset (ι →₀ M)
hs : (↑s : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support
suffices suffices₁ suffices₂ : Multiset.Pairwise (Disjoint on Finsupp.support) s.val
suffices₃ :
  ∀ (l : List (ι →₀ M)) (hl : l.toFinset = s) (hn : l.Nodup), Multiset.Pairwise (Disjoint on Finsupp.support) s.val
suffices₄ :
  ∀ (l : List (ι →₀ M)) (hn : l.Nodup) (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support),
    Multiset.Pairwise (Disjoint on Finsupp.support) l.toFinset.val
⊢ (s.sum id).support = s.sup Finsupp.support
have hr : ∀ (l : List (ι →₀ M)) (hn : l.Nodup) (hs : (↑l.toFinset : Set (ι →₀ M)).PairwiseDisjoint Finsupp.support),
  Symmetric (α := ι →₀ M) (Disjoint on Finsupp.support)
Tactic: classical
  suffices s.1.Pairwise (_root_.Disjoint on Finsupp.support) by
    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
Cleared hypotheses: s, hs