∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i : 𝒰.I₀),
  AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i =
    {
      hom :=
        CategoryTheory.Limits.pullback.lift
          (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
            (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g))
          ⋯,
      inv :=
        CategoryTheory.Limits.pullback.lift ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i)
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }