-- Module: Mathlib.Algebra.MonoidAlgebra.Opposite
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : Mul M
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ᵐᵒᵖ)
⊢ 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ᵐᵒᵖ))

Tactic:
ext