∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (𝒱 :
    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover)
  (I : (AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).I₀),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.1) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f I.fst))
      (𝒰.f I.fst) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.1) (CategoryTheory.Limits.pullback.fst f (𝒰.f I.fst))) f