∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : F.IsEquivalence] [inst_6 : CategoryTheory.MonoidalClosed D] {X Y Z : C} (f : Y ⟶ X ⟹ Z),
  CategoryTheory.MonoidalClosed.uncurry f =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y)
      ((adj.toEquivalence.symm.toAdjunction.homEquiv
            ((F.comp (CategoryTheory.MonoidalCategory.tensorLeft (F.obj X))).obj Y) Z).symm
        (CategoryTheory.MonoidalClosed.uncurry
          ((adj.homEquiv Y (F.obj X ⟹ adj.toEquivalence.symm.inverse.obj Z)).symm f)))