-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
Goal:
R : CommRingCat
S T : Under R
f : S ⟶ T
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))
                        ⋯))
                    ⋯)) :
            (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))
                        ⋯))
                    ⋯ ≫
                  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))
⊢ 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₁ : ∀
  (m :
    (↑(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)),
  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 m 1) :
      (↑(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 m 1) :
      (↑(Functor.obj (𝟭 (Under R)) T).right : Type u))
Tactic: apply MonoidAlgebra.ringHom_ext