awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
p : M × M
hps : p ∈ s
hp :
  p ∈ s →
    Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R) →
      Eq.{u_1 + 1} (α := R) ((y : (a : M) → R) p.2 : R) (0 : R)
pos :
  ∀ (h1 : Eq.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R)),
    HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0
have neg : ∀ (h1 : ¬Eq.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R)),
  HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0
Tactic: by_cases h1 : x p.1 = 0
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
p : M × M
hps : p ∈ s
hp :
  p ∈ s →
    Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R) →
      Eq.{u_1 + 1} (α := R) ((y : (a : M) → R) p.2 : R) (0 : R)
h1 : Eq.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R)
⊢ HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0
have pos : HMul.hMul (α := R) (β := R) (0 : R) ((y : (a : M) → R) p.2 : R) = 0
Tactic: rw [h1, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
p : M × M
hps : p ∈ s
hp :
  p ∈ s →
    Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R) →
      Eq.{u_1 + 1} (α := R) ((y : (a : M) → R) p.2 : R) (0 : R)
h1 : Eq.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R)
pos : HMul.hMul (α := R) (β := R) (0 : R) ((y : (a : M) → R) p.2 : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0
have pos₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [h1, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
p : M × M
hps : p ∈ s
hp :
  p ∈ s →
    Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R) →
      Eq.{u_1 + 1} (α := R) ((y : (a : M) → R) p.2 : R) (0 : R)
h1 : ¬Eq.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R)
⊢ HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0
have neg : HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) (0 : R) = 0
Tactic: rw [hp hps h1, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
p : M × M
hps : p ∈ s
hp :
  p ∈ s →
    Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R) →
      Eq.{u_1 + 1} (α := R) ((y : (a : M) → R) p.2 : R) (0 : R)
h1 : ¬Eq.{u_1 + 1} (α := R) ((x : (a : M) → R) p.1 : R) (0 : R)
neg : HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) (0 : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0
have neg₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [hp hps h1, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
⊢ Eq.{u_1 + 1} (α := R) ((x * y : (a : M) → R) m : R)
    (∑ p ∈ s, HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) : R)
have m₁ : Eq.{u_1 + 1} (α := R) (∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂))
  (∑ p ∈ x.support ×ˢ y.support with p.1 * p.2 = m,
    HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R))
Tactic: calc
    (x * y) m = ∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂) := mul_apply ..
    _ = ∑ p ∈ x.support ×ˢ y.support with p.1 * p.2 = m, x p.1 * y p.2 := by
      rw [Finset.sum_filter, Finset.sum_product]
    _ = ∑ p ∈ s with p.1 ∈ x.support ∧ p.2 ∈ y.support, x p.1 * y p.2 := by
      congr! 1; ext; simp only [mem_filter, mem_product, hs, and_comm]
    _ = ∑ p ∈ s, x p.1 * y p.2 :=
      sum_subset (filter_subset _ _) fun p hps hp => by
        simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : x p.1 = 0
        · rw [h1, zero_mul]
        · rw [hp hps h1, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : (p : M × M) → R :=
  fun (p : M × M) ↦
    if p.1 * p.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) else 0
m₁ :
  Eq.{u_1 + 1} (α := R) (∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂))
    (∑ p ∈ x.support ×ˢ y.support with p.1 * p.2 = m,
      HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R))
⊢ Eq.{u_1 + 1} (α := R) ((x * y : (a : M) → R) m : R)
    (∑ p ∈ s, HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) : R)
have m₂ : Eq.{u_1 + 1} (α := R)
  (∑ p ∈ x.support ×ˢ y.support with p.1 * p.2 = m,
    HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R))
  (∑ p ∈ s with p.1 ∈ x.support ∧ p.2 ∈ y.support,
    HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R))
Tactic: calc
    (x * y) m = ∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂) := mul_apply ..
    _ = ∑ p ∈ x.support ×ˢ y.support with p.1 * p.2 = m, x p.1 * y p.2 := by
      rw [Finset.sum_filter, Finset.sum_product]
    _ = ∑ p ∈ s with p.1 ∈ x.support ∧ p.2 ∈ y.support, x p.1 * y p.2 := by
      congr! 1; ext; simp only [mem_filter, mem_product, hs, and_comm]
    _ = ∑ p ∈ s, x p.1 * y p.2 :=
      sum_subset (filter_subset _ _) fun p hps hp => by
        simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : x p.1 = 0
        · rw [h1, zero_mul]
        · rw [hp hps h1, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
r : R
m : M
inst_1 : Mul M
hm : ∀ (m' : M), Commute m m'
hr : ∀ (r' : R), Commute r r'
x : R[M]
⊢ Eq (α := R[M] →+ R[M]) (AddMonoidHom.mulLeft (single m r)) (AddMonoidHom.mulRight (single m r))
have hfg : ∀ (m' : M) (r' : R),
  Eq (α := R[M])
    (((AddMonoidHom.comp (AddMonoidHom.mulLeft (single m r)) (singleAddHom m') : R →+ R[M]) : (a : R) → R[M]) r' : R[M])
    (((AddMonoidHom.comp (AddMonoidHom.mulRight (single m r)) (singleAddHom m') : R →+ R[M]) : (a : R) → R[M]) r' :
      R[M])
Tactic: ext m' r' : 2
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (hypothesis)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
r : R
m : M
inst_1 : Mul M
hm : ∀ (m' : M), Commute m m'
hr : ∀ (r' : R), Commute r r'
x : R[M]
⊢ Commute (single m r) x
have this : Eq (α := R[M] →+ R[M]) (AddMonoidHom.mulLeft (single m r)) (AddMonoidHom.mulRight (single m r))
Tactic: have : AddMonoidHom.mulLeft (single m r) = AddMonoidHom.mulRight (single m r) := by
    ext m' r' : 2; exact single_commute_single (hm m') (hr r')
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m' * m = m₁ ↔ m' = m₂
⊢ (x * single m r : (a : M) → R) m₁ = HMul.hMul (α := R) ((x : (a : M) → R) m₂ : R) r
have single : Eq (α := R) ((x * single m r : (a : M) → R) m₁ : R)
  (sum x fun (m' : M) (r' : R) ↦ if m' * m = m₁ then r' * r else 0 : R)
Tactic: calc
    (x * single m r) m₁
    _ = x.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r' * r else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = x m₂ * r := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m' * m = m₁ ↔ m' = m₂
single :
  Eq (α := R) ((x * MonoidAlgebra.single m r : (a : M) → R) m₁ : R)
    (sum x fun (m' : M) (r' : R) ↦ if m' * m = m₁ then r' * r else 0 : R)
⊢ (x * MonoidAlgebra.single m r : (a : M) → R) m₁ = HMul.hMul (α := R) ((x : (a : M) → R) m₂ : R) r
have single₁ : Eq (α := R) (sum x fun (m' : M) (r' : R) ↦ if m' * m = m₁ then r' * r else 0)
  (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r' * r else 0)
Tactic: calc
    (x * single m r) m₁
    _ = x.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r' * r else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = x m₂ * r := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m' * m = m₁ ↔ m' = m₂
single :
  Eq (α := R) ((x * MonoidAlgebra.single m r : (a : M) → R) m₁ : R)
    (sum x fun (m' : M) (r' : R) ↦ if m' * m = m₁ then r' * r else 0 : R)
single₁ :
  Eq (α := R) (sum x fun (m' : M) (r' : R) ↦ if m' * m = m₁ then r' * r else 0)
    (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r' * r else 0)
⊢ (x * MonoidAlgebra.single m r : (a : M) → R) m₁ = HMul.hMul (α := R) ((x : (a : M) → R) m₂ : R) r
have single₂ : (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r' * r else 0) = HMul.hMul (α := R) ((x : (a : M) → R) m₂ : R) r
Tactic: calc
    (x * single m r) m₁
    _ = x.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r' * r else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = x m₂ * r := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m' * m = m₁ ↔ m' = m₂
⊢ (x * single m r : (a : M) → R) m₁ = HMul.hMul (α := R) ((x : (a : M) → R) m₂ : R) r
have single : Eq (α := R) ((x * single m r : (a : M) → R) m₁ : R)
  (sum x fun (m' : M) (r' : R) ↦ if m' * m = m₁ then r' * r else 0 : R)
Tactic: classical
  calc
    (x * single m r) m₁
    _ = x.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r' * r else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = x m₂ * r := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m' * m = m₁ ↔ m' = m₂
single :
  Eq (α := R) ((x * MonoidAlgebra.single m r : (a : M) → R) m₁ : R)
    (sum x fun (m' : M) (r' : R) ↦ if m' * m = m₁ then r' * r else 0 : R)
⊢ (x * MonoidAlgebra.single m r : (a : M) → R) m₁ = HMul.hMul (α := R) ((x : (a : M) → R) m₂ : R) r
have single₁ : Eq (α := R) (sum x fun (m' : M) (r' : R) ↦ if m' * m = m₁ then r' * r else 0)
  (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r' * r else 0)
Tactic: classical
  calc
    (x * single m r) m₁
    _ = x.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r' * r else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = x m₂ * r := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m' * m = m₁ ↔ m' = m₂
single :
  Eq (α := R) ((x * MonoidAlgebra.single m r : (a : M) → R) m₁ : R)
    (sum x fun (m' : M) (r' : R) ↦ if m' * m = m₁ then r' * r else 0 : R)
single₁ :
  Eq (α := R) (sum x fun (m' : M) (r' : R) ↦ if m' * m = m₁ then r' * r else 0)
    (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r' * r else 0)
⊢ (x * MonoidAlgebra.single m r : (a : M) → R) m₁ = HMul.hMul (α := R) ((x : (a : M) → R) m₂ : R) r
have single₂ : (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r' * r else 0) = HMul.hMul (α := R) ((x : (a : M) → R) m₂ : R) r
Tactic: classical
  calc
    (x * single m r) m₁
    _ = x.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r' * r else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = x m₂ * r := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m * m' = m₁ ↔ m' = m₂
⊢ (single m r * x : (a : M) → R) m₁ = HMul.hMul (β := R) r ((x : (a : M) → R) m₂ : R)
have m₃ : Eq (α := R) ((single m r * x : (a : M) → R) m₁ : R)
  (sum x fun (m' : M) (r' : R) ↦ if m * m' = m₁ then r * r' else 0 : R)
Tactic: calc
    (single m r * x) m₁
    _ = x.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r * r' else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = r * x m₂ := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m * m' = m₁ ↔ m' = m₂
m₃ :
  Eq (α := R) ((single m r * x : (a : M) → R) m₁ : R)
    (sum x fun (m' : M) (r' : R) ↦ if m * m' = m₁ then r * r' else 0 : R)
⊢ (single m r * x : (a : M) → R) m₁ = HMul.hMul (β := R) r ((x : (a : M) → R) m₂ : R)
have m₄ : Eq (α := R) (sum x fun (m' : M) (r' : R) ↦ if m * m' = m₁ then r * r' else 0)
  (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r * r' else 0)
Tactic: calc
    (single m r * x) m₁
    _ = x.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r * r' else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = r * x m₂ := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m * m' = m₁ ↔ m' = m₂
m₃ :
  Eq (α := R) ((single m r * x : (a : M) → R) m₁ : R)
    (sum x fun (m' : M) (r' : R) ↦ if m * m' = m₁ then r * r' else 0 : R)
m₄ :
  Eq (α := R) (sum x fun (m' : M) (r' : R) ↦ if m * m' = m₁ then r * r' else 0)
    (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r * r' else 0)
⊢ (single m r * x : (a : M) → R) m₁ = HMul.hMul (β := R) r ((x : (a : M) → R) m₂ : R)
have m₅ : (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r * r' else 0) = HMul.hMul (β := R) r ((x : (a : M) → R) m₂ : R)
Tactic: calc
    (single m r * x) m₁
    _ = x.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r * r' else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = r * x m₂ := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m * m' = m₁ ↔ m' = m₂
⊢ (single m r * x : (a : M) → R) m₁ = HMul.hMul (β := R) r ((x : (a : M) → R) m₂ : R)
have m₃ : Eq (α := R) ((single m r * x : (a : M) → R) m₁ : R)
  (sum x fun (m' : M) (r' : R) ↦ if m * m' = m₁ then r * r' else 0 : R)
Tactic: classical
  calc
    (single m r * x) m₁
    _ = x.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r * r' else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = r * x m₂ := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m * m' = m₁ ↔ m' = m₂
m₃ :
  Eq (α := R) ((single m r * x : (a : M) → R) m₁ : R)
    (sum x fun (m' : M) (r' : R) ↦ if m * m' = m₁ then r * r' else 0 : R)
⊢ (single m r * x : (a : M) → R) m₁ = HMul.hMul (β := R) r ((x : (a : M) → R) m₂ : R)
have m₄ : Eq (α := R) (sum x fun (m' : M) (r' : R) ↦ if m * m' = m₁ then r * r' else 0)
  (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r * r' else 0)
Tactic: classical
  calc
    (single m r * x) m₁
    _ = x.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r * r' else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = r * x m₂ := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
x : R[M]
r : R
m m₁ m₂ : M
inst_1 : Mul M
H : ∀ m' ∈ x.support, m * m' = m₁ ↔ m' = m₂
m₃ :
  Eq (α := R) ((single m r * x : (a : M) → R) m₁ : R)
    (sum x fun (m' : M) (r' : R) ↦ if m * m' = m₁ then r * r' else 0 : R)
m₄ :
  Eq (α := R) (sum x fun (m' : M) (r' : R) ↦ if m * m' = m₁ then r * r' else 0)
    (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r * r' else 0)
⊢ (single m r * x : (a : M) → R) m₁ = HMul.hMul (β := R) r ((x : (a : M) → R) m₂ : R)
have m₅ : (sum x fun (m' : M) (r' : R) ↦ if m' = m₂ then r * r' else 0) = HMul.hMul (β := R) r ((x : (a : M) → R) m₂ : R)
Tactic: classical
  calc
    (single m r * x) m₁
    _ = x.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0 := by simp [mul_apply]
    _ = x.sum fun m' r' ↦ if m' = m₂ then r * r' else 0 := by
      dsimp [Finsupp.sum]; congr! 2; simp [*]
    _ = r * x m₂ := by simp +contextual [Finsupp.sum_eq_single m₂]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Semigroup M
⊢ ∀ (a b c : R[M]), a * b * c = a * (b * c)
have simp : ∀ (a b c : R[M]),
  Eq (α := R[M])
    (sum (sum a fun (m₁ : M) (r₁ : R) ↦ sum b fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
      fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
    (sum a fun (m₁ : M) (r₁ : R) ↦
      sum (sum b fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
        fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
Tactic: simp [mul_def]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Monoid M
inst_2 : Monoid N
⊢ ∀ (a : R), IsUnit (M := R[M]) ((singleOneRingHom : (a : R) → R[M]) a : R[M]) → IsUnit a
have simp_rw : ∀ (a : R),
  (∃ (b : R[M]),
      HMul.hMul (α := R[M]) ((singleOneRingHom : (a : R) → R[M]) a : R[M]) b = 1 ∧
        HMul.hMul (β := R[M]) b ((singleOneRingHom : (a : R) → R[M]) a : R[M]) = 1) →
    ∃ (b : R), a * b = 1 ∧ b * a = 1
Tactic: simp_rw [isUnit_iff_exists]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x_1 y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Monoid M
inst_2 : Monoid N
a : R
x : R[M]
hax : HMul.hMul (α := R[M]) ((singleOneRingHom : (a : R) → R[M]) a : R[M]) x = 1
hxa : HMul.hMul (β := R[M]) x ((singleOneRingHom : (a : R) → R[M]) a : R[M]) = 1
⊢ ∃ (b : R), a * b = 1 ∧ b * a = 1
have refine_1 : HMul.hMul (β := R) a ((x : (a : M) → R) 1 : R) = 1
Tactic: refine ⟨x 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x_1 y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Monoid M
inst_2 : Monoid N
a : R
x : R[M]
hax : HMul.hMul (α := R[M]) ((singleOneRingHom : (a : R) → R[M]) a : R[M]) x = 1
hxa : HMul.hMul (β := R[M]) x ((singleOneRingHom : (a : R) → R[M]) a : R[M]) = 1
refine_1 : HMul.hMul (β := R) a ((x : (a : M) → R) 1 : R) = 1
⊢ ∃ (b : R), a * b = 1 ∧ b * a = 1
have refine_2 : HMul.hMul (α := R) ((x : (a : M) → R) 1 : R) a = 1
Tactic: refine ⟨x 1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x_1 y_1 : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Subsingleton M
x y : R[M]
this : Unique M := { default := 1, uniq := ⋯ }
⊢ Equiv.toFun (AddEquiv.toEquiv (uniqueAddEquiv 1)) (x * y) =
    HMul.hMul (α := R) (Equiv.toFun (AddEquiv.toEquiv (uniqueAddEquiv 1)) x)
      (Equiv.toFun (AddEquiv.toEquiv (uniqueAddEquiv 1)) y)
have refine : (sum x fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = 1 then r₁ * r₂ else 0) =
  HMul.hMul (α := R) (Equiv.toFun (AddEquiv.toEquiv (uniqueAddEquiv 1)) x)
    (Equiv.toFun (AddEquiv.toEquiv (uniqueAddEquiv 1)) y)
Tactic: refine (mul_apply ..).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (hypothesis)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Monoid M
inst_2 : Monoid N
f : R[M × N] →+ R[N][M] := AddEquiv.toAddMonoidHom curryAddEquiv
⊢ ∀ (x y : R[M × N]),
    Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) (x * y) =
      HMul.hMul (α := R[N][M]) (β := R[N][M]) (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) x : R[N][M])
        (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) y)
have this : ∀ {mn : M × N} {r : R},
  Eq (α := R[N][M]) ((f : (a : R[M × N]) → R[N][M]) (single mn r) : R[N][M]) (single mn.1 (single mn.2 r) : R[N][M])
Tactic: have {mn r} : f (single mn r) = single mn.1 (single mn.2 r) := Finsupp.curry_single _ _
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ : M
inst_1 : Monoid M
inst_2 : Monoid N
f : R[M × N] →+ R[N][M] := AddEquiv.toAddMonoidHom curryAddEquiv
this :
  ∀ {mn : M × N} {r : R},
    Eq (α := R[N][M]) ((f : (a : R[M × N]) → R[N][M]) (single mn r) : R[N][M]) (single mn.1 (single mn.2 r) : R[N][M])
⊢ ∀ (x y : R[M × N]),
    Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) (x * y) =
      HMul.hMul (α := R[N][M]) (β := R[N][M]) (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) x : R[N][M])
        (Equiv.toFun (AddEquiv.toEquiv curryAddEquiv) y)
have refine : AddMonoidHom.compr₂ AddMonoidHom.mul f = (AddMonoidHom.comp AddMonoidHom.mul f).compl₂ f
Tactic: refine f.map_mul_iff.2 ?_