-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
S : Under R
hf :
  ∀
    (x :
      (↑(Functor.obj
            (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
              CommMonCat.carrier))
            S.right) :
        Type u)),
    Eq (α :=
      (↑(Functor.obj
            (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
              CommMonCat.carrier))
            S.right) :
        Type u))
      ((CommMonCat.Hom.hom
              (CategoryStruct.comp (Y :=
                Functor.obj
                  (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                    CommMonCat.carrier))
                  (of (MonoidAlgebra (↑R : Type u) (↑S.right : Type u))))
                (CommMonCat.ofHom (MonoidAlgebra.of (↑R : Type u) (↑S.right : Type u)))
                (CommMonCat.ofHom
                  (↑(MonoidAlgebra.liftNCRingHom (Hom.hom S.hom) (MonoidHom.id (↑S.right : Type u)) ⋯) :
                    MonoidAlgebra (↑R : Type u) (↑S.right : Type u) →* (↑S.right : Type u)))) :
            (a : (↑((forget₂ CommRingCat CommMonCat).obj S.right) : Type u)) →
              (↑((forget₂ CommRingCat CommMonCat).obj S.right) : Type u))
          x :
        (↑(Functor.obj
              (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                CommMonCat.carrier))
              S.right) :
          Type u))
      ((CommMonCat.Hom.hom
              (𝟙
                (Functor.obj
                  (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                    CommMonCat.carrier))
                  S.right)) :
            (a : (↑((forget₂ CommRingCat CommMonCat).obj S.right) : Type u)) →
              (↑((forget₂ CommRingCat CommMonCat).obj S.right) : Type u))
          x :
        (↑(Functor.obj
              (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                CommMonCat.carrier))
              S.right) :
          Type u))
⊢ CategoryStruct.comp (Y :=
      Functor.obj
        (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
          CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
        (of (MonoidAlgebra (↑R : Type u) (↑S.right : Type u))))
      (CommMonCat.ofHom (MonoidAlgebra.of (↑R : Type u) (↑S.right : Type u)))
      (CommMonCat.ofHom
        (↑(MonoidAlgebra.liftNCRingHom (Hom.hom S.hom) (MonoidHom.id (↑S.right : Type u)) ⋯) :
          MonoidAlgebra (↑R : Type u) (↑S.right : Type u) →* (↑S.right : Type u))) =
    𝟙
      (Functor.obj
        (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
          CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
        S.right)

Tactic:
ext