-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s_1 s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (W := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
create :
  Eq (α :=
    pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶ 𝒰.X i)
    ((pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i)) ≫ pullback.fst (𝒰.f i ≫ f) g)
    (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (CategoryStruct.comp (Y := pullback (𝒰.f i) s.fst)
        (CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
            (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
              pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
            (Iso.hom (pullbackSymmetry s.fst (𝒰.f i))) :
          pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
            pullback (𝒰.f i) s.fst)
        (pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ :
          pullback (𝒰.f i) s.fst ⟶ pullback (𝒰.f i ≫ f) g))
      (pullback.fst (𝒰.f i ≫ f) g))
create₁ :
  Eq (α :=
    pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶ Y)
    ((pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i)) ≫ pullback.snd (𝒰.f i ≫ f) g)
    (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (CategoryStruct.comp (Y := pullback (𝒰.f i) s.fst)
        (CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
            (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
              pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
            (Iso.hom (pullbackSymmetry s.fst (𝒰.f i))) :
          pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
            pullback (𝒰.f i) s.fst)
        (pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ :
          pullback (𝒰.f i) s.fst ⟶ pullback (𝒰.f i ≫ f) g))
      (pullback.snd (𝒰.f i ≫ f) g))
⊢ Eq (α :=
    pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
      pullback (𝒰.f i ≫ f) g)
    (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i))
    (CategoryStruct.comp (Y := pullback (𝒰.f i) s.fst)
      (CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
          (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
            pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
          (Iso.hom (pullbackSymmetry s.fst (𝒰.f i))) :
        pullback (Y := pullback (X := (gluing 𝒰 f g).glued) (p1 𝒰 f g) (𝒰.f i)) m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ⟶
          pullback (𝒰.f i) s.fst)
      (pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ :
        pullback (𝒰.f i) s.fst ⟶ pullback (𝒰.f i ≫ f) g))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext