-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
Goal:
R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ CategoryTheory.Functor.map
        ((Under.forget R ⋙
            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)) ⋙
          R.monoidAlgebra)
        f ≫
      Under.homMk
        (ofHom
          (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
            (MonoidHom.id
              (↑(Functor.obj
                    (Under.forget R ⋙
                      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))
                    T) :
                Type u))
            ⋯))
        ⋯ =
    Under.homMk
        (ofHom
          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
            (MonoidHom.id
              (↑(Functor.obj
                    (Under.forget R ⋙
                      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) :
                Type u))
            ⋯))
        ⋯ ≫
      CategoryTheory.Functor.map (𝟭 (Under R)) f
have h : Hom.hom
    (Under.Hom.right
      (CategoryTheory.Functor.map
          ((Under.forget R ⋙
              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)) ⋙
            R.monoidAlgebra)
          f ≫
        Under.homMk
          (ofHom
            (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
              (MonoidHom.id
                (↑(Functor.obj
                      (Under.forget R ⋙
                        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))
                      T) :
                  Type u))
              sorry))
          sorry)) =
  Hom.hom
    (Under.Hom.right
      (Under.homMk
          (ofHom
            (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
              (MonoidHom.id
                (↑(Functor.obj
                      (Under.forget R ⋙
                        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) :
                  Type u))
              sorry))
          sorry ≫
        CategoryTheory.Functor.map (𝟭 (Under R)) f))
Tactic: ext : 2