∀ {C : Type u_5} [inst : CategoryTheory.Category.{u_4, u_5} C] {α : Type u_2} {I : α → Type u_3}
  [inst_1 : (i : α) → CategoryTheory.Category.{u_1, u_3} (I i)]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (F : (i : α) → CategoryTheory.Functor (I i) C) [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasColimitsOfShape (I i) C]
  ⦃X Y : (i : α) → I i⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pointwiseProduct F).map f)
      (CategoryTheory.Limits.Pi.map fun s => CategoryTheory.Limits.colimit.ι (F s) (Y s)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Pi.map fun s => CategoryTheory.Limits.colimit.ι (F s) (X s))
      (((CategoryTheory.Functor.const ((i : α) → I i)).obj (∏ᶜ fun s => CategoryTheory.Limits.colimit (F s))).map f)