∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {A : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_1, u_4} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.MonoidalClosed A] (M : A) (F G : CategoryTheory.Functor Cᵒᵖ A)
  [inst_4 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom A F G] (X : C)
  (f :
    ((CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom A F G).comp
          (CategoryTheory.coyoneda.obj (Opposite.op M))).obj
      (Opposite.op X)),
  (fun g =>
        CategoryTheory.Limits.end_.lift
          (fun j => CategoryTheory.MonoidalClosed.curry (g.app (Opposite.op (CategoryTheory.Over.mk j.hom.unop)))) ⋯)
      ((fun f =>
          {
            app := fun j =>
              CategoryTheory.MonoidalClosed.uncurry
                (CategoryTheory.CategoryStruct.comp f
                  (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ A
                    ((CategoryTheory.Under.forget (Opposite.op X)).comp F)
                    ((CategoryTheory.Under.forget (Opposite.op X)).comp G)
                    (CategoryTheory.Under.mk (Opposite.unop j).hom.op))),
            naturality := ⋯ })
        f) =
    f