-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
Goal:
R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ 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))
have h : ∀ (r : (↑R : Type u)),
  Eq (α := (↑(Functor.obj (𝟭 (Under R)) T).right : Type u))
    ((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)) :
          (a : MonoidAlgebra (↑R : Type u) (↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S) : Type u)) →
            (↑((𝟭 (Under R)).obj T).right : Type u))
        (MonoidAlgebra.single 1 r) :
      (↑(Functor.obj (𝟭 (Under R)) T).right : 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))
                      sorry))
                  sorry ≫
                CategoryTheory.Functor.map (𝟭 (Under R)) f)) :
          (a : MonoidAlgebra (↑R : Type u) (↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S) : Type u)) →
            (↑((𝟭 (Under R)).obj T).right : Type u))
        (MonoidAlgebra.single 1 r) :
      (↑(Functor.obj (𝟭 (Under R)) T).right : Type u))
Tactic: apply MonoidAlgebra.ringHom_ext