∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} (E : CategoryTheory.PreZeroHypercover Y) {X Z : C}
  (f : X ⟶ Z) (g : Y ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)]
  (i : E.I₀),
  (E.pullbackCoverOfRight f g).f i =
    CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp (E.f i) g) f g
      (CategoryTheory.CategoryStruct.id X) (E.f i) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯