∀ {I : Type u_1} {C : I → Type u_2} [inst : (i : I) → CategoryTheory.Category.{u_1, u_2} (C i)] {J : Type u_1}
  [inst_1 : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J ((i : I) → C i)}
  (c : (i : I) → CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Pi.eval C i))) (j j' : J) (f : j ⟶ j'),
  (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const J).obj fun i => (c i).pt).map f) fun i =>
      (c i).π.app j') =
    CategoryTheory.CategoryStruct.comp (fun i => (c i).π.app j) (F.map f)