-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 :
  (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
    OpenCover.{w, u} ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
fst : (openCoverOfBase 𝒰 f f).I₀
snd :
  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X fst)
    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                  OpenCover.{w, u}
                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
              i) :
          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
      fst)
⊢ Eq (α :=
    (diagonalCover f 𝒰 𝒱).X
        (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
          PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                            (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                          OpenCover.{w, u}
                            (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                              (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                      i) :
                  PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
              i))
          fst snd) ⟶
      X)
    ((diagonalCover f 𝒰 𝒱).f
        (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
          PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                            (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                          OpenCover.{w, u}
                            (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                              (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                      i) :
                  PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
              i))
          fst snd) ≫
      pullback.fst f f)
    (CategoryStruct.comp (Y := pullback f f)
      (pullback.map
        (PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (𝒱
                (Sigma.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                  OpenCover.{w, u}
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                              i) :
                          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                      i))
                  (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                    PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                      ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                              ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                  (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                    OpenCover.{w, u}
                                      (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                        (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                          (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                        (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                          (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                                i) :
                            PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                        i))
                    fst snd))))
            (Sigma.snd (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                  ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                              (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                OpenCover.{w, u}
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                            i) :
                        PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                    i))
                (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                  OpenCover.{w, u}
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                              i) :
                          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                      i))
                  fst snd)).1 ≫
          Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f
            (Sigma.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
              PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                            (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                              OpenCover.{w, u}
                                (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                          i) :
                      PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                  i))
              (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                  ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                              (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                OpenCover.{w, u}
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                            i) :
                        PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                    i))
                fst snd)))
        (PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (𝒱
                (Sigma.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                  OpenCover.{w, u}
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                              i) :
                          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                      i))
                  (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                    PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                      ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                              ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                  (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                    OpenCover.{w, u}
                                      (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                        (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                          (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                        (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                          (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                                i) :
                            PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                        i))
                    fst snd))))
            (Sigma.snd (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                  ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                              (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                OpenCover.{w, u}
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                            i) :
                        PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                    i))
                (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                  OpenCover.{w, u}
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                              i) :
                          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                      i))
                  fst snd)).2 ≫
          Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f
            (Sigma.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
              PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                            (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                              OpenCover.{w, u}
                                (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                          i) :
                      PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                  i))
              (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                  ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                              (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                OpenCover.{w, u}
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                            i) :
                        PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                    i))
                fst snd)))
        f f
        (PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (𝒱
                (Sigma.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                  OpenCover.{w, u}
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                              i) :
                          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                      i))
                  (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                    PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                      ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                              ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                  (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                    OpenCover.{w, u}
                                      (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                        (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                          (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                        (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                          (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                                i) :
                            PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                        i))
                    fst snd))))
            (Sigma.snd (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                  ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                              (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                OpenCover.{w, u}
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                            i) :
                        PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                    i))
                (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                  OpenCover.{w, u}
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                              i) :
                          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                      i))
                  fst snd)).1 ≫
          pullback.fst f
            (𝒰.f
              (Sigma.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                  ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                              (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                OpenCover.{w, u}
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                            i) :
                        PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                    i))
                (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                  OpenCover.{w, u}
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                              i) :
                          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                      i))
                  fst snd))))
        (PreZeroHypercover.f
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (𝒱
                (Sigma.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                  OpenCover.{w, u}
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                              i) :
                          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                      i))
                  (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                    PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                      ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                              ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                  (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                    OpenCover.{w, u}
                                      (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                        (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                          (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                        (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                          (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                                i) :
                            PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                        i))
                    fst snd))))
            (Sigma.snd (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                  ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                              (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                OpenCover.{w, u}
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                            i) :
                        PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                    i))
                (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                  OpenCover.{w, u}
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                              i) :
                          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                      i))
                  fst snd)).2 ≫
          pullback.fst f
            (𝒰.f
              (Sigma.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                  ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                          ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                              (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                OpenCover.{w, u}
                                  (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                            i) :
                        PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                    i))
                (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                    ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                            ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                                (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                                  OpenCover.{w, u}
                                    (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                      (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                      (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                              i) :
                          PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                      i))
                  fst snd))))
        (𝒰.f
          (Sigma.fst (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
            PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
              ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                      ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                          (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                              (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                            OpenCover.{w, u}
                              (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                        i) :
                    PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                i))
            (Sigma.mk (β := fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
              PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (openCoverOfBase 𝒰 f f).X i)
                ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := precoverage IsOpenImmersion)
                        ((fun (i : (openCoverOfBase 𝒰 f f).I₀) ↦
                            (openCoverOfLeftRight (𝒱 i) (𝒱 i) (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
                                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
                              OpenCover.{w, u}
                                (pullback (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i) (Y :=
                                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
                                  (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                                    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i))))
                          i) :
                      PreZeroHypercover.{w, u, u + 1} ((openCoverOfBase 𝒰 f f).X i)))
                  i))
              fst snd)))
        ⋯ ⋯)
      (pullback.fst f f))

Tactic:
simp [diagonalCover, Cover.pullbackHom]

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, AlgebraicGeometry.Scheme.Pullback.diagonalCover