-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
Goal:
R : CommRingCat
G : CommMonCat
⊢ 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)
have 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 := sorry }
            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))
                    sorry))
                sorry,
            naturality := sorry }
          (R.monoidAlgebra.obj G)))) =
  Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))
Tactic: ext : 2