∀ {J : Type u_5} {K : Type u_6} [inst : CategoryTheory.Category.{u_3, u_5} J]
  [inst_1 : CategoryTheory.Category.{u_4, u_6} K] {C : Type u_2} [inst_2 : CategoryTheory.Category.{u_1, u_2} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCones F}
  (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j))
  {c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.uncurry.obj F)}
  (P : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfConeUncurry Q c))
  (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.uncurry.obj F)) (p : J × K),
  CategoryTheory.CategoryStruct.comp
      (P.lift
        ((fun s =>
            { pt := s.pt,
              π :=
                {
                  app := fun j =>
                    (Q j).lift
                      ((CategoryTheory.Limits.Cones.postcompose
                            ((fun j =>
                                  CategoryTheory.NatIso.ofComponents
                                    (fun x =>
                                      CategoryTheory.Iso.refl
                                        (((CategoryTheory.Prod.sectR j K).comp
                                              (CategoryTheory.Functor.uncurry.obj F)).obj
                                          x))
                                    ⋯)
                                j).hom).obj
                        (CategoryTheory.Limits.Cone.whisker (CategoryTheory.Prod.sectR j K) s)),
                  naturality := ⋯ } })
          s))
      (c.π.app p) =
    s.π.app p