-- 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 (N := R[M]ᵐᵒᵖ)
                    ((AddMonoidHom.comp
                          (AddMonoidHom.comp
                            (AddMonoidHom.compr₂ (P := R[M]ᵐᵒᵖ) AddMonoidHom.mul
                              (AddEquiv.toAddMonoidHom
                                (AddEquiv.trans (AddEquiv.symm opAddEquiv)
                                  (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv)))))
                            (AddEquiv.toAddMonoidHom opAddEquiv))
                          (singleAddHom m) :
                        (a : R) → R[M]ᵐᵒᵖ →+ Rᵐᵒᵖ[Mᵐᵒᵖ])
                      x)
                    (AddEquiv.toAddMonoidHom opAddEquiv))
                  (singleAddHom m_1) :
                (a : R) → Rᵐᵒᵖ[Mᵐᵒᵖ])
              x_1 :
            MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)
    ((((AddMonoidHom.comp
                  (AddMonoidHom.comp (N := R[M]ᵐᵒᵖ)
                    ((AddMonoidHom.comp
                          (AddMonoidHom.comp (N := R[M]ᵐᵒᵖ)
                            (AddMonoidHom.compl₂ (N := MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
                              (AddMonoidHom.comp AddMonoidHom.mul
                                  (AddEquiv.toAddMonoidHom
                                    (AddEquiv.trans (AddEquiv.symm opAddEquiv)
                                      (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv)))) :
                                R[M]ᵐᵒᵖ →+ MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ →+ MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
                              (AddEquiv.toAddMonoidHom
                                  (AddEquiv.trans (AddEquiv.symm opAddEquiv)
                                    (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv))) :
                                (M →₀ R)ᵐᵒᵖ →+ Finsupp.{u_2, u_1} Mᵐᵒᵖ Rᵐᵒᵖ))
                            (AddEquiv.toAddMonoidHom opAddEquiv))
                          (singleAddHom m) :
                        (a : R) → R[M]ᵐᵒᵖ →+ Rᵐᵒᵖ[Mᵐᵒᵖ])
                      x)
                    (AddEquiv.toAddMonoidHom opAddEquiv))
                  (singleAddHom m_1) :
                (a : R) → Rᵐᵒᵖ[Mᵐᵒᵖ])
              x_1 :
            MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ) :
          (a : Mᵐᵒᵖ) → Rᵐᵒᵖ)
        m_2 :
      Rᵐᵒᵖ)
have h : 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: simp only [AddMonoidHom.coe_comp, Function.comp_apply, singleAddHom_apply,
      AddMonoidHom.compr₂_apply, AddMonoidHom.coe_mul, AddMonoidHom.coe_mulLeft,
      AddMonoidHom.compl₂_apply, AddEquiv.toAddMonoidHom_eq_coe,
      AddEquiv.coe_addMonoidHom_trans]