-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Basic (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this_1 : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
    ((fun (i : 𝒰.I₀) ↦
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
          PreZeroHypercover (𝒰.X i)))
      i)
this :
  P (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ Q (X :=
    (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).X
      (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
        PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
          ((fun (i : 𝒰.I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                PreZeroHypercover (𝒰.X i)))
            i))
        i j))
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰.affineRefinement.openCover f
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))
          i j) :
      (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).X
          (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            i j) ⟶
        𝒰.affineRefinement.openCover.X
          (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            i j))
have of_sSup_eq_top : Q (X :=
  PreZeroHypercover.X (S :=
    (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X
      (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
        PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
          ((fun (i : 𝒰.I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                PreZeroHypercover (𝒰.X i)))
            i))
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))
          i j)))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁
          (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f
            (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))
              (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                  ((fun (i : 𝒰.I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                        PreZeroHypercover (𝒰.X i)))
                    i))
                i j)))
          (𝒰.X
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                  ((fun (i : 𝒰.I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                        PreZeroHypercover (𝒰.X i)))
                    i))
                (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                    ((fun (i : 𝒰.I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                          PreZeroHypercover (𝒰.X i)))
                      i))
                  i j))).affineCover) :
      PreZeroHypercover
        ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X
          (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))
              i j))))
    (Sigma.snd (β := fun (i : 𝒰.I₀) ↦
        PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
          ((fun (i : 𝒰.I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                PreZeroHypercover (𝒰.X i)))
            i))
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))
          i j) :
      PreZeroHypercover.I₀ (C := Scheme) (S :=
        𝒰.X
          (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))
              i j)))
        ((fun (i : 𝒰.I₀) ↦
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
              PreZeroHypercover (𝒰.X i)))
          (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))
              i j)))))
  (Scheme.Cover.pullbackHom (P := IsOpenImmersion)
      (𝒰.X
          (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))
              i j))).affineCover
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f
        (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))
          (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            i j)))
      (Sigma.snd (β := fun (i : 𝒰.I₀) ↦
        PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
          ((fun (i : 𝒰.I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                PreZeroHypercover (𝒰.X i)))
            i))
        (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))
          i j)) :
    PreZeroHypercover.X (S :=
        (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X
          (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))
              i j)))
        (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁
              (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f
                (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                    ((fun (i : 𝒰.I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                          PreZeroHypercover (𝒰.X i)))
                      i))
                  (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
                    PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                      ((fun (i : 𝒰.I₀) ↦
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                              ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                            PreZeroHypercover (𝒰.X i)))
                        i))
                    i j)))
              (𝒰.X
                  (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
                    PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                      ((fun (i : 𝒰.I₀) ↦
                          (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                              ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                            PreZeroHypercover (𝒰.X i)))
                        i))
                    (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
                      PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                        ((fun (i : 𝒰.I₀) ↦
                            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                                ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                              PreZeroHypercover (𝒰.X i)))
                          i))
                      i j))).affineCover) :
          PreZeroHypercover
            ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                  ((fun (i : 𝒰.I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                        PreZeroHypercover (𝒰.X i)))
                    i))
                (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                    ((fun (i : 𝒰.I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                          PreZeroHypercover (𝒰.X i)))
                      i))
                  i j))))
        (Sigma.snd (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))
              i j) :
          PreZeroHypercover.I₀ (C := Scheme) (S :=
            𝒰.X
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                  ((fun (i : 𝒰.I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                        PreZeroHypercover (𝒰.X i)))
                    i))
                (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                    ((fun (i : 𝒰.I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                          PreZeroHypercover (𝒰.X i)))
                      i))
                  i j)))
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                  ((fun (i : 𝒰.I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                        PreZeroHypercover (𝒰.X i)))
                    i))
                (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                    ((fun (i : 𝒰.I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                          PreZeroHypercover (𝒰.X i)))
                      i))
                  i j)))) ⟶
      PreZeroHypercover.X (S :=
        𝒰.X
          (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
              PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                ((fun (i : 𝒰.I₀) ↦
                    (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                        ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                      PreZeroHypercover (𝒰.X i)))
                  i))
              i j)))
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (𝒰.X
              (Sigma.fst (β := fun (i : 𝒰.I₀) ↦
                PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                  ((fun (i : 𝒰.I₀) ↦
                      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                          ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                        PreZeroHypercover (𝒰.X i)))
                    i))
                (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
                  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
                    ((fun (i : 𝒰.I₀) ↦
                        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                          PreZeroHypercover (𝒰.X i)))
                      i))
                  i j))).affineCover)
        (Sigma.snd (β := fun (i : 𝒰.I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
            ((fun (i : 𝒰.I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                  PreZeroHypercover (𝒰.X i)))
              i))
          (Sigma.mk (β := fun (i : 𝒰.I₀) ↦
            PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
              ((fun (i : 𝒰.I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
                    PreZeroHypercover (𝒰.X i)))
                i))
            i j)))
Tactic: rw [← Q.cancel_left_of_respectsIso (𝒰.pullbackCoverAffineRefinementObjIso f _).inv,
      𝒰.pullbackCoverAffineRefinementObjIso_inv_pullbackHom]