-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
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₀
e_2 :
  pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) =
    pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
      ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
h :
  Eq (α := pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶ (𝒰' i).X j)
    (CategoryStruct.comp (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)))
        (CategoryStruct.comp (Y :=
            pullback (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) (Z :=
              pullback.diagonalObj f) (pullback.diagonal f)
              (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
                ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯))
            (Iso.inv (pullbackDiagonalMapIso f (𝒰.f i) ((𝒰' i).f j) ((𝒰' i).f k)) :
              pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶
                pullback (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)))
                  (Z := pullback.diagonalObj f) (pullback.diagonal f)
                  (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
                    ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯))
            (pullback.snd (pullback.diagonal f)
                (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
                  ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯) :
              pullback (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) (Z :=
                  pullback.diagonalObj f) (pullback.diagonal f)
                  (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
                    ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯) ⟶
                pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) :
          pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶
            pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)))
        (pullback.fst ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) :
          pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) ⟶ (𝒰' i).X j) :
      pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶ (𝒰' i).X j)
    (CategoryStruct.comp (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)))
        (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
        (pullback.fst ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) :
      pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶ (𝒰' i).X j)
⊢ Eq (α :=
    pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶
      pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)))
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) (Z :=
          pullback.diagonalObj f) (pullback.diagonal f)
          (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
            ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIso f (𝒰.f i) ((𝒰' i).f j) ((𝒰' i).f k)) :
          pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶
            pullback (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) (Z :=
              pullback.diagonalObj f) (pullback.diagonal f)
              (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
                ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯))
        (pullback.snd (pullback.diagonal f)
            (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
              ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯) :
          pullback (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) (Z :=
              pullback.diagonalObj f) (pullback.diagonal f)
              (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
                ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯) ⟶
            pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) :
      pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶
        pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)))
    (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) :
      pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶
        pullback ((𝒰' i).f j ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)
          ((𝒰' i).f k ≫ Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
have h₁ : Eq (α := pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶ (𝒰' i).X k)
  (CategoryStruct.comp (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)))
      (CategoryStruct.comp (Y :=
          pullback (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) (Z :=
            pullback.diagonalObj f) (pullback.diagonal f)
            (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
              ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) sorry sorry))
          (Iso.inv (pullbackDiagonalMapIso f (𝒰.f i) ((𝒰' i).f j) ((𝒰' i).f k)) :
            pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶
              pullback (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) (Z :=
                pullback.diagonalObj f) (pullback.diagonal f)
                (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
                  ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) sorry sorry))
          (pullback.snd (pullback.diagonal f)
              (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
                ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) sorry sorry) :
            pullback (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) (Z :=
                pullback.diagonalObj f) (pullback.diagonal f)
                (pullback.map ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) f f
                  ((𝒰' i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) sorry sorry) ⟶
              pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) :
        pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶
          pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)))
      (pullback.snd ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) :
        pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)) ⟶ (𝒰' i).X k) :
    pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶ (𝒰' i).X k)
  (CategoryStruct.comp (Y := pullback ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i)))
      (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))
      (pullback.snd ((𝒰' i).f j ≫ pullback.snd f (𝒰.f i)) ((𝒰' i).f k ≫ pullback.snd f (𝒰.f i))) :
    pullback ((𝒰' i).f j) ((𝒰' i).f k) ⟶ (𝒰' i).X k)
Tactic: ext1