∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left}
  {hc : CategoryTheory.Limits.IsColimit c} {d : CategoryTheory.Limits.Cofan I.right}
  (a : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc))
  ⦃X Y : CategoryTheory.Limits.WalkingMultispan J⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (I.multispan.map f)
      (match Y with
      | CategoryTheory.Limits.WalkingMultispan.left a_1 =>
        CategoryTheory.CategoryStruct.comp (c.inj a_1)
          (CategoryTheory.CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) a.π)
      | CategoryTheory.Limits.WalkingMultispan.right a_1 => CategoryTheory.CategoryStruct.comp (d.inj a_1) a.π) =
    CategoryTheory.CategoryStruct.comp
      (match X with
      | CategoryTheory.Limits.WalkingMultispan.left a_1 =>
        CategoryTheory.CategoryStruct.comp (c.inj a_1)
          (CategoryTheory.CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) a.π)
      | CategoryTheory.Limits.WalkingMultispan.right a_1 => CategoryTheory.CategoryStruct.comp (d.inj a_1) a.π)
      (((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingMultispan J)).obj a.pt).map f)