∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  [inst : P.IsStableUnderBaseChange] (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst_1 : CategoryTheory.Category.{u_3, u_2} 𝒰.I₀] [inst_2 : 𝒰.LocallyDirected] {Y : AlgebraicGeometry.Scheme}
  (f : Y ⟶ X) (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀),
  CategoryTheory.Limits.pullback.map f (𝒰.f i) f (𝒰.f i) (CategoryTheory.CategoryStruct.id Y)
      (𝒰.trans (CategoryTheory.CategoryStruct.id i)) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯ =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)