∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  (ij :
    (i :
      (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰) f
          g).I₀) ×
      ((fun i =>
            ((fun i =>
                  AlgebraicGeometry.Scheme.coverOfIsIso
                    (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
                          (CategoryTheory.Limits.pullback.snd g (𝒰.f i))).hom
                      (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv
                        (CategoryTheory.Limits.pullback.map
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.f i)) (𝒰.f i)) g
                          (CategoryTheory.CategoryStruct.comp
                            ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) f)
                          g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.f i)))
                          (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯))))
                i).toPreZeroHypercover)
          i).I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' 𝒰 f g).f ij =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.f ij.fst))
          (CategoryTheory.Limits.pullback.snd g (𝒰.f ij.fst))).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.f ij.fst)) (𝒰.f ij.fst)) g
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) f) g
            (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.f ij.fst)))
            (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
          (CategoryTheory.Limits.pullback.map
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) f) g f g
            (CategoryTheory.Limits.pullback.fst f (𝒰.f ij.fst)) (CategoryTheory.CategoryStruct.id Y)
            (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))