-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.OpenCover.{v, u} Y
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → Scheme.OpenCover.{w, u} (pullback f (𝒰.f i))
inst_2 : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine.{u} ((𝒰' i).X j)
h𝒰' :
  ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀),
    Q (X := pullback ((𝒰' i).f j) ((𝒰' i).f k)) (Y :=
      pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
        ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
this : Q.IsLocal := ⋯
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (Scheme.Pullback.openCoverOfBase 𝒰 f f)
    fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine.{u} (𝒱.X i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀
j k : (𝒰' i).I₀
dsimp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Q (X :=
    (Precoverage.ZeroHypercover.pullback₁ (pullback.diagonal f) 𝒱).X
      (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
        PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase 𝒰 f f).X i)
          ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
                      (Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i))
                          (pullback.snd f (𝒰.f i)) :
                        Scheme.OpenCover.{w, u}
                          (pullback (X := pullback f (𝒰.f i)) (Y := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
                            (pullback.snd f (𝒰.f i)))))
                    i) :
                PreZeroHypercover.{w, u, u + 1} ((Scheme.Pullback.openCoverOfBase 𝒰 f f).X i)))
            i))
        i (j, k)))
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒱 (pullback.diagonal f)
        (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
          PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase 𝒰 f f).X i)
            ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
                        (Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i))
                            (pullback.snd f (𝒰.f i)) :
                          Scheme.OpenCover.{w, u}
                            (pullback (X := pullback f (𝒰.f i)) (Y := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
                              (pullback.snd f (𝒰.f i)))))
                      i) :
                  PreZeroHypercover.{w, u, u + 1} ((Scheme.Pullback.openCoverOfBase 𝒰 f f).X i)))
              i))
          i (j, k)) :
      (Precoverage.ZeroHypercover.pullback₁ (pullback.diagonal f) 𝒱).X
          (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
            PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase 𝒰 f f).X i)
              ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
                          (Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i))
                              (pullback.snd f (𝒰.f i)) :
                            Scheme.OpenCover.{w, u}
                              (pullback (X := pullback f (𝒰.f i)) (Y := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
                                (pullback.snd f (𝒰.f i)))))
                        i) :
                    PreZeroHypercover.{w, u, u + 1} ((Scheme.Pullback.openCoverOfBase 𝒰 f f).X i)))
                i))
            i (j, k)) ⟶
        𝒱.X
          (Sigma.mk (β := fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
            PreZeroHypercover.I₀.{w, u, u + 1} (C := Scheme) (S := (Scheme.Pullback.openCoverOfBase 𝒰 f f).X i)
              ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                      ((fun (i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).I₀) ↦
                          (Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i))
                              (pullback.snd f (𝒰.f i)) :
                            Scheme.OpenCover.{w, u}
                              (pullback (X := pullback f (𝒰.f i)) (Y := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
                                (pullback.snd f (𝒰.f i)))))
                        i) :
                    PreZeroHypercover.{w, u, u + 1} ((Scheme.Pullback.openCoverOfBase 𝒰 f f).X i)))
                i))
            i (j, k)))

Tactic:
dsimp [𝒱]