∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasBiproductsOfShape J C]
  {X Y : CategoryTheory.Functor (CategoryTheory.Discrete J) C} (η : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colim.map η)
      ((CategoryTheory.Limits.Sigma.isoColimit Y).symm ≪≫
          (CategoryTheory.Limits.biproduct.isoCoproduct fun j => Y.obj { as := j }).symm ≪≫
            (CategoryTheory.Limits.biproduct.isoProduct fun j => Y.obj { as := j }) ≪≫
              CategoryTheory.Limits.Pi.isoLimit Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.Sigma.isoColimit X).symm ≪≫
          (CategoryTheory.Limits.biproduct.isoCoproduct fun j => X.obj { as := j }).symm ≪≫
            (CategoryTheory.Limits.biproduct.isoProduct fun j => X.obj { as := j }) ≪≫
              CategoryTheory.Limits.Pi.isoLimit X).hom
      (CategoryTheory.Limits.lim.map η)