∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type w}
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) {J : Finset (CategoryTheory.Discrete α)} (j : ↥J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => F.obj ↑x) j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj F) J)
        (CategoryTheory.Limits.colimit.isoColimitCocone
            (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone F)).inv) =
    CategoryTheory.Limits.colimit.ι F ↑j