awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α → M
⊢ Eq.{u_8 + 1} (α := M) (sum ((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) f) fun (x : α) (n : M) ↦ n)
    (∑ a : α, f a)
have rw : Eq.{u_8 + 1} (α := M) (sum (∑ a : α, single a (f a)) fun (x : α) (n : M) ↦ n) (∑ a : α, f a)
Tactic: rw [equivFunOnFinite_symm_eq_sum, sum_fintype _ _ fun _ ↦ rfl, coe_univ_sum_single]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α → M
rw : Eq.{u_8 + 1} (α := M) (sum (∑ a : α, single a (f a)) fun (x : α) (n : M) ↦ n) (∑ a : α, f a)
⊢ Eq.{u_8 + 1} (α := M) (sum ((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) f) fun (x : α) (n : M) ↦ n)
    (∑ a : α, f a)
have rw₁ : Eq.{u_8 + 1} (α := M) (∑ i : α, (∑ a : α, single a (f a) : (a : α) → M) i) (∑ a : α, f a)
Tactic: rw [equivFunOnFinite_symm_eq_sum, sum_fintype _ _ fun _ ↦ rfl, coe_univ_sum_single]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α → M
rw : Eq.{u_8 + 1} (α := M) (sum (∑ a : α, single a (f a)) fun (x : α) (n : M) ↦ n) (∑ a : α, f a)
rw₁ : Eq.{u_8 + 1} (α := M) (∑ i : α, (∑ a : α, single a (f a) : (a : α) → M) i) (∑ a : α, f a)
⊢ Eq.{u_8 + 1} (α := M) (sum ((Equiv.symm equivFunOnFinite : (a : α → M) → α →₀ M) f) fun (x : α) (n : M) ↦ n)
    (∑ a : α, f a)
have rw₂ : Eq.{u_8 + 1} (α := M) (∑ i : α, f i) (∑ a : α, f a)
Tactic: rw [equivFunOnFinite_symm_eq_sum, sum_fintype _ _ fun _ ↦ rfl, coe_univ_sum_single]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst : AddZeroClass M
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
⊢ (AddEquiv.symm liftAddHom : (a : (α →₀ M) →+ P) → α → M →+ P)
      (g.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f)) a =
    g.comp (f a)
have rw : AddMonoidHom.comp (g.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f)) (singleAddHom a) = g.comp (f a)
Tactic: rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst : AddZeroClass M
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
rw : AddMonoidHom.comp (g.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f)) (singleAddHom a) = g.comp (f a)
⊢ (AddEquiv.symm liftAddHom : (a : (α →₀ M) →+ P) → α → M →+ P)
      (g.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f)) a =
    g.comp (f a)
have rw₁ : g.comp (AddMonoidHom.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f) (singleAddHom a)) = g.comp (f a)
Tactic: rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst : AddZeroClass M
inst_1 : AddCommMonoid N
inst_2 : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
rw : AddMonoidHom.comp (g.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f)) (singleAddHom a) = g.comp (f a)
rw₁ : g.comp (AddMonoidHom.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f) (singleAddHom a)) = g.comp (f a)
⊢ (AddEquiv.symm liftAddHom : (a : (α →₀ M) →+ P) → α → M →+ P)
      (g.comp ((liftAddHom : (a : α → M →+ N) → (α →₀ M) →+ N) f)) a =
    g.comp (f a)
have rw₂ : g.comp (f a) = g.comp (f a)
Tactic: rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ (embDomain f v).prod g = v.prod fun (a : α) (b : M) ↦ g ((f : (a : α) → β) a) b
have rw : Eq.{u_10 + 1} (α := N)
  (∏ x ∈ v.support, g ((f : (a : α) → β) x) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) x : β)))
  (∏ a ∈ v.support, g ((f : (a : α) → β) a) ((v : (a : α) → M) a))
Tactic: rw [prod, prod, support_embDomain, Finset.prod_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : CommMonoid N
s_1 : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = prod (∑ i ∈ s, g i) h
⊢ ∏ i ∈ cons a s has, (g i).prod h = prod (∑ i ∈ cons a s has, g i) h
have rw : (g a).prod h * ∏ x ∈ s, (g x).prod h = prod (∑ i ∈ cons a s has, g i) h
Tactic: rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : CommMonoid N
s_1 : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = prod (∑ i ∈ s, g i) h
rw : (g a).prod h * ∏ x ∈ s, (g x).prod h = prod (∑ i ∈ cons a s has, g i) h
⊢ ∏ i ∈ cons a s has, (g i).prod h = prod (∑ i ∈ cons a s has, g i) h
have rw₁ : (g a).prod h * prod (∑ i ∈ s, g i) h = prod (∑ i ∈ cons a s has, g i) h
Tactic: rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : CommMonoid N
s_1 : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = prod (∑ i ∈ s, g i) h
rw : (g a).prod h * ∏ x ∈ s, (g x).prod h = prod (∑ i ∈ cons a s has, g i) h
rw₁ : (g a).prod h * prod (∑ i ∈ s, g i) h = prod (∑ i ∈ cons a s has, g i) h
⊢ ∏ i ∈ cons a s has, (g i).prod h = prod (∑ i ∈ cons a s has, g i) h
have rw₂ : (g a).prod h * prod (∑ i ∈ s, g i) h = (g a + ∑ x ∈ s, g x).prod h
Tactic: rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : CommMonoid N
s_1 : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = prod (∑ i ∈ s, g i) h
rw : (g a).prod h * ∏ x ∈ s, (g x).prod h = prod (∑ i ∈ cons a s has, g i) h
rw₁ : (g a).prod h * prod (∑ i ∈ s, g i) h = prod (∑ i ∈ cons a s has, g i) h
rw₂ : (g a).prod h * prod (∑ i ∈ s, g i) h = (g a + ∑ x ∈ s, g x).prod h
⊢ ∏ i ∈ cons a s has, (g i).prod h = prod (∑ i ∈ cons a s has, g i) h
have rw₃ : (g a).prod h * prod (∑ i ∈ s, g i) h = (g a).prod h * prod (∑ x ∈ s, g x) h
Tactic: rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
⊢ (a ::ₘ s).sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
have rw : (a + s.sum).sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
Tactic: rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
rw : (a + s.sum).sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
⊢ (a ::ₘ s).sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
have rw₁ : (a + s.sum).sum h = (a.sum h ::ₘ Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s).sum
Tactic: rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
rw : (a + s.sum).sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
rw₁ : (a + s.sum).sum h = (a.sum h ::ₘ Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s).sum
⊢ (a ::ₘ s).sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
have rw₂ : (a + s.sum).sum h = a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
Tactic: rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
rw : (a + s.sum).sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
rw₁ : (a + s.sum).sum h = (a.sum h ::ₘ Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s).sum
rw₂ : (a + s.sum).sum h = a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
⊢ (a ::ₘ s).sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
have rw₃ : a.sum h + s.sum.sum h = a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
Tactic: rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
f : Multiset (α →₀ M)
h : α → M → N
h₀ : ∀ (a : α), h a 0 = 0
h₁ : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂
a : α →₀ M
s : Multiset (α →₀ M)
ih : s.sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
rw : (a + s.sum).sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
rw₁ : (a + s.sum).sum h = (a.sum h ::ₘ Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s).sum
rw₂ : (a + s.sum).sum h = a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
rw₃ : a.sum h + s.sum.sum h = a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
⊢ (a ::ₘ s).sum.sum h = Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) (a ::ₘ s))
have rw₄ : a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s) =
  a.sum h + Multiset.sum (Multiset.map (fun (g : α →₀ M) ↦ g.sum h) s)
Tactic: rw [Multiset.sum_cons, Multiset.map_cons, Multiset.sum_cons, sum_add_index' h₀ h₁, ih]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)
have refine_1 : Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ ∅, g i))
  (Finset.biUnion ∅ fun (i : ι) ↦ (g i).support)
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
refine_1 :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ ∅, g i))
    (Finset.biUnion ∅ fun (i : ι) ↦ (g i).support)
⊢ Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i))
        (s.biUnion fun (i : ι) ↦ (g i).support) →
      Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ insert a s, g i))
        ((insert a s).biUnion fun (i : ι) ↦ (g i).support)
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s_1 : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
⊢ Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support) →
    Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ insert i s, g i))
      ((insert i s).biUnion fun (i : ι) ↦ (g i).support)
have refine_2 : Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support) →
  (g i + ∑ i ∈ s, g i).support = (g i).support ∪ s.biUnion fun (i : ι) ↦ (g i).support
Tactic: simp only [hi, sum_insert, not_false_iff, biUnion_insert]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s_1 : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)
⊢ (g i + ∑ i ∈ s, g i).support = (g i).support ∪ s.biUnion fun (i : ι) ↦ (g i).support
have refine_2 : Disjoint (g i).support (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i))
Tactic: rw [Finsupp.support_add_eq, hs]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s_1 : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
i : ι
s : Finset ι
hi : i ∉ s
hs :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)
⊢ Disjoint (g i).support (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i))
have refine_2 : ∀ i_1 ∈ s, Disjoint (g i).support (g i_1).support
Tactic: rw [hs, Finset.disjoint_biUnion_right]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
⊢ Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)
have refine_1 : Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ ∅, g i))
  (Finset.biUnion ∅ fun (i : ι) ↦ (g i).support)
Tactic: classical
  refine Finset.induction_on s ?_ ?_
  · simp
  · intro i s hi
    simp only [hi, sum_insert, not_false_iff, biUnion_insert]
    intro hs
    rw [Finsupp.support_add_eq, hs]
    rw [hs, Finset.disjoint_biUnion_right]
    intro j hj
    exact h _ _ (ne_of_mem_of_not_mem hj hi).symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_16
ι : Type u_17
M : Type u_18
inst : DecidableEq α
inst_1 : AddCommMonoid M
g : ι → α →₀ M
s : Finset ι
h : ∀ (i₁ i₂ : ι), i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support
refine_1 :
  Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ ∅, g i))
    (Finset.biUnion ∅ fun (i : ι) ↦ (g i).support)
⊢ Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i)) (s.biUnion fun (i : ι) ↦ (g i).support)
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ s, g i))
        (s.biUnion fun (i : ι) ↦ (g i).support) →
      Eq.{u_16 + 1} (α := Finset α) (support.{u_16, u_18} (M := M) (∑ i ∈ insert a s, g i))
        ((insert a s).biUnion fun (i : ι) ↦ (g i).support)
Tactic: classical
  refine Finset.induction_on s ?_ ?_
  · simp
  · intro i s hi
    simp only [hi, sum_insert, not_false_iff, biUnion_insert]
    intro hs
    rw [Finsupp.support_add_eq, hs]
    rw [hs, Finset.disjoint_biUnion_right]
    intro j hj
    exact h _ _ (ne_of_mem_of_not_mem hj hi).symm
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst_1 : CommMonoid β
g : α → M → β
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g
have this : ∀ {f1 f2 : α →₀ M},
  Disjoint f1.support f2.support →
    ∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)) =
      f1.prod g
Tactic: have :
    ∀ {f1 f2 : α →₀ M},
      Disjoint f1.support f2.support → (∏ x ∈ f1.support, g x (f1 x + f2 x)) = f1.prod g :=
    fun hd =>
    Finset.prod_congr rfl fun x hx => by
      simp only [notMem_support_iff.mp (disjoint_left.mp hd hx), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst_1 : CommMonoid β
g : α → M → β
this :
  ∀ {f1 f2 : α →₀ M},
    Disjoint f1.support f2.support →
      ∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)) =
        f1.prod g
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g
have simp_rw : (f1 + f2).prod g =
  (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M))) *
    f2.prod g
Tactic: simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd,
      prod_union hd, add_apply]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst_1 : CommMonoid β
g : α → M → β
this :
  ∀ {f1 f2 : α →₀ M},
    Disjoint f1.support f2.support →
      ∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)) =
        f1.prod g
simp_rw :
  (f1 + f2).prod g =
    (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M))) *
      f2.prod g
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g
have simp_rw₁ : (f1 + f2).prod g =
  HMul.hMul (α := β)
    (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
    (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f2 : (a : α) → M) x : M) ((f1 : (a : α) → M) x : M)))
Tactic: simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd,
      prod_union hd, add_apply]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst_1 : CommMonoid β
g : α → M → β
this :
  ∀ {f1 f2 : α →₀ M},
    Disjoint f1.support f2.support →
      ∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)) =
        f1.prod g
simp_rw :
  (f1 + f2).prod g =
    (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M))) *
      f2.prod g
simp_rw₁ :
  (f1 + f2).prod g =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f2 : (a : α) → M) x : M) ((f1 : (a : α) → M) x : M)))
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g
have simp_rw₂ : (f1 + f2).prod g =
  HMul.hMul (α := β)
    (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
    (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
Tactic: simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd,
      prod_union hd, add_apply]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst_1 : CommMonoid β
g : α → M → β
this :
  ∀ {f1 f2 : α →₀ M},
    Disjoint f1.support f2.support →
      ∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)) =
        f1.prod g
simp_rw :
  (f1 + f2).prod g =
    (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M))) *
      f2.prod g
simp_rw₁ :
  (f1 + f2).prod g =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f2 : (a : α) → M) x : M) ((f1 : (a : α) → M) x : M)))
simp_rw₂ :
  (f1 + f2).prod g =
    HMul.hMul (α := β)
      (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
      (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g
have simp_rw₃ : ∏ a ∈ (f1 + f2).support, g a ((f1 + f2 : (a : α) → M) a) =
  HMul.hMul (α := β)
    (∏ x ∈ f1.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
    (∏ x ∈ f2.support, g x (HAdd.hAdd (α := M) (β := M) ((f1 : (a : α) → M) x : M) ((f2 : (a : α) → M) x : M)))
Tactic: simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd,
      prod_union hd, add_apply]