-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
Goal:
R : CommRingCat
S : Under R
⊢ 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)
have 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)) sorry) :
                  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))
Tactic: ext