-- 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)
    (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))
h₁ :
  Eq (α :=
    pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ⟶ Y)
    (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.snd 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.snd f g))
⊢ 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) ⋯ ⋯)))

Tactic:
ext : 1