awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 a : ∀ x_1 ∈ x.support, x_1 * m = m₁ ↔ x_1 = m₂
⊢ Eq.{u_1 + 1} (α := R) (∑ a ∈ x.support, if a * m = m₁ then HMul.hMul (α := R) ((x : (a : M) → R) a : R) r else 0)
    (∑ a ∈ x.support, if a = m₂ then HMul.hMul (α := R) ((x : (a : M) → R) a : R) r else 0)

Tactic:
congr! 2
-- 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₂
x_1 : M
h : x_1 ∈ x.support
⊢ x_1 * m = m₁ ↔ x_1 = m₂

Tactic:
simp [*]
-- 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₂
⊢ (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:
simp +contextual [Finsupp.sum_eq_single m₂]

Premises used: Finsupp.sum_eq_single
-- 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₂
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)
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
⊢ (x * MonoidAlgebra.single m r : (a : M) → R) m₁ = 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₂]

Premises used: HMul.hMul, Finsupp.sum, OfNat.ofNat, Eq, DFunLike.coe, MonoidAlgebra.single, ite
-- 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₂
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)
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
⊢ (x * MonoidAlgebra.single m r : (a : M) → R) m₁ = 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₂]

Premises used: HMul.hMul, DFunLike.coe, MonoidAlgebra.single
-- 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) ((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:
simp [mul_apply]

Premises used: MonoidAlgebra.mul_apply
-- 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 a : ∀ x_1 ∈ x.support, m * x_1 = m₁ ↔ x_1 = m₂
⊢ Eq.{u_1 + 1} (α := R) (∑ a ∈ x.support, if m * a = m₁ then HMul.hMul (β := R) r ((x : (a : M) → R) a : R) else 0)
    (∑ a ∈ x.support, if a = m₂ then HMul.hMul (β := R) r ((x : (a : M) → R) a : R) else 0)

Tactic:
congr! 2
-- 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₂
x_1 : M
h : x_1 ∈ x.support
⊢ m * x_1 = m₁ ↔ x_1 = m₂

Tactic:
simp [*]
-- 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₂
⊢ (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:
simp +contextual [Finsupp.sum_eq_single m₂]

Premises used: Finsupp.sum_eq_single
-- 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₂
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)
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)
⊢ (single m r * x : (a : M) → R) m₁ = 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₂]

Premises used: HMul.hMul, Finsupp.sum, OfNat.ofNat, Eq, DFunLike.coe, MonoidAlgebra.single, ite
-- 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₂
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)
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)
⊢ (single m r * x : (a : M) → R) m₁ = 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₂]

Premises used: HMul.hMul, DFunLike.coe, MonoidAlgebra.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m m' : M
inst_1 : Mul M
r : R
x : R[M]
h : ¬∃ (d : M), m' = d * m
⊢ Eq.{u_1 + 1} (α := R) ((x * single m r : (a : M) → R) m' : R) (0 : R)

Tactic:
simp_all [mul_apply, eq_comm]

Premises used: eq_comm, MonoidAlgebra.mul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m m' : M
inst_1 : Mul M
r : R
x : R[M]
h : ¬∃ (d : M), m' = d * m
⊢ Eq.{u_1 + 1} (α := R) ((x * single m r : (a : M) → R) m' : R) (0 : R)

Tactic:
classical simp_all [mul_apply, eq_comm]

Premises used: eq_comm, MonoidAlgebra.mul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m m' : M
inst_1 : Mul M
r : R
x : R[M]
h : ¬∃ (d : M), m' = m * d
⊢ Eq.{u_1 + 1} (α := R) ((single m r * x : (a : M) → R) m' : R) (0 : R)

Tactic:
simp_all [mul_apply, eq_comm]

Premises used: eq_comm, MonoidAlgebra.mul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m m' : M
inst_1 : Mul M
r : R
x : R[M]
h : ¬∃ (d : M), m' = m * d
⊢ Eq.{u_1 + 1} (α := R) ((single m r * x : (a : M) → R) m' : R) (0 : R)

Tactic:
classical simp_all [mul_apply, eq_comm]

Premises used: eq_comm, MonoidAlgebra.mul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R_1 : Type u_1
S : Type u_2
G : Type u_3
M_1 : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst : Semiring R_1
x y : R_1[M_1]
r r₁ r₂ : R_1
m m' m₁ m₂ : M_1
inst_1 : Mul M_1
R : Type u_8
M : Type u_9
inst_2 : Semiring R
inst_3 : Mul M
a b : M
⊢ single (a * b) 1 = HMul.hMul (α := R[M]) (single a 1) (single b 1)

Tactic:
simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero]

Premises used: MonoidAlgebra.mul_def, MonoidAlgebra.single_eq_zero, MulZeroClass.mul_zero, mul_one, MonoidAlgebra.sum_single_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 : Semigroup M
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₂))
⊢ ∀ (a b c : R[M]), a * b * c = a * (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 : Semigroup M
⊢ ∀ (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 [MonoidAlgebra, sum_sum_index, mul_add, add_mul, mul_assoc]

Premises used: add_mul, mul_assoc, MonoidAlgebra, mul_add, Finsupp.sum_sum_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 : MulOneClass M
⊢ ∀ (a : R[M]), 1 * a = a

Tactic:
simp [mul_def, one_def]

Premises used: MonoidAlgebra.mul_def, MonoidAlgebra.one_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 : MulOneClass M
⊢ ∀ (a : R[M]), a * 1 = a

Tactic:
simp [mul_def, one_def]

Premises used: MonoidAlgebra.mul_def, MonoidAlgebra.one_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 : MulOneClass M
⊢ Eq (α := R[M]) (single 1 (↑0 : R)) 0

Tactic:
simp
-- 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 : MulOneClass M
⊢ ∀ (n : ℕ), single 1 (↑(n + 1) : R) = HAdd.hAdd (α := R[M]) (single 1 (↑n : R)) 1

Tactic:
simp [one_def]

Premises used: MonoidAlgebra.one_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
n : ℕ
⊢ Eq (α := R[M]) (↑n : R[M]) (single 1 (↑n : R))

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
x : R[M]
r : R
m : M
⊢ ∀ m' ∈ x.support, m' * 1 = m ↔ m' = m

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
x : R[M]
r : R
m : M
⊢ ∀ m' ∈ x.support, 1 * m' = m ↔ m' = m

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
inst_2 : Nontrivial R
a b : M
h : Eq (α := R[M]) ((of R M : (a : M) → R[M]) a : R[M]) ((of R M : (a : M) → R[M]) b : R[M])
⊢ a = b

Tactic:
simpa using (single_eq_single_iff _ _ _ _).mp h

Premises used: Finsupp.single_eq_single_iff, Iff.mp
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
m : M
inst_1 : MulOneClass M
h : ∀ (m' : M), Commute m m'
f : R[M]
⊢ Commute ((of R M : (a : M) → R[M]) m) f

Tactic:
single_commute h .one_left f

Premises used: MonoidAlgebra.single_commute, Finsupp.single
-- 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 : MulOneClass M
_a _b : R × M
⊢ single (_a * _b).2 (_a * _b).1 = HMul.hMul (α := R[M]) (single _a.2 _a.1) (single _b.2 _b.1)

Tactic:
simp
-- 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 : MulOneClass M
⊢ ∀ (x y : R),
    ZeroHom.toFun (↑(singleAddHom 1) : ZeroHom R R[M]) (x * y) =
      HMul.hMul (α := R[M]) (ZeroHom.toFun (↑(singleAddHom 1) : ZeroHom R R[M]) x)
        (ZeroHom.toFun (↑(singleAddHom 1) : ZeroHom R R[M]) y)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
inst_2 : Semiring S
f g : R[M] →+* S
h₁ : ∀ (r : R), Eq.{u_2 + 1} (α := S) ((f : (a : R[M]) → S) (single 1 r) : S) ((g : (a : R[M]) → S) (single 1 r) : S)
h_of : ∀ (m : M), Eq.{u_2 + 1} (α := S) ((f : (a : R[M]) → S) (single m 1) : S) ((g : (a : R[M]) → S) (single m 1) : S)
m : M
r : R
⊢ Eq.{u_2 + 1} (α := S)
    (((fun (f : R[M] →+* S) ↦ ((↑f : R[M] →+ S) : R[M] →+ S)) f : (a : M →₀ R) → S) (Finsupp.single m r) : S)
    (((fun (f : R[M] →+* S) ↦ ((↑f : R[M] →+ S) : R[M] →+ S)) g : (a : M →₀ R) → S) (Finsupp.single m r) : S)

Tactic:
simpa [← map_mul] using congr($(h₁ r) * $(h_of m))

Premises used: map_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
inst_2 : Semiring S
f g : R[M] →+* S
h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom
h_of : Eq (α := M →* S) (MonoidHom.comp (↑f : R[M] →* S) (of R M)) (MonoidHom.comp (↑g : R[M] →* S) (of R M))
⊢ ∀ (r : R), Eq.{u_2 + 1} (α := S) ((f : (a : R[M]) → S) (single 1 r) : S) ((g : (a : R[M]) → S) (single 1 r) : S)

Tactic:
simpa [DFunLike.ext_iff] using h₁

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
S : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : MulOneClass M
inst_2 : Semiring S
f g : R[M] →+* S
h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom
h_of : Eq (α := M →* S) (MonoidHom.comp (↑f : R[M] →* S) (of R M)) (MonoidHom.comp (↑g : R[M] →* S) (of R M))
⊢ ∀ (m : M), Eq.{u_2 + 1} (α := S) ((f : (a : R[M]) → S) (single m 1) : S) ((g : (a : R[M]) → S) (single m 1) : S)

Tactic:
simpa [DFunLike.ext_iff] using h_of

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Monoid M
m : M
r : R
⊢ HPow.hPow (α := R[M]) (β := ℕ) (single m r) 0 = single (HPow.hPow (β := ℕ) m 0) (HPow.hPow (β := ℕ) r 0)

Tactic:
simp [one_def]

Premises used: MonoidAlgebra.one_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Monoid M
m : M
r : R
n : ℕ
⊢ HPow.hPow (α := R[M]) (single m r) (n + 1) = single (m ^ (n + 1)) (r ^ (n + 1))

Tactic:
simp [pow_succ, single_pow _ _ n]

Premises used: pow_succ
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Monoid M
p : R[M] → Prop
x : R[M]
hM : ∀ (m : M), p ((of R M : (a : M) → R[M]) m)
hadd : ∀ (x y : R[M]), p x → p y → p (x + y)
hsmul : ∀ (r : R) (x : R[M]), p x → p (r • x)
⊢ p 0

Tactic:
simpa using hsmul 0 (of R M 1) (hM 1)

Premises used: MonoidAlgebra.of, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Monoid M
p : R[M] → Prop
x : R[M]
hM : ∀ (m : M), p ((of R M : (a : M) → R[M]) m)
hadd : ∀ (x y : R[M]), p x → p y → p (x + y)
hsmul : ∀ (r : R) (x : R[M]), p x → p (r • x)
m : M
r : R
⊢ p (Finsupp.single m r)

Tactic:
simpa using hsmul r (of R M m) (hM m)

Premises used: MonoidAlgebra.of, DFunLike.coe
-- 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 : Monoid M
inst_2 : Monoid N
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
⊢ ∀ (a : R), IsUnit (M := R[M]) ((singleOneRingHom : (a : R) → R[M]) a : R[M]) → IsUnit a

Tactic:
simp_rw [isUnit_iff_exists]

Premises used: isUnit_iff_exists
-- 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_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

Tactic:
⟨x 1, ?_, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat, DFunLike.coe
-- 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_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
refine_2 : HMul.hMul (α := R) ((x : (a : M) → R) 1 : R) a = 1
⊢ ∃ (b : R), a * b = 1 ∧ b * a = 1

Tactic:
refine ⟨x 1, ?_, ?_⟩
-- 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_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
⊢ HMul.hMul (β := R) a ((x : (a : M) → R) 1 : R) = 1

Tactic:
simpa [single_one_mul_apply, one_def] using congr($hax 1)

Premises used: MonoidAlgebra.single_one_mul_apply, MonoidAlgebra.one_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_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
⊢ HMul.hMul (α := R) ((x : (a : M) → R) 1 : R) a = 1

Tactic:
simpa [mul_single_one_apply, one_def] using congr($hxa 1)

Premises used: MonoidAlgebra.mul_single_one_apply, MonoidAlgebra.one_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_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)

Tactic:
(mul_apply ..).trans ?_

Premises used: MonoidAlgebra.mul_apply, Eq.trans
-- 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_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 := ⋯ }
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)
⊢ 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)

Tactic:
refine (mul_apply ..).trans ?_

Premises used: MonoidAlgebra.mul_apply, Eq.trans
-- 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_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 := ⋯ }
⊢ (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:
simp [Finsupp.sum_unique, Unique.eq_default, MonoidAlgebra]

Premises used: Finsupp.sum_unique, Unique.eq_default, MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Monoid M
inst_2 : Subsingleton M
r : R
⊢ Eq (α := R[M]) ((RingEquiv.symm (uniqueRingEquiv M) : (a : R) → R[M]) r : R[M]) (single 1 r : R[M])

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Defs
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : Monoid M
inst_2 : Subsingleton M
r : R
m : M
⊢ (((RingEquiv.symm (uniqueRingEquiv M) : (a : R) → R[M]) r : R[M]) : (a : M) → R) m = r

Tactic:
simp [Subsingleton.elim m 1]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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 : Monoid M
inst_2 : Monoid N
f : R[M × N] →+ R[N][M] := AddEquiv.toAddMonoidHom curryAddEquiv
⊢ ∀ {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 _ _
-- 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 : 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)

Tactic:
f.map_mul_iff.2 ?_

Premises used: Iff.mpr, Finsupp.curry, AddMonoidHom.map_mul_iff