∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (J : CategoryTheory.Limits.MulticospanShape)
  [inst_1 : Unique J.R] {X Y : C} (f g : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl (CategoryTheory.Limits.Fan.mk X fun x => (CategoryTheory.Iso.refl X).hom).pt).hom g =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g).sndPiMapOfIsLimit
        (CategoryTheory.Limits.Fan.mk X fun x => (CategoryTheory.Iso.refl X).hom)
        (CategoryTheory.Limits.Fan.isLimitMkOfUnique (CategoryTheory.Iso.refl Y) J.R))
      (CategoryTheory.Iso.refl (CategoryTheory.Limits.Fan.mk Y fun x => (CategoryTheory.Iso.refl Y).hom).pt).hom