awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
h₁ : ∀ (m : M), g m 0 = 0
h₂ : ∀ (m : M) (t₁ t₂ : R), g m (t₁ + t₂) = g m t₁ + g m t₂
rw :
  Eq.{u_4 + 1} (α := A) (sum a₁ fun (a : M) (b : R) ↦ sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (a * m₂) (b * r₂)) g)
    (sum a₁ fun (x' : M) (v' : R) ↦
      sum a₂ fun (x : M) (v : R) ↦ HSMul.hSMul (β := A) (v' * v) ((f : (a : M) → A) (x' * x) : A))
⊢ Eq.{u_4 + 1} (α := A)
    (sum (sum a₁ fun (m₁ : M) (r₁ : R) ↦ sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (m₁ * m₂) (r₁ * r₂))
      fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A))
    (sum a₁ fun (x' : M) (v' : R) ↦
      sum a₂ fun (x : M) (v : R) ↦ HSMul.hSMul (β := A) (v' * v) ((f : (a : M) → A) (x' * x) : A))

Tactic:
rw [sum_sum_index h₁ h₂]

Premises used: Finsupp.sum_sum_index
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
h₁ : ∀ (m : M), g m 0 = 0
h₂ : ∀ (m : M) (t₁ t₂ : R), g m (t₁ + t₂) = g m t₁ + g m t₂
e_g :
  Eq (α := M → R → A) (fun (a : M) (b : R) ↦ sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (a * m₂) (b * r₂)) g)
    fun (x' : M) (v' : R) ↦ sum a₂ fun (x : M) (v : R) ↦ HSMul.hSMul (β := A) (v' * v) ((f : (a : M) → A) (x' * x) : A)
⊢ Eq.{u_4 + 1} (α := A) (sum a₁ fun (a : M) (b : R) ↦ sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (a * m₂) (b * r₂)) g)
    (sum a₁ fun (x' : M) (v' : R) ↦
      sum a₂ fun (x : M) (v : R) ↦ HSMul.hSMul (β := A) (v' * v) ((f : (a : M) → A) (x' * x) : A))

Tactic:
congr
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
h₁ : ∀ (m : M), g m 0 = 0
h₂ : ∀ (m : M) (t₁ t₂ : R), g m (t₁ + t₂) = g m t₁ + g m t₂
e_g :
  ∀ (x : M) (x_1 : R),
    sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (x * m₂) (x_1 * r₂)) g =
      sum a₂ fun (x_2 : M) (v : R) ↦ HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A)
⊢ Eq (α := M → R → A) (fun (a : M) (b : R) ↦ sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (a * m₂) (b * r₂)) g)
    fun (x' : M) (v' : R) ↦ sum a₂ fun (x : M) (v : R) ↦ HSMul.hSMul (β := A) (v' * v) ((f : (a : M) → A) (x' * x) : A)

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
h₁ : ∀ (m : M), g m 0 = 0
h₂ : ∀ (m : M) (t₁ t₂ : R), g m (t₁ + t₂) = g m t₁ + g m t₂
x : M
x_1 : R
e_g :
  Eq.{u_4 + 1} (α := A) (sum a₂ fun (a : M) (b : R) ↦ sum (single (x * a) (x_1 * b)) g)
    (sum a₂ fun (x_2 : M) (v : R) ↦ HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A))
⊢ sum (sum a₂ fun (m₂ : M) (r₂ : R) ↦ single (x * m₂) (x_1 * r₂)) g =
    sum a₂ fun (x_2 : M) (v : R) ↦ HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A)

Tactic:
rw [sum_sum_index h₁ h₂]

Premises used: Finsupp.sum_sum_index
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
h₁ : ∀ (m : M), g m 0 = 0
h₂ : ∀ (m : M) (t₁ t₂ : R), g m (t₁ + t₂) = g m t₁ + g m t₂
x : M
x_1 : R
e_g :
  Eq (α := M → R → A) (fun (a : M) (b : R) ↦ sum (single (x * a) (x_1 * b)) g) fun (x_2 : M) (v : R) ↦
    HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A)
⊢ Eq.{u_4 + 1} (α := A) (sum a₂ fun (a : M) (b : R) ↦ sum (single (x * a) (x_1 * b)) g)
    (sum a₂ fun (x_2 : M) (v : R) ↦ HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A))

Tactic:
congr
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
h₁ : ∀ (m : M), g m 0 = 0
h₂ : ∀ (m : M) (t₁ t₂ : R), g m (t₁ + t₂) = g m t₁ + g m t₂
x : M
x_1 : R
e_g :
  ∀ (x_2 : M) (x_3 : R),
    sum (single (x * x_2) (x_1 * x_3)) g = HSMul.hSMul (β := A) (x_1 * x_3) ((f : (a : M) → A) (x * x_2) : A)
⊢ Eq (α := M → R → A) (fun (a : M) (b : R) ↦ sum (single (x * a) (x_1 * b)) g) fun (x_2 : M) (v : R) ↦
    HSMul.hSMul (β := A) (x_1 * v) ((f : (a : M) → A) (x * x_2) : A)

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
a₁ a₂ : R[M]
g : M → R → A := fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A)
h₁ : ∀ (m : M), g m 0 = 0
h₂ : ∀ (m : M) (t₁ t₂ : R), g m (t₁ + t₂) = g m t₁ + g m t₂
x : M
x_1 : R
x_2 : M
x_3 : R
e_g e_g₁ : g (x * x_2) (x_1 * x_3) = HSMul.hSMul (β := A) (x_1 * x_3) ((f : (a : M) → A) (x * x_2) : A)
⊢ sum (single (x * x_2) (x_1 * x_3)) g = HSMul.hSMul (β := A) (x_1 * x_3) ((f : (a : M) → A) (x * x_2) : A)

Tactic:
rw [sum_single_index (h₁ _)]

Premises used: MonoidAlgebra.sum_single_index
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
h :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := A)
      (((fun (F : R[M] →ₙₐ[R] A) ↦ F.toMulHom.comp (ofMagma R M))
              ((fun (f : M →ₙ* A) ↦
                  let __src : (M →₀ R) →+ A :=
                    (liftAddHom : (a : M → R →+ A) → (M →₀ R) →+ A) fun (x : M) ↦
                      (AddMonoidHom.flip (smulAddHom R A) : (a : A) → R →+ A) ((f : (a : M) → A) x);
                  ({
                      toFun := fun (a : R[M]) ↦
                        sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A),
                      map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ } :
                    R[M] →ₙₐ[R] A))
                f) :
            (a : M) → A)
          x :
        A)
      ((f : (a : M) → A) x : A)
⊢ (fun (F : R[M] →ₙₐ[R] A) ↦ F.toMulHom.comp (ofMagma R M))
      ((fun (f : M →ₙ* A) ↦
          let __src : (M →₀ R) →+ A :=
            (liftAddHom : (a : M → R →+ A) → (M →₀ R) →+ A) fun (x : M) ↦
              (AddMonoidHom.flip (smulAddHom R A) : (a : A) → R →+ A) ((f : (a : M) → A) x);
          ({ toFun := fun (a : R[M]) ↦ sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A),
              map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ } :
            R[M] →ₙₐ[R] A))
        f) =
    f

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
f : M →ₙ* A
x : M
⊢ Eq.{u_4 + 1} (α := A)
    (((fun (F : R[M] →ₙₐ[R] A) ↦ F.toMulHom.comp (ofMagma R M))
            ((fun (f : M →ₙ* A) ↦
                let __src : (M →₀ R) →+ A :=
                  (liftAddHom : (a : M → R →+ A) → (M →₀ R) →+ A) fun (x : M) ↦
                    (AddMonoidHom.flip (smulAddHom R A) : (a : A) → R →+ A) ((f : (a : M) → A) x);
                ({
                    toFun := fun (a : R[M]) ↦
                      sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A),
                    map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ } :
                  R[M] →ₙₐ[R] A))
              f) :
          (a : M) → A)
        x :
      A)
    ((f : (a : M) → A) x : A)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
F : R[M] →ₙₐ[R] A
h :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := A)
      ((MulHom.comp (N := R[M])
              (NonUnitalAlgHom.toMulHom (R := R) (S := R) (φ := MonoidHom.id R)
                ((fun (f : M →ₙ* A) ↦
                    let __src : (M →₀ R) →+ A :=
                      (liftAddHom : (a : M → R →+ A) → (M →₀ R) →+ A) fun (x : M) ↦
                        (AddMonoidHom.flip (smulAddHom R A) : (a : A) → R →+ A) ((f : (a : M) → A) x);
                    ({
                        toFun := fun (a : R[M]) ↦
                          sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A),
                        map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ } :
                      R[M] →ₙₐ[R] A))
                  ((fun (F : R[M] →ₙₐ[R] A) ↦ F.toMulHom.comp (ofMagma R M)) F)))
              (ofMagma R M) :
            (a : M) → A)
          x :
        A)
      ((F.toMulHom.comp (ofMagma R M) : (a : M) → A) x : A)
⊢ (fun (f : M →ₙ* A) ↦
        let __src : (M →₀ R) →+ A :=
          (liftAddHom : (a : M → R →+ A) → (M →₀ R) →+ A) fun (x : M) ↦
            (AddMonoidHom.flip (smulAddHom R A) : (a : A) → R →+ A) ((f : (a : M) → A) x);
        ({ toFun := fun (a : R[M]) ↦ sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A),
            map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ } :
          R[M] →ₙₐ[R] A))
      ((fun (F : R[M] →ₙₐ[R] A) ↦ F.toMulHom.comp (ofMagma R M)) F) =
    F

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : Semiring R
inst_1 : Mul M
inst_2 : NonUnitalNonAssocSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
F : R[M] →ₙₐ[R] A
x : M
⊢ Eq.{u_4 + 1} (α := A)
    ((MulHom.comp (N := R[M])
            (NonUnitalAlgHom.toMulHom (R := R) (S := R) (φ := MonoidHom.id R)
              ((fun (f : M →ₙ* A) ↦
                  let __src : (M →₀ R) →+ A :=
                    (liftAddHom : (a : M → R →+ A) → (M →₀ R) →+ A) fun (x : M) ↦
                      (AddMonoidHom.flip (smulAddHom R A) : (a : A) → R →+ A) ((f : (a : M) → A) x);
                  ({
                      toFun := fun (a : R[M]) ↦
                        sum a fun (m : M) (t : R) ↦ HSMul.hSMul (β := A) t ((f : (a : M) → A) m : A),
                      map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ } :
                    R[M] →ₙₐ[R] A))
                ((fun (F : R[M] →ₙₐ[R] A) ↦ F.toMulHom.comp (ofMagma R M)) F)))
            (ofMagma R M) :
          (a : M) → A)
        x :
      A)
    ((F.toMulHom.comp (ofMagma R M) : (a : M) → A) x : A)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
f : A[M]
hfg :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := A)
      ((HMul.hMul (α := A[M])
              (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M]) f :
            (a : M) → A)
          m :
        A)
      ((HMul.hMul (β := A[M]) f
              (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M]) :
            (a : M) → A)
          m :
        A)
⊢ HMul.hMul (α := A[M]) (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M]) f =
    HMul.hMul (β := A[M]) f (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M])

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
f : A[M]
m : M
hfg :
  Eq.{u_4 + 1} (α := A)
    ((HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) f : (a : M) → A) m : A)
    ((HMul.hMul (β := A[M]) f (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m : A)
⊢ Eq.{u_4 + 1} (α := A)
    ((HMul.hMul (α := A[M]) (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M])
            f :
          (a : M) → A)
        m :
      A)
    ((HMul.hMul (β := A[M]) f
            (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M]) :
          (a : M) → A)
        m :
      A)

Tactic:
dsimp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
f : A[M]
m : M
hfg :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((f : (a : M) → A) m : A) =
    (HMul.hMul (β := A[M]) f (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m
hfg₁ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((f : (a : M) → A) m : A) =
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((algebraMap R A : (a : R) → A) r : A)
hfg₂ hfg₃ :
  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((algebraMap R A : (a : R) → A) r : A) =
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((algebraMap R A : (a : R) → A) r : A)
⊢ Eq.{u_4 + 1} (α := A)
    ((HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) f : (a : M) → A) m : A)
    ((HMul.hMul (β := A[M]) f (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m : A)

Tactic:
rw [single_one_mul_apply, mul_single_one_apply, Algebra.commutes]

Premises used: MonoidAlgebra.single_one_mul_apply, MonoidAlgebra.mul_single_one_apply, Algebra.commutes
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
a : A[M]
hfg :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := A) ((r • a : (a : M) → A) m : A)
      ((HMul.hMul (α := A[M])
              (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M]) a :
            (a : M) → A)
          m :
        A)
⊢ r • a =
    HMul.hMul (α := A[M]) (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M]) a

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
a : A[M]
m : M
hfg :
  HSMul.hSMul (β := A) r ((a : (a : M) → A) m : A) =
    (HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) a : (a : M) → A) m
⊢ Eq.{u_4 + 1} (α := A) ((r • a : (a : M) → A) m : A)
    ((HMul.hMul (α := A[M]) (((RingHom.comp singleOneRingHom (algebraMap R A) : R →+* A[M]) : (a : R) → A[M]) r : A[M])
            a :
          (a : M) → A)
        m :
      A)

Tactic:
dsimp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
a : A[M]
m : M
hfg :
  HSMul.hSMul (β := A) r ((a : (a : M) → A) m : A) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((a : (a : M) → A) m : A)
hfg₁ hfg₂ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((a : (a : M) → A) m : A) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((a : (a : M) → A) m : A)
⊢ HSMul.hSMul (β := A) r ((a : (a : M) → A) m : A) =
    (HMul.hMul (α := A[M]) (single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) a : (a : M) → A) m

Tactic:
rw [single_one_mul_apply, Algebra.smul_def]

Premises used: MonoidAlgebra.single_one_mul_apply, Algebra.smul_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
hfg :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := A)
      (((OneHom.toFun (↑(↑singleOneRingHom : A →* A[M]) : OneHom A A[M]) ((algebraMap R A : (a : R) → A) r) : A[M]) :
            (a : M) → A)
          m :
        A)
      ((((algebraMap R A[M] : (a : R) → A[M]) r : A[M]) : (a : M) → A) m : A)
⊢ Eq (α := A[M])
    (OneHom.toFun (↑(↑singleOneRingHom : A →* A[M]) : OneHom A A[M]) ((algebraMap R A : (a : R) → A) r) : A[M])
    ((algebraMap R A[M] : (a : R) → A[M]) r : A[M])

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
m : M
hfg :
  Eq.{u_4 + 1} (α := A) (((single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m : A)
    ((((algebraMap R A[M] : (a : R) → A[M]) r : A[M]) : (a : M) → A) m : A)
⊢ Eq.{u_4 + 1} (α := A)
    (((OneHom.toFun (↑(↑singleOneRingHom : A →* A[M]) : OneHom A A[M]) ((algebraMap R A : (a : R) → A) r) : A[M]) :
          (a : M) → A)
        m :
      A)
    ((((algebraMap R A[M] : (a : R) → A[M]) r : A[M]) : (a : M) → A) m : A)

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
m : M
⊢ Eq.{u_4 + 1} (α := A) (((single 1 ((algebraMap R A : (a : R) → A) r) : A[M]) : (a : M) → A) m : A)
    ((((algebraMap R A[M] : (a : R) → A[M]) r : A[M]) : (a : M) → A) m : A)

Tactic:
rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
⊢ Eq (α := (a : R) → A[M]) (⇑(algebraMap R A[M]) : (a : R) → A[M]) (single 1 ∘ (⇑(algebraMap R A) : (a : R) → A))

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
M : Type u_7
inst : CommSemiring R
inst_1 : Monoid M
m : M
r : R
⊢ single m r =
    HMul.hMul (α := R[M]) (β := R[M]) ((algebraMap R R[M] : (a : R) → R[M]) r : R[M])
      ((of R M : (a : M) → R[M]) m : R[M])

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
m : M
r : R
⊢ single m ((algebraMap R A : (a : R) → A) r) =
    HMul.hMul (α := A[M]) (β := A[M]) ((algebraMap R A[M] : (a : R) → A[M]) r : A[M])
      ((of A M : (a : M) → A[M]) m : A[M])

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Unique M
r : R
⊢ Eq.{u_4 + 1} (α := A)
    (Equiv.toFun (α := A[M]) (RingEquiv.toEquiv (uniqueRingEquiv M)) ((algebraMap R A[M] : (a : R) → A[M]) r) : A)
    ((algebraMap R A : (a : R) → A) r : A)

Tactic:
simp [Unique.eq_default]

Premises used: Unique.eq_default
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Unique M
⊢ Eq (α := A[M] ≃+* A) (↑(uniqueAlgEquiv R M) : A[M] ≃+* A) (uniqueRingEquiv M)

Tactic:
rfl

Premises used: MonoidAlgebra.uniqueRingEquiv, RingEquivClass.toRingEquiv, MonoidAlgebra, Finsupp.uniqueEquiv, EquivLike.toEquiv, rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
A : Type u_4
M : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Unique M
⊢ Eq (α := A ≃+* A[M]) (↑(AlgEquiv.symm (uniqueAlgEquiv R M)) : A ≃+* A[M]) (RingEquiv.symm (uniqueRingEquiv M))

Tactic:
rfl

Premises used: RingEquivClass.toRingEquiv, MonoidAlgebra, Equiv.symm, EquivLike.toEquiv, RingEquiv.symm, rfl, Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
hfg :
  ∀ (m : M) (m_1 : N),
    Eq.{u_4 + 1} (α := A)
      ((((Equiv.toFun (RingEquiv.toEquiv curryRingEquiv) ((algebraMap R A[M × N] : (a : R) → A[M × N]) r) :
                  (a : M) → A[N])
                m :
              A[N]) :
            (a : N) → A)
          m_1 :
        A)
      ((((((algebraMap R A[N][M] : (a : R) → A[N][M]) r : A[N][M]) : (a : M) → A[N]) m : A[N]) : (a : N) → A) m_1 : A)
⊢ Eq (α := A[N][M]) (Equiv.toFun (RingEquiv.toEquiv curryRingEquiv) ((algebraMap R A[M × N] : (a : R) → A[M × N]) r))
    ((algebraMap R A[N][M] : (a : R) → A[N][M]) r)

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Monoid M
inst_4 : Monoid N
r : R
m : M
m_1 : N
⊢ Eq.{u_4 + 1} (α := A)
    ((((Equiv.toFun (RingEquiv.toEquiv curryRingEquiv) ((algebraMap R A[M × N] : (a : R) → A[M × N]) r) :
                (a : M) → A[N])
              m :
            A[N]) :
          (a : N) → A)
        m_1 :
      A)
    ((((((algebraMap R A[N][M] : (a : R) → A[N][M]) r : A[N][M]) : (a : M) → A[N]) m : A[N]) : (a : N) → A) m_1 : A)

Tactic:
simp [MonoidAlgebra, algebraMap, Algebra.algebraMap, singleOneRingHom, curryRingEquiv,
      EquivLike.toEquiv, singleAddHom, curryAddEquiv]

Premises used: Algebra.algebraMap, MonoidAlgebra.singleAddHom, Finsupp.curryAddEquiv, MonoidAlgebra.curryRingEquiv, MonoidAlgebra, MonoidAlgebra.singleOneRingHom, EquivLike.toEquiv