-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : CommSemiring R
S : Set M
hS : Eq (α := Submonoid M) (closure S) ⊤
m : M
this : Membership.mem (γ := Submonoid M) (closure S) m
m₁ m₂ : M
hx : Membership.mem (γ := Submonoid M) (closure S) m₁
hy : Membership.mem (γ := Submonoid M) (closure S) m₂
P₁ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₁ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₁ :
      R[M])
    ((of R M : (a : M) → R[M]) m₁ : R[M])
P₂ : FreeAlgebra.{u_1, u_2} R (↑S : Type u_2)
hP₂ :
  Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        P₂ :
      R[M])
    ((of R M : (a : M) → R[M]) m₂ : R[M])
rw :
  HMul.hMul (α := R[M]) (β := R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₁ :
        R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₁ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M])
      (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
              fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
            (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
          P₂ :
        R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₂ :
  HMul.hMul (α := R[M]) (β := R[M]) ((of R M : (a : M) → R[M]) m₁ : R[M]) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₃ :
  HMul.hMul (α := R[M]) (β := R[M]) (single m₁ 1) ((of R M : (a : M) → R[M]) m₂ : R[M]) =
    (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₄ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = (of R M : (a : M) → R[M]) (m₁ * m₂)
rw₅ : HMul.hMul (α := R[M]) (single m₁ 1) (single m₂ 1) = single (m₁ * m₂) 1
rw₆ : Eq (α := R[M]) (single (m₁ * m₂) (HMul.hMul (α := R) 1 1)) (single (m₁ * m₂) 1)
rw₇ rw₈ : Eq (α := R[M]) (single (m₁ * m₂) 1) (single (m₁ * m₂) 1)
⊢ Eq (α := R[M])
    (((FreeAlgebra.lift R : (a : (↑S : Type u_2) → R[M]) → FreeAlgebra R (↑S : Type u_2) →ₐ[R] R[M])
            fun (s : (↑S : Type u_2)) ↦ (of R M : (a : M) → R[M]) (↑s : M) :
          (a : FreeAlgebra R (↑S : Type u_2)) → R[M])
        (P₁ * P₂) :
      R[M])
    ((of R M : (a : M) → R[M]) (m₁ * m₂) : R[M])

Tactic:
rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]

Premises used: MonoidAlgebra.single_mul_single, map_mul, one_mul, MonoidAlgebra.of_apply