{J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    {K₁ : CategoryTheory.Functor J₁ C₁} →
                      {K₂ : CategoryTheory.Functor J₂ C₂} →
                        (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                          [CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] →
                            {c₁ : CategoryTheory.Limits.Cone K₁} →
                              CategoryTheory.Limits.IsLimit c₁ →
                                {c₂ : CategoryTheory.Limits.Cone K₂} →
                                  CategoryTheory.Limits.IsLimit c₂ →
                                    {c₃ :
                                        CategoryTheory.Limits.Cone
                                          (CategoryTheory.Functor.uncurry.obj
                                            ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))} →
                                      CategoryTheory.Limits.IsLimit c₃ → ((G.obj c₁.pt).obj c₂.pt ≅ c₃.pt)