-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Opposite (goal)
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ᵐᵒᵖ
⊢ 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ᵐᵒᵖ)
have 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ᵐᵒᵖ)
Tactic: erw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply,
      MulOpposite.opAddEquiv_symm_apply]