∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat}
  (Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) {X Y_1 : J} (f : X ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) X)
      ((F.comp CategoryTheory.Cat.objects).map f) Y =
    CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) Y_1 Y