-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} Z
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
h₀ :
  Eq (α :=
    pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ⟶ X)
    (pullback.fst (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ≫ pullback.fst f (𝒰.f i))
    (pullback.fst
        (pullback.snd f
          (𝒰.f
            (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
              ((Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}) :
                  (a : 𝒰.I₀ × PUnit.{v + 1}) → (openCoverOfBase' 𝒰 f g).I₀)
                (i, PUnit.unit)))))
        (pullback.snd g
          (𝒰.f
            (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
              ((Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}) :
                  (a : 𝒰.I₀ × PUnit.{v + 1}) → (openCoverOfBase' 𝒰 f g).I₀)
                (i, PUnit.unit))))) ≫
      pullback.fst f
        (𝒰.f
          (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
            ((Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}) :
                (a : 𝒰.I₀ × PUnit.{v + 1}) → (openCoverOfBase' 𝒰 f g).I₀)
              (i, PUnit.unit)))))
⊢ Eq (α :=
    pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g)
      (pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i))
        (pullback.fst g (𝒰.f i)) (𝒰.f i) ⋯ ⋯)
      (pullback.fst f g))
    (CategoryStruct.comp (Y := pullback f g)
      (Iso.hom
          (pullbackSymmetry
            (pullback.snd f
              (𝒰.f
                (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                  ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                        (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                      (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                    i))))
            (pullback.snd g
              (𝒰.f
                (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                  ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                        (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                      (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                    i))))) ≫
        CategoryStruct.comp (Y :=
          limit
            (cospan (X :=
              pullback (Y :=
                𝒰.X
                  (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                    ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                          (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                        (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                      i)))
                f
                (𝒰.f
                  (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                    ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                          (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                        (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                      i))))
              (pullback.snd f
                  (𝒰.f
                    (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                      ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                            (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                          (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                        i))) ≫
                𝒰.f
                  (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                    ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                          (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                        (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                      i)))
              g))
          (Iso.inv (limit.isoLimitCone { cone := IsPullback.cone ⋯, isLimit := IsPullback.isLimit ⋯ }))
          (CategoryStruct.comp (Y :=
            pullback (X :=
              pullback (Y :=
                𝒰.X
                  (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                    ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                          (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                        (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                      i)))
                f
                (𝒰.f
                  (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                    ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                          (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                        (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                      i))))
              (pullback.fst f
                  (𝒰.f
                    (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                      ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                            (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                          (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                        i))) ≫
                f)
              g)
            (pullback.map
              (pullback.snd f
                  (𝒰.f
                    (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                      ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                            (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                          (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                        i))) ≫
                𝒰.f
                  (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                    ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                          (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                        (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                      i)))
              g
              (pullback.fst f
                  (𝒰.f
                    (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                      ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                            (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                          (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                        i))) ≫
                f)
              g
              (𝟙
                (pullback (Y :=
                  𝒰.X
                    (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                      ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                            (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                          (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                        i)))
                  f
                  (𝒰.f
                    (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                      ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                            (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                          (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                        i)))))
              (𝟙 Y) (𝟙 Z) ⋯ ⋯)
            (pullback.map
              (pullback.fst f
                  (𝒰.f
                    (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                      ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                            (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                          (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                        i))) ≫
                f)
              g f g
              (pullback.fst f
                (𝒰.f
                  (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
                    ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀))
                          (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
                        (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
                      i))))
              (𝟙 Y) (𝟙 Z) ⋯ ⋯)))
      (pullback.fst f g))

Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Equiv.trans_apply,
      Equiv.prodPUnit_symm_apply, Category.assoc, limit.lift_π_assoc, cospan_left, Category.comp_id,
      limit.isoLimitCone_inv_π_assoc, PullbackCone.π_app_left, IsPullback.cone_fst,
      pullbackSymmetry_hom_comp_snd_assoc, limit.isoLimitCone_inv_π,
      PullbackCone.π_app_right, IsPullback.cone_snd, pullbackSymmetry_hom_comp_fst_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.π_app_right, Equiv.trans_apply, CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.IsPullback.cone_fst, CategoryTheory.Limits.cospan_left, CategoryTheory.Category.comp_id, CategoryTheory.Limits.PullbackCone.π_app_left, CategoryTheory.Limits.limit.isoLimitCone_inv_π_assoc, CategoryTheory.Limits.PullbackCone.mk_pt, Equiv.prodPUnit_symm_apply, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc, CategoryTheory.IsPullback.cone_snd, CategoryTheory.Limits.limit.isoLimitCone_inv_π, CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc, CategoryTheory.Limits.limit.lift_π