-- 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
⊢ Eq (α := R[M]ᵐᵒᵖ →+ R[M]ᵐᵒᵖ →+ MonoidAlgebra.{u_1, u_2} Rᵐᵒᵖ Mᵐᵒᵖ)
    (AddMonoidHom.compr₂ (P := R[M]ᵐᵒᵖ) AddMonoidHom.mul
      (AddEquiv.toAddMonoidHom
        (AddEquiv.trans (AddEquiv.symm opAddEquiv)
          (AddEquiv.trans (mapRange.addEquiv opAddEquiv) (Finsupp.domCongr opEquiv)))))
    (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ᵐᵒᵖ))
have h : ∀ (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ᵐᵒᵖ)
Tactic: ext