∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (d : CategoryTheory.Limits.Cofan I.right) (hc : CategoryTheory.Limits.IsColimit c),
  I.sndSigmaMapOfIsColimit d hc =
    CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i =>
      CategoryTheory.CategoryStruct.comp (I.snd i) (d.inj (J.snd i))