∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} {c : CategoryTheory.Limits.Fan I.left}
  (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d)
  (K : CategoryTheory.Limits.Multifork I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.fstPiMapOfIsLimit c hd) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc K.ι) (I.sndPiMapOfIsLimit c hd)