-- Module: Mathlib.Algebra.MonoidAlgebra.Opposite
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : Mul M
m : M
x : R
m_1 : M
x_1 : R
m_2 : Mᵐᵒᵖ
h :
  Eq.{u_1 + 1} (α := Rᵐᵒᵖ)
    ((((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (unop
                  (HMul.hMul (α := R[M]ᵐᵒᵖ) (β := R[M]ᵐᵒᵖ)
                    (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m x) : R[M]ᵐᵒᵖ)
                    (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m_1 x_1) : R[M]ᵐᵒᵖ)))) :
            Finsupp.{u_2, u_1} Mᵐᵒᵖ Rᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)
    ((HMul.hMul (α := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
            ((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m x)))))
            ((Finsupp.domCongr opEquiv : (a : M →₀ Rᵐᵒᵖ) → Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
              ((mapRange.addEquiv opAddEquiv : (a : M →₀ R) → M →₀ Rᵐᵒᵖ)
                (unop (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m_1 x_1))))) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)
⊢ Eq.{u_1 + 1} (α := Rᵐᵒᵖ)
    ((((AddMonoidHom.comp
                  (AddMonoidHom.comp (↑(Finsupp.domCongr opEquiv) : (M →₀ Rᵐᵒᵖ) →+ Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
                    (↑(mapRange.addEquiv opAddEquiv) : (M →₀ R) →+ M →₀ Rᵐᵒᵖ))
                  (↑(AddEquiv.symm opAddEquiv) : (M →₀ R)ᵐᵒᵖ →+ M →₀ R) :
                (a : R[M]ᵐᵒᵖ) → Rᵐᵒᵖ[Mᵐᵒᵖ])
              (HMul.hMul (α := R[M]ᵐᵒᵖ) (β := R[M]ᵐᵒᵖ)
                (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m x) : R[M]ᵐᵒᵖ)
                (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m_1 x_1) : R[M]ᵐᵒᵖ)) :
            MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)
    ((HMul.hMul (α := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ) (β := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
            ((AddMonoidHom.comp
                    (AddMonoidHom.comp (↑(Finsupp.domCongr opEquiv) : (M →₀ Rᵐᵒᵖ) →+ Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
                      (↑(mapRange.addEquiv opAddEquiv) : (M →₀ R) →+ M →₀ Rᵐᵒᵖ))
                    (↑(AddEquiv.symm opAddEquiv) : (M →₀ R)ᵐᵒᵖ →+ M →₀ R) :
                  (a : R[M]ᵐᵒᵖ) → Rᵐᵒᵖ[Mᵐᵒᵖ])
                (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m x)) :
              MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
            ((AddMonoidHom.comp
                    (AddMonoidHom.comp (↑(Finsupp.domCongr opEquiv) : (M →₀ Rᵐᵒᵖ) →+ Mᵐᵒᵖ →₀ Rᵐᵒᵖ)
                      (↑(mapRange.addEquiv opAddEquiv) : (M →₀ R) →+ M →₀ Rᵐᵒᵖ))
                    (↑(AddEquiv.symm opAddEquiv) : (M →₀ R)ᵐᵒᵖ →+ M →₀ R) :
                  (a : R[M]ᵐᵒᵖ) → Rᵐᵒᵖ[Mᵐᵒᵖ])
                (((↑opAddEquiv : R[M] →+ R[M]ᵐᵒᵖ) : (a : R[M]) → R[M]ᵐᵒᵖ) (single m_1 x_1)) :
              MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)

Tactic:
erw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply,
      MulOpposite.opAddEquiv_symm_apply]

Premises used: AddEquiv.trans_apply, MulOpposite.opAddEquiv_symm_apply