-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
X Y Z : CommMonCat
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (r : (↑R : Type (max u v))),
    Eq (α :=
      (↑(Under.right (X := R)
            (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
              (ofHom MonoidAlgebra.singleOneRingHom))) :
        Type (max u v)))
      ((Hom.hom
              (Under.Hom.right
                (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g))))
                  ⋯)) :
            (a : MonoidAlgebra (↑R : Type (max u v)) (↑X : Type v)) →
              (↑(Under.mk (ofHom MonoidAlgebra.singleOneRingHom)).right : Type (max u v)))
          (MonoidAlgebra.single 1 r) :
        (↑(Under.right (X := R)
              (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
                (ofHom MonoidAlgebra.singleOneRingHom))) :
          Type (max u v)))
      ((Hom.hom
              (Under.Hom.right
                (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) ⋯ ≫
                  Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g)))
                    ⋯)) :
            (a : MonoidAlgebra (↑R : Type (max u v)) (↑X : Type v)) →
              (↑(Under.mk (ofHom MonoidAlgebra.singleOneRingHom)).right : Type (max u v)))
          (MonoidAlgebra.single 1 r) :
        (↑(Under.right (X := R)
              (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
                (ofHom MonoidAlgebra.singleOneRingHom))) :
          Type (max u v)))
h₁ :
  ∀ (m : (↑X : Type v)),
    Eq (α :=
      (↑(Under.right (X := R)
            (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
              (ofHom MonoidAlgebra.singleOneRingHom))) :
        Type (max u v)))
      ((Hom.hom
              (Under.Hom.right
                (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g))))
                  ⋯)) :
            (a : MonoidAlgebra (↑R : Type (max u v)) (↑X : Type v)) →
              (↑(Under.mk (ofHom MonoidAlgebra.singleOneRingHom)).right : Type (max u v)))
          (MonoidAlgebra.single m 1) :
        (↑(Under.right (X := R)
              (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
                (ofHom MonoidAlgebra.singleOneRingHom))) :
          Type (max u v)))
      ((Hom.hom
              (Under.Hom.right
                (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) ⋯ ≫
                  Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g)))
                    ⋯)) :
            (a : MonoidAlgebra (↑R : Type (max u v)) (↑X : Type v)) →
              (↑(Under.mk (ofHom MonoidAlgebra.singleOneRingHom)).right : Type (max u v)))
          (MonoidAlgebra.single m 1) :
        (↑(Under.right (X := R)
              (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
                (ofHom MonoidAlgebra.singleOneRingHom))) :
          Type (max u v)))
⊢ Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) ⋯ ≫
          Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g))) ⋯))

Tactic:
apply MonoidAlgebra.ringHom_ext

Premises used: MonoidAlgebra.ringHom_ext