∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C] {J : Type u_1} [inst_3 : CategoryTheory.Category.{u_4, u_1} J]
  [inst_4 :
    ∀ (F₁ F₂ : CategoryTheory.Functor J C), CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom C F₁ F₂]
  {F₁ F₂ F₃ : CategoryTheory.Functor J C} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj F₁ F₂ ⟶ F₃),
  (fun g =>
        {
          app := fun j =>
            CategoryTheory.MonoidalClosed.uncurry
              (CategoryTheory.CategoryStruct.comp (g.app j)
                (CategoryTheory.Enriched.FunctorCategory.enrichedHomπ C ((CategoryTheory.Under.forget j).comp F₁)
                  ((CategoryTheory.Under.forget j).comp F₃)
                  (CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.id j)))),
          naturality := ⋯ })
      ((fun f =>
          {
            app := fun j =>
              CategoryTheory.Limits.end_.lift
                (fun k =>
                  CategoryTheory.CategoryStruct.comp (F₂.map k.hom)
                    (CategoryTheory.MonoidalClosed.curry (f.app k.right)))
                ⋯,
            naturality := ⋯ })
        f) =
    f