-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
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)))
⊢ 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))) ⋯))
have 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))))
                sorry)) :
          (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))) sorry ≫
                Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g))) sorry)) :
          (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)))
Tactic: apply MonoidAlgebra.ringHom_ext