-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
G : CommMonCat
h :
  Hom.hom
      (Under.Hom.right
        (CategoryStruct.comp (Y :=
          R.monoidAlgebra.obj
            (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))
              (R.monoidAlgebra.obj G)))
          (R.monoidAlgebra.map
            (NatTrans.app
              { app := fun (G : CommMonCat.{u}) ↦ CommMonCat.ofHom (MonoidAlgebra.of (↑R : Type u) (↑G : Type u)),
                naturality := ⋯ }
              G))
          (NatTrans.app
            {
              app := fun (S : Under R) ↦
                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))
                      ⋯))
                  ⋯,
              naturality := ⋯ }
            (R.monoidAlgebra.obj G)))) =
    Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))
⊢ Eq (α := R.monoidAlgebra.obj G ⟶ R.monoidAlgebra.obj G)
    (CategoryStruct.comp (Y :=
        R.monoidAlgebra.obj
          (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))
            (R.monoidAlgebra.obj G)))
        (R.monoidAlgebra.map
          (NatTrans.app
            { app := fun (G : CommMonCat.{u}) ↦ CommMonCat.ofHom (MonoidAlgebra.of (↑R : Type u) (↑G : Type u)),
              naturality := ⋯ }
            G))
        (NatTrans.app
          {
            app := fun (S : Under R) ↦
              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))
                    ⋯))
                ⋯,
            naturality := ⋯ }
          (R.monoidAlgebra.obj G)) :
      R.monoidAlgebra.obj G ⟶ R.monoidAlgebra.obj G)
    (𝟙 (R.monoidAlgebra.obj G) : R.monoidAlgebra.obj G ⟶ R.monoidAlgebra.obj G)

Tactic:
ext : 2