-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰X : OpenCover.{v, u} X
𝒰Y : OpenCover.{w, u} Y
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰X.I₀
j : 𝒰Y.I₀
h₀ :
  Eq (α := pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g)
        (pullback.map (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) f g (𝒰X.f (i, j).1) (𝒰Y.f (i, j).2) (𝟙 Z) ⋯ ⋯)
        (pullback.fst f g) :
      pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g)
        (Iso.hom
            (Iso.refl
              ((fun (ij : Prod.{v, w} 𝒰X.I₀ 𝒰Y.I₀) ↦
                  pullback (X := 𝒰X.X ij.1) (Y := 𝒰Y.X ij.2) (𝒰X.f ij.1 ≫ f) (𝒰Y.f ij.2 ≫ g))
                (i, j))) ≫
          (Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (openCoverOfLeft 𝒰X f g)
                fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦ openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).f
            ((Equiv.symm (Equiv.sigmaEquivProd 𝒰X.I₀ 𝒰Y.I₀) :
                (a : 𝒰X.I₀ × 𝒰Y.I₀) →
                  (Precoverage.ZeroHypercover.bind (openCoverOfLeft 𝒰X f g) fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦
                      openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).I₀)
              (i, j)))
        (pullback.fst f g) :
      pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ X)
h₁ :
  Eq (α := pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback f g)
        (pullback.map (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) f g (𝒰X.f (i, j).1) (𝒰Y.f (i, j).2) (𝟙 Z) ⋯ ⋯)
        (pullback.snd f g) :
      pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback f g)
        (Iso.hom
            (Iso.refl
              ((fun (ij : Prod.{v, w} 𝒰X.I₀ 𝒰Y.I₀) ↦
                  pullback (X := 𝒰X.X ij.1) (Y := 𝒰Y.X ij.2) (𝒰X.f ij.1 ≫ f) (𝒰Y.f ij.2 ≫ g))
                (i, j))) ≫
          (Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (openCoverOfLeft 𝒰X f g)
                fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦ openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).f
            ((Equiv.symm (Equiv.sigmaEquivProd 𝒰X.I₀ 𝒰Y.I₀) :
                (a : 𝒰X.I₀ × 𝒰Y.I₀) →
                  (Precoverage.ZeroHypercover.bind (openCoverOfLeft 𝒰X f g) fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦
                      openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).I₀)
              (i, j)))
        (pullback.snd f g) :
      pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ Y)
⊢ Eq (α := pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ pullback f g)
    (pullback.map (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) f g (𝒰X.f (i, j).1) (𝒰Y.f (i, j).2) (𝟙 Z) ⋯ ⋯ :
      pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ pullback f g)
    (Iso.hom
          (Iso.refl
            ((fun (ij : Prod.{v, w} 𝒰X.I₀ 𝒰Y.I₀) ↦
                pullback (X := 𝒰X.X ij.1) (Y := 𝒰Y.X ij.2) (𝒰X.f ij.1 ≫ f) (𝒰Y.f ij.2 ≫ g))
              (i, j))) ≫
        (Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (openCoverOfLeft 𝒰X f g)
              fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦ openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).f
          ((Equiv.symm (Equiv.sigmaEquivProd 𝒰X.I₀ 𝒰Y.I₀) :
              (a : 𝒰X.I₀ × 𝒰Y.I₀) →
                (Precoverage.ZeroHypercover.bind (openCoverOfLeft 𝒰X f g) fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦
                    openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).I₀)
            (i, j)) :
      pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ pullback f g)

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext