∀ {C : Type u_5} [inst : CategoryTheory.Category.{u_4, u_5} C] {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_1, u_2} A] {S : C} (E : CategoryTheory.PreOneHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} {d : CategoryTheory.Limits.Cofan E.Y'} (hd : CategoryTheory.Limits.IsColimit d)
  (F : CategoryTheory.Functor Cᵒᵖ A)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun i => Opposite.op (E.Y' i)) F],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          (CategoryTheory.Limits.Fan.mk (F.obj (Opposite.op c.pt)) fun i => F.map (c.inj i).op).pt).hom
      (F.map
        (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x =>
            CategoryTheory.CategoryStruct.comp (E.p₂ x.snd) (c.inj x.fst.2)).op) =
    CategoryTheory.CategoryStruct.comp
      ((E.multicospanIndex F).sndPiMapOfIsLimit
        (CategoryTheory.Limits.Fan.mk (F.obj (Opposite.op c.pt)) fun i => F.map (c.inj i).op)
        (CategoryTheory.Limits.isLimitFanMkObjOfIsLimit F (fun i => Opposite.op (E.Y' i)) (fun i => (d.inj i).op)
          (CategoryTheory.Limits.Cofan.IsColimit.op hd)))
      (CategoryTheory.Iso.refl
          (CategoryTheory.Limits.Fan.mk (F.obj (Opposite.op d.pt)) fun i => F.map (d.inj i).op).pt).hom