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 : 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)))
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)))
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g
have simp_rw₄ : ∏ x ∈ f1.support ∪ f2.support, g x ((f1 + f2 : (a : α) → M) x) =
  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)))
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)))
simp_rw₄ :
  ∏ x ∈ f1.support ∪ f2.support, g x ((f1 + f2 : (a : α) → M) x) =
    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₅ : HMul.hMul (α := β) (∏ x ∈ f1.support, g x ((f1 + f2 : (a : α) → M) x))
    (∏ x ∈ f2.support, g x ((f1 + f2 : (a : α) → M) x)) =
  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
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g
have classical : (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: classical 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
classical :
  (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 classical₁ : (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: classical 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
classical :
  (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
classical₁ :
  (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 classical₂ : (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: classical 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
classical :
  (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
classical₁ :
  (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)))
classical₂ :
  (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 classical₃ : ∏ 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: classical 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
classical :
  (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
classical₁ :
  (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)))
classical₂ :
  (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)))
classical₃ :
  ∏ 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)))
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g
have classical₄ : ∏ x ∈ f1.support ∪ f2.support, g x ((f1 + f2 : (a : α) → M) x) =
  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: classical 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
classical :
  (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
classical₁ :
  (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)))
classical₂ :
  (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)))
classical₃ :
  ∏ 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)))
classical₄ :
  ∏ x ∈ f1.support ∪ f2.support, g x ((f1 + f2 : (a : α) → M) x) =
    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 classical₅ : HMul.hMul (α := β) (∏ x ∈ f1.support, g x ((f1 + f2 : (a : α) → M) x))
    (∏ x ∈ f2.support, g x ((f1 + f2 : (a : α) → M) x)) =
  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: classical 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
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
⊢ f1.prod g1 ∣ f2.prod g2
have simp : Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a)) (∏ a ∈ f2.support, g2 a ((f2 : (a : α) → M) a))
Tactic: simp only [Finsupp.prod]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
⊢ Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a))
    (∏ a ∈ f2.support, g2 a ((f2 : (a : α) → M) a))
have rw : ∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣
  HMul.hMul (α := N) (∏ x ∈ f2.support \ f1.support, g2 x ((f2 : (a : α) → M) x))
    (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))
Tactic: rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
⊢ ∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣
    HMul.hMul (α := N) (∏ x ∈ f2.support \ f1.support, g2 x ((f2 : (a : α) → M) x))
      (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))
have h : Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a)) (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))
Tactic: apply dvd_mul_of_dvd_right
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
⊢ f1.prod g1 ∣ f2.prod g2
have simp : Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a)) (∏ a ∈ f2.support, g2 a ((f2 : (a : α) → M) a))
Tactic: classical
    simp only [Finsupp.prod]
    rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]
    apply dvd_mul_of_dvd_right
    apply prod_dvd_prod_of_dvd
    exact h2
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
simp :
  Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a))
    (∏ a ∈ f2.support, g2 a ((f2 : (a : α) → M) a))
⊢ f1.prod g1 ∣ f2.prod g2
have simp₁ : ∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣
  HMul.hMul (α := N) (∏ x ∈ f2.support \ f1.support, g2 x ((f2 : (a : α) → M) x))
    (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))
Tactic: classical
    simp only [Finsupp.prod]
    rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]
    apply dvd_mul_of_dvd_right
    apply prod_dvd_prod_of_dvd
    exact h2
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f1 f2 : α →₀ M
g1 g2 : α → M → N
h1 : f1.support ⊆ f2.support
h2 : ∀ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣ g2 a ((f2 : (a : α) → M) a)
simp :
  Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a))
    (∏ a ∈ f2.support, g2 a ((f2 : (a : α) → M) a))
simp₁ :
  ∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a) ∣
    HMul.hMul (α := N) (∏ x ∈ f2.support \ f1.support, g2 x ((f2 : (a : α) → M) x))
      (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))
⊢ f1.prod g1 ∣ f2.prod g2
have h : Dvd.dvd.{u_10} (α := N) (∏ a ∈ f1.support, g1 a ((f1 : (a : α) → M) a)) (∏ x ∈ f1.support, g2 x ((f2 : (a : α) → M) x))
Tactic: classical
    simp only [Finsupp.prod]
    rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]
    apply dvd_mul_of_dvd_right
    apply prod_dvd_prod_of_dvd
    exact h2
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ Eq (α := α →₀ M) (indicator s f) (∑ x ∈ s.attach, single (↑x : α) (f (↑x : α) ⋯))
have rw : Eq (α := α →₀ M) (∑ x ∈ s.attach, single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
  (∑ x ∈ s.attach, single (↑x : α) (f (↑x : α) sorry))
Tactic: rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
rw :
  Eq (α := α →₀ M) (∑ x ∈ s.attach, single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
    (∑ x ∈ s.attach, single (↑x : α) (f (↑x : α) ⋯))
⊢ Eq (α := α →₀ M) (indicator s f) (∑ x ∈ s.attach, single (↑x : α) (f (↑x : α) ⋯))
have rw₁ : ∀ x ∈ s,
  x ∉ support (indicator s f) → Eq (α := α →₀ M) (single x ((indicator s f : (a : α) → M) x) : α →₀ M) (0 : α →₀ M)
Tactic: rw [← sum_single (indicator s f), sum, sum_subset (support_indicator_subset _ _), ← sum_attach]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
⊢ Eq (α := α →₀ M) (∑ x ∈ s.attach, single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
    (∑ x ∈ s.attach, single (↑x : α) (f (↑x : α) ⋯))
have refine : ∀ x ∈ s.attach,
  Eq (α := α →₀ M) (single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)) : α →₀ M)
    (single (↑x : α) (f (↑x : α) sorry) : α →₀ M)
Tactic: refine Finset.sum_congr rfl (fun _ _ => ?_)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
x : ↥s
h : x ∈ s.attach
⊢ Eq (α := α →₀ M) (single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)) : α →₀ M)
    (single (↑x : α) (f (↑x : α) ⋯) : α →₀ M)
have rw : Eq (α := α →₀ M) (single (↑x : α) (f (↑x : α) sorry)) (single (↑x : α) (f (↑x : α) sorry))
Tactic: rw [indicator_of_mem]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
x : ↥s
h : x ∈ s.attach
rw : Eq (α := α →₀ M) (single (↑x : α) (f (↑x : α) ⋯)) (single (↑x : α) (f (↑x : α) ⋯))
⊢ Eq (α := α →₀ M) (single (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)) : α →₀ M)
    (single (↑x : α) (f (↑x : α) ⋯) : α →₀ M)
have hi : (↑x : α) ∈ s
Tactic: rw [indicator_of_mem]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
h : i ∈ s
hi : i ∉ support (indicator s f)
⊢ Eq (α := α →₀ M) (single i ((indicator s f : (a : α) → M) i) : α →₀ M) (0 : α →₀ M)
have rw : Eq (α := α →₀ M) (single i 0) 0
Tactic: rw [notMem_support_iff.mp hi, single_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s : Finset α
f : (a : α) → a ∈ s → M
i : α
h : i ∈ s
hi : i ∉ support (indicator s f)
rw : Eq (α := α →₀ M) (single i 0) 0
⊢ Eq (α := α →₀ M) (single i ((indicator s f : (a : α) → M) i) : α →₀ M) (0 : α →₀ M)
have rw₁ : Eq (α := α →₀ M) 0 0
Tactic: rw [notMem_support_iff.mp hi, single_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ prod (indicator s f) h = ∏ x ∈ s.attach, h (↑x : α) (f (↑x : α) ⋯)
have rw : Eq.{u_10 + 1} (α := N) (∏ x ∈ s.attach, h (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
  (∏ x ∈ s.attach, h (↑x : α) (f (↑x : α) sorry))
Tactic: rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ Eq.{u_10 + 1} (α := N) (∏ x ∈ s.attach, h (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)))
    (∏ x ∈ s.attach, h (↑x : α) (f (↑x : α) ⋯))
have refine : ∀ x ∈ s.attach, h (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)) = h (↑x : α) (f (↑x : α) sorry)
Tactic: refine Finset.prod_congr rfl (fun _ _ => ?_)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
x : ↥s
h_1 : x ∈ s.attach
⊢ h (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)) = h (↑x : α) (f (↑x : α) ⋯)
have rw : h (↑x : α) (f (↑x : α) sorry) = h (↑x : α) (f (↑x : α) sorry)
Tactic: rw [indicator_of_mem]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
x : ↥s
h_1 : x ∈ s.attach
rw : h (↑x : α) (f (↑x : α) ⋯) = h (↑x : α) (f (↑x : α) ⋯)
⊢ h (↑x : α) ((indicator s f : (a : α) → M) (↑x : α)) = h (↑x : α) (f (↑x : α) ⋯)
have hi : (↑x : α) ∈ s
Tactic: rw [indicator_of_mem]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
ι : Type u_2
γ : Type u_3
B : Type u_5
inst : AddCommMonoid B
A : Type u_16
F : Type u_17
inst_1 : AddZeroClass A
inst_2 : AddCommMonoid F
inst_3 : FunLike F γ B
g : ι →₀ A
k : ι → A → F
x : γ
h0 : Eq.{u_5 + 1} (α := B) ((0 : (a : γ) → B) x : B) (0 : B)
hadd :
  ∀ (f g : F), (f + g : (a : γ) → B) x = HAdd.hAdd (α := B) (β := B) ((f : (a : γ) → B) x : B) ((g : (a : γ) → B) x : B)
⊢ Eq.{u_5 + 1} (α := B) ((g.sum k : (a : γ) → B) x : B) (g.sum fun (i : ι) (a : A) ↦ (k i a : (a : γ) → B) x : B)
have unfold : Eq.{u_5 + 1} (α := B) ((∑ a ∈ g.support, k a ((g : (a : ι) → A) a) : (a : γ) → B) x : B)
  (∑ a ∈ g.support, (fun (i : ι) (a : A) ↦ ((k i a : (a : γ) → B) x : B)) a ((g : (a : ι) → A) a) : B)
Tactic: unfold Finsupp.sum