-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
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))
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))
                        ⋯))
                    ⋯)) :
            (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))
                        ⋯))
                    ⋯ ≫
                  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))
⊢ 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))

Tactic:
apply MonoidAlgebra.ringHom_ext

Premises used: MonoidAlgebra.ringHom_ext