∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_5, u_6} J] {K : Type u_1} [inst_2 : CategoryTheory.Category.{u_4, u_1} K]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (c : CategoryTheory.Limits.Cone F)
  (t : (k : K) → CategoryTheory.Limits.IsLimit (((CategoryTheory.evaluation K C).obj k).mapCone c))
  (s : CategoryTheory.Limits.Cone F) (j : J),
  CategoryTheory.CategoryStruct.comp
      {
        app := fun k =>
          (t k).lift
            { pt := s.pt.obj k, π := CategoryTheory.Functor.whiskerRight s.π ((CategoryTheory.evaluation K C).obj k) },
        naturality := ⋯ }
      (c.π.app j) =
    s.π.app j