awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
r : R
m : M
⊢ Eq (α := R[M]) (single m r) 0 ↔ r = 0

Tactic:
Finsupp.single_eq_zero

Premises used: Finsupp.single_eq_zero, MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
r : R
m : M
⊢ Ne (α := R[M]) (single m r) 0 ↔ r ≠ 0

Tactic:
simp [single]

Premises used: MonoidAlgebra.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
p : R[M] → Prop
x : R[M]
zero : p 0
add : ∀ (x y : R[M]), p x → p y → p (x + y)
single : ∀ (m : M) (r : R), p (MonoidAlgebra.single m r)
⊢ p x

Tactic:
Finsupp.induction_linear x zero (fun _ _ ↦ add _ _) (fun _ _ ↦ single _ _)

Premises used: Finsupp.induction_linear
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : One M
⊢ Eq (α := R[M]) 1 (single 1 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
⊢ x * y = sum x fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)

Tactic:
rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
x y : R[M]
⊢ x * y = sum x fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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 : Mul M
simp :
  ∀ (a b c : R[M]),
    (sum a fun (m₁ : M) (r₁ : R) ↦ sum (b + c) fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)) =
      HAdd.hAdd (α := R[M]) (sum a fun (m₁ : M) (r₁ : R) ↦ sum b fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
        (sum a fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
⊢ ∀ (a b c : R[M]), a * (b + c) = a * b + a * c

Tactic:
simp [mul_def]

Premises used: MonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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 : Mul M
⊢ ∀ (a b c : R[M]),
    (sum a fun (m₁ : M) (r₁ : R) ↦ sum (b + c) fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)) =
      HAdd.hAdd (α := R[M]) (sum a fun (m₁ : M) (r₁ : R) ↦ sum b fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
        (sum a fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))

Tactic:
simp [MonoidAlgebra, sum_add_index, mul_add]

Premises used: MonoidAlgebra, mul_add, Finsupp.sum_add_index
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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 : Mul M
classical classical₁ :
  ∀ (a b c : R[M]),
    (sum a fun (m₁ : M) (r₁ : R) ↦ sum (b + c) fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)) =
      HAdd.hAdd (α := R[M]) (sum a fun (m₁ : M) (r₁ : R) ↦ sum b fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
        (sum a fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
⊢ ∀ (a b c : R[M]), a * (b + c) = a * b + a * c

Tactic:
classical simp [mul_def]; simp [MonoidAlgebra, sum_add_index, mul_add]

Premises used: MonoidAlgebra.mul_def, MonoidAlgebra, mul_add, Finsupp.sum_add_index
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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 : Mul M
simp :
  ∀ (a b c : R[M]),
    (sum (a + b) fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)) =
      HAdd.hAdd (α := R[M]) (sum a fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
        (sum b fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
⊢ ∀ (a b c : R[M]), (a + b) * c = a * c + b * c

Tactic:
simp [mul_def]

Premises used: MonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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 : Mul M
⊢ ∀ (a b c : R[M]),
    (sum (a + b) fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)) =
      HAdd.hAdd (α := R[M]) (sum a fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
        (sum b fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))

Tactic:
simp [MonoidAlgebra, sum_add_index, add_mul]

Premises used: add_mul, MonoidAlgebra, Finsupp.sum_add_index
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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 : Mul M
classical classical₁ :
  ∀ (a b c : R[M]),
    (sum (a + b) fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂)) =
      HAdd.hAdd (α := R[M]) (sum a fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
        (sum b fun (m₁ : M) (r₁ : R) ↦ sum c fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
⊢ ∀ (a b c : R[M]), (a + b) * c = a * c + b * c

Tactic:
classical simp [mul_def]; simp [MonoidAlgebra, sum_add_index, add_mul]

Premises used: add_mul, MonoidAlgebra.mul_def, MonoidAlgebra, Finsupp.sum_add_index
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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 : Mul M
⊢ ∀ (a : R[M]), 0 * a = 0

Tactic:
simp [mul_def]

Premises used: MonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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 : Mul M
⊢ ∀ (a : R[M]), a * 0 = 0

Tactic:
simp [mul_def]

Premises used: MonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m : M
rw :
  Eq (α := R) (sum x fun (a₁ : M) (b : R) ↦ (sum y fun (m₂ : M) (r₂ : R) ↦ single (a₁ * m₂) (b * r₂) : (a : M) → R) m)
    (sum x fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0)
⊢ Eq (α := R) ((x * y : (a : M) → R) m : R)
    (sum x fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 : R)

Tactic:
rw [mul_def, Finsupp.sum_apply]

Premises used: MonoidAlgebra.mul_def, Finsupp.sum_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m : M
e_g :
  Eq (α := M → R → R) (fun (a₁ : M) (b : R) ↦ (sum y fun (m₂ : M) (r₂ : R) ↦ single (a₁ * m₂) (b * r₂) : (a : M) → R) m)
    fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0
⊢ Eq (α := R) (sum x fun (a₁ : M) (b : R) ↦ (sum y fun (m₂ : M) (r₂ : R) ↦ single (a₁ * m₂) (b * r₂) : (a : M) → R) m)
    (sum x fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0)

Tactic:
congr
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m : M
e_g :
  ∀ (x : M) (x_1 : R),
    Eq (α := R) ((sum y fun (m₂ : M) (r₂ : R) ↦ single (x * m₂) (x_1 * r₂) : (a : M) → R) m : R)
      (sum y fun (m₂ : M) (r₂ : R) ↦ if x * m₂ = m then x_1 * r₂ else 0 : R)
⊢ Eq (α := M → R → R) (fun (a₁ : M) (b : R) ↦ (sum y fun (m₂ : M) (r₂ : R) ↦ single (a₁ * m₂) (b * r₂) : (a : M) → R) m)
    fun (m₁ : M) (r₁ : R) ↦ sum y fun (m₂ : M) (r₂ : R) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m x_1 : M
x_2 : R
e_g :
  Eq (α := R) (sum y fun (a₁ : M) (b : R) ↦ (single (x_1 * a₁) (x_2 * b) : (a : M) → R) m)
    (sum y fun (m₂ : M) (r₂ : R) ↦ if x_1 * m₂ = m then x_2 * r₂ else 0)
⊢ Eq (α := R) ((sum y fun (m₂ : M) (r₂ : R) ↦ single (x_1 * m₂) (x_2 * r₂) : (a : M) → R) m : R)
    (sum y fun (m₂ : M) (r₂ : R) ↦ if x_1 * m₂ = m then x_2 * r₂ else 0 : R)

Tactic:
rw [Finsupp.sum_apply]

Premises used: Finsupp.sum_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m x_1 : M
x_2 : R
e_g :
  Eq (α := M → R → R) (fun (a₁ : M) (b : R) ↦ (single (x_1 * a₁) (x_2 * b) : (a : M) → R) m) fun (m₂ : M) (r₂ : R) ↦
    if x_1 * m₂ = m then x_2 * r₂ else 0
⊢ Eq (α := R) (sum y fun (a₁ : M) (b : R) ↦ (single (x_1 * a₁) (x_2 * b) : (a : M) → R) m)
    (sum y fun (m₂ : M) (r₂ : R) ↦ if x_1 * m₂ = m then x_2 * r₂ else 0)

Tactic:
congr
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m x_1 : M
x_2 : R
e_g : ∀ (x : M) (x_3 : R), (single (x_1 * x) (x_2 * x_3) : (a : M) → R) m = if x_1 * x = m then x_2 * x_3 else 0
⊢ Eq (α := M → R → R) (fun (a₁ : M) (b : R) ↦ (single (x_1 * a₁) (x_2 * b) : (a : M) → R) m) fun (m₂ : M) (r₂ : R) ↦
    if x_1 * m₂ = m then x_2 * r₂ else 0

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
inst_2 : DecidableEq M
x y : R[M]
m x_1 : M
x_2 : R
x_3 : M
x_4 : R
⊢ (single (x_1 * x_3) (x_2 * x_4) : (a : M) → R) m = if x_1 * x_3 = m then x_2 * x_4 else 0

Tactic:
apply single_apply

Premises used: MonoidAlgebra.single_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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) (∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂) : R)

Tactic:
mul_apply ..

Premises used: Finsupp.sum, MonoidAlgebra.mul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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
rw :
  Eq.{u_1 + 1} (α := R) (∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂))
    (∑ a ∈ x.support ×ˢ y.support,
      if a.1 * a.2 = m then HMul.hMul (α := R) (β := R) ((x : (a : M) → R) a.1 : R) ((y : (a : M) → R) a.2 : R) else 0)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R) (∑ m₁ ∈ x.support, ∑ m₂ ∈ y.support, F (m₁, m₂))
    (∑ x_1 ∈ x.support,
      ∑ y_1 ∈ y.support,
        if (x_1, y_1).1 * (x_1, y_1).2 = m then
          HMul.hMul (α := R) (β := R) ((x : (a : M) → R) (x_1, y_1).1 : R) ((y : (a : M) → R) (x_1, y_1).2 : R)
        else 0)
⊢ 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:
rw [Finset.sum_filter, Finset.sum_product]

Premises used: Finset.sum_filter, Finset.sum_product
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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
h : {p ∈ x.support ×ˢ y.support | p.1 * p.2 = m} = {p ∈ s | p.1 ∈ x.support ∧ p.2 ∈ y.support}
⊢ 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:
congr! 1
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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
h : ∀ (a : M × M), a ∈ {p ∈ x.support ×ˢ y.support | p.1 * p.2 = m} ↔ a ∈ {p ∈ s | p.1 ∈ x.support ∧ p.2 ∈ y.support}
⊢ {p ∈ x.support ×ˢ y.support | p.1 * p.2 = m} = {p ∈ s | p.1 ∈ x.support ∧ p.2 ∈ y.support}

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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
a : M × M
⊢ a ∈ {p ∈ x.support ×ˢ y.support | p.1 * p.2 = m} ↔ a ∈ {p ∈ s | p.1 ∈ x.support ∧ p.2 ∈ y.support}

Tactic:
simp only [mem_filter, mem_product, hs, and_comm]

Premises used: and_comm, Finset.mem_filter, Finset.mem_product
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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 ∉ {p ∈ s | p.1 ∈ x.support ∧ p.2 ∈ y.support}
⊢ 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)

Tactic:
simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢

Premises used: Finsupp.mem_support_iff, Classical.not_not, Finset.mem_filter, not_and
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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
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
⊢ 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

Premises used: Prod.fst, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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
pos₁ pos₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0

Tactic:
rw [h1, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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
neg₁ neg₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((x : (a : M) → R) p.1 : R) ((y : (a : M) → R) p.2 : R) = 0

Tactic:
rw [hp hps h1, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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))
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))
⊢ 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)

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]

Premises used: HMul.hMul, Finsupp.support, Finset.filter_subset, Finset.sum_subset, MonoidAlgebra.mul_apply, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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
let let₁ let₂ :
  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)
⊢ 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)

Tactic:
classical
  let F (p : M × M) : R := if p.1 * p.2 = m then x p.1 * y p.2 else 0
  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]

Premises used: HMul.hMul, Finsupp.support, Finset.filter_subset, Finset.sum_subset, MonoidAlgebra.mul_apply, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Mul M
m₁ m₂ : M
r₁ r₂ : R
⊢ HMul.hMul (α := R[M]) (single m₁ r₁) (single m₂ r₂) = single (m₁ * m₂) (r₁ * r₂)

Tactic:
simp [mul_def]

Premises used: MonoidAlgebra.mul_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
r₁ r₂ : R
m₁ m₂ : M
inst_1 : Mul M
hm : Commute m₁ m₂
hr : Commute r₁ r₂
⊢ Commute (S := R[M]) (single m₁ r₁) (single m₂ r₂)

Tactic:
simp [Commute, SemiconjBy, hm.eq, hr.eq]

Premises used: SemiconjBy, Commute, Commute.eq
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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]
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])
⊢ Eq (α := R[M] →+ R[M]) (AddMonoidHom.mulLeft (single m r)) (AddMonoidHom.mulRight (single m r))

Tactic:
ext m' r' : 2
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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]
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:
single_commute_single (hm m') (hr r')

Premises used: Multiset.sum, Multiset.foldr, SemiconjBy, Finsupp.sum, Commute, MonoidAlgebra.single_commute_single, Finset.sum, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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]
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:
exact single_commute_single (hm m') (hr r')

Premises used: MonoidAlgebra.single_commute_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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))

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')
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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]
this : Eq (α := R[M] →+ R[M]) (AddMonoidHom.mulLeft (single m r)) (AddMonoidHom.mulRight (single m r))
⊢ Commute (single m r) x

Tactic:
congr($this x)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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]
this : Eq (α := R[M] →+ R[M]) (AddMonoidHom.mulLeft (single m r)) (AddMonoidHom.mulRight (single m r))
⊢ Commute (single m r) x

Tactic:
exact congr($this x)
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
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₂
⊢ 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:
simp [mul_apply]

Premises used: MonoidAlgebra.mul_apply