-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
S T : Under R
f : S ⟶ T
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))
                ⋯))
            ⋯)) =
    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))
                ⋯))
            ⋯ ≫
          CategoryTheory.Functor.map (𝟭 (Under R)) f))
⊢ 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

Tactic:
ext : 2