-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Adjunctions (goal)
Goal:
R : CommRingCat
G : CommMonCat
h :
  ∀ (r : (↑R : Type u)),
    Eq (α := (↑(R.monoidAlgebra.obj G).right : Type u))
      (((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)))) :
              (↑(R.monoidAlgebra.obj G).right : Type u) →+* (↑(R.monoidAlgebra.obj G).right : Type u)) :
            (a : MonoidAlgebra (↑R : Type u) (↑G : Type u)) → (↑(R.monoidAlgebra.obj G).right : Type u))
          (MonoidAlgebra.single 1 r) :
        (↑(R.monoidAlgebra.obj G).right : Type u))
      ((Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G))) :
            (a : MonoidAlgebra (↑R : Type u) (↑G : Type u)) → (↑(R.monoidAlgebra.obj G).right : Type u))
          (MonoidAlgebra.single 1 r) :
        (↑(R.monoidAlgebra.obj G).right : Type u))
⊢ 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)))
have h₁ : ∀ (m : (↑G : Type u)),
  Eq (α := (↑(R.monoidAlgebra.obj G).right : Type u))
    (((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)))) :
            (↑(R.monoidAlgebra.obj G).right : Type u) →+* (↑(R.monoidAlgebra.obj G).right : Type u)) :
          (a : MonoidAlgebra (↑R : Type u) (↑G : Type u)) → (↑(R.monoidAlgebra.obj G).right : Type u))
        (MonoidAlgebra.single m 1) :
      (↑(R.monoidAlgebra.obj G).right : Type u))
    ((Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G))) :
          (a : MonoidAlgebra (↑R : Type u) (↑G : Type u)) → (↑(R.monoidAlgebra.obj G).right : Type u))
        (MonoidAlgebra.single m 1) :
      (↑(R.monoidAlgebra.obj G).right : Type u))
Tactic: apply MonoidAlgebra.ringHom_ext