-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 :
  (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
    OpenCover.{w, u} ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
I : (diagonalCover f 𝒰 𝒱).I₀
⊢ (diagonalCover f 𝒰 𝒱).f I =
    pullback.map
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒱
              (I.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)))))
          I.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)).1 ≫
        Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f
          (I.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))))
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒱
              (I.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)))))
          I.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)).2 ≫
        Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f
          (I.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))))
      f f
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒱
              (I.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)))))
          I.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)).1 ≫
        pullback.fst f
          (𝒰.f
            (I.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)))))
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (𝒱
              (I.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)))))
          I.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)).2 ≫
        pullback.fst f
          (𝒰.f
            (I.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)))))
      (𝒰.f
        (I.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))))
      ⋯ ⋯
have mk : ∀ (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) ⟶
      pullback.diagonalObj f)
    ((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.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)))
      sorry sorry)
Tactic: cases I
Cleared hypotheses: I