-- 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)) ⟶ Y)
    (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ Iso.hom (pullbackP1Iso 𝒰 f g i) ≫ pullback.snd (𝒰.f i ≫ f) g)
    (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
      CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
        (pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
        (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
          CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
            (pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) (pullback.snd (𝒰.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)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g)
    (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
      CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
        (pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
        (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
          CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
            (pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) (pullback.snd (𝒰.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)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g)
    (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
      CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
        (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.snd (𝒰.f i) s.fst ≫ s.snd))
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)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g)
    (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
      CategoryStruct.comp (Y := pullback s.fst (𝒰.f i))
        (pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯)
        (pullback.fst s.fst (𝒰.f i) ≫ s.snd))
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)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g)
    (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫
      (pullback.fst (m ≫ p1 𝒰 f g) (𝒰.f i) ≫ 𝟙 s.pt) ≫ s.snd)
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)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g)
    (Iso.hom (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m) ≫ pullback.fst (m ≫ p1 𝒰 f g) (𝒰.f i) ≫ s.snd)
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)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g)
    (pullback.fst m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ s.snd)
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.fst m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ m ≫ p2 𝒰 f g)
    (pullback.fst m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ s.snd)
⊢ 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))

Tactic:
simp_rw [Category.assoc, pullbackP1Iso_hom_snd, pullback.lift_snd,
      pullbackSymmetry_hom_comp_snd_assoc, pullback.lift_fst_assoc, Category.comp_id,
      pullbackRightPullbackFstIso_hom_fst_assoc, ← pullback.condition_assoc, h₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.Limits.pullback.lift_snd, AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd, CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc