∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).X i =
    CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g