∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasBiproductsOfShape J C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete J) C),
  CategoryTheory.Limits.HasBiproductsOfShape.colimIsoLim.hom.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.biproduct.ι fun j => X.obj { as := j }))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.biproduct.π fun j => X.obj { as := j }))
          (CategoryTheory.Limits.Pi.isoLimit X).hom))