-- 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₀
rw :
  Eq (α :=
    pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ⟶
      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) ⋯ ⋯)
    (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) ⋯ ⋯)))
⊢ Eq (α :=
    pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ⟶
      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) ⋯ ⋯)
    (Iso.hom
        (Iso.refl
          ((fun (i : 𝒰.I₀) ↦
              pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i))
                (pullback.snd g (𝒰.f i)))
            i)) ≫
      (openCoverOfBase' 𝒰 f g).f
        ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀)) (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
            (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
          i))

Tactic:
rw [Iso.refl_hom, Category.id_comp, openCoverOfBase'_f]

Premises used: AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_f, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp