∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [inst_2 : Small.{v, u₁} J] [inst_3 : Small.{v, u₂} K] (F : CategoryTheory.Functor (J × K) (Type v)) (j : J) (k : K)
  (f :
    ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim).obj k),
  CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj F).comp CategoryTheory.Limits.colim) j
      (CategoryTheory.Limits.colimitLimitToLimitColimit F
        (CategoryTheory.Limits.colimit.ι
          ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).comp CategoryTheory.Limits.lim) k
          f)) =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj F).obj j) k
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp F)).obj k)
        j f)