∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} J]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} K] {C : Type u_6} [inst_2 : CategoryTheory.Category.{u_5, u_6} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)]
  {x y : J × K} (x_1 : x ⟶ y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.const (J × K)).obj
            (CategoryTheory.Limits.limit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim))).map
        x_1)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) y.1)
        (((CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits (CategoryTheory.Functor.curry.obj G)).obj y.1).π.app
          y.2)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) x.1)
        (((CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits (CategoryTheory.Functor.curry.obj G)).obj x.1).π.app x.2))
      (G.map x_1)