∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w} {I : α → Type u₁}
  [inst_1 : (i : α) → CategoryTheory.Category.{v₁, u₁} (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]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape ((i : α) → I i) C] (k : (i : α) → I i) (s : α) {Z : C}
  (h : CategoryTheory.Limits.colimit (F s) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pointwiseProduct F) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Pi.π (fun s => CategoryTheory.Limits.colimit (F s)) s) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun s => (F s).obj (k s)) s)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F s) (k s)) h)