awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
rw : Membership.mem (γ := Set ↥(Spec R)) Set.univ x
⊢ Membership.mem (γ := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
            PreZeroHypercover (Spec R) }
          1))
      ⇑(PreZeroHypercover.f
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }
          1))
    x
have rw₁ : Epi.{u, u + 1} (X :=
  (↑(toLocallyRingedSpace
          (PreZeroHypercover.X (S := Spec R)
            { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun (r : (↑R : Type u)) ↦
                Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
              PreZeroHypercover (Spec R) }
            1)).toPresheafedSpace :
    TopCat))
  (Y := (↑(Spec R).toPresheafedSpace : TopCat))
  (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Hom.toLRSHom'
        (PreZeroHypercover.f
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }
          1))))
Tactic: rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
⊢ IsTopologicalBasis.{u} (α := ↥X)
    {x : Set ↥X |
      ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
have h_open : ∀ (u : Set ↥X),
  Membership.mem (γ := Set (Set ↥X))
      {x : Set ↥X |
        ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
      u →
    IsOpen u
Tactic: apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
h_open :
  ∀ (u : Set ↥X),
    Membership.mem (γ := Set (Set ↥X))
        {x : Set ↥X |
          ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
        u →
      IsOpen u
⊢ IsTopologicalBasis.{u} (α := ↥X)
    {x : Set ↥X |
      ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
have h_nhds : ∀ (a : ↥X) (u : Set ↥X),
  a ∈ u →
    IsOpen u →
      ∃ (v : Set ↥X),
        Membership.mem (γ := Set (Set ↥X))
            {x : Set ↥X |
              ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
            v ∧
          a ∈ v ∧ v ⊆ u
Tactic: apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
⊢ ∃ (v : Set ↥X),
    Membership.mem (γ := Set (Set ↥X))
        {x : Set ↥X |
          ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
        v ∧
      a ∈ v ∧ v ⊆ U
have h_nhds : ∀ (x : ↥(X.affineCover.X (Cover.idx X.affineCover a))) (e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a),
  ∃ (v : Set ↥X),
    Membership.mem (γ := Set (Set ↥X))
        {x : Set ↥X |
          ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
        v ∧
      a ∈ v ∧ v ⊆ U
Tactic: rcases X.affineCover.covers a with ⟨x, e⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
⊢ x ∈ U'
have rw : ∀ (haU : Membership.mem (α := ↥X) U ((X.affineCover.f (Cover.idx X.affineCover a)) x : ↥X))
  (e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a),
  let U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U;
  x ∈ U'
Tactic: rw [← e] at haU
Cleared hypotheses: haU, e, U'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (hypothesis)
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
⊢ ∃ (v : Set ↥X),
    Membership.mem (γ := Set (Set ↥X))
        {x : Set ↥X |
          ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
        v ∧
      a ∈ v ∧ v ⊆ U
have hxU' : x ∈ U'
Tactic: have hxU' : x ∈ U' := by rw [← e] at haU; exact haU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Open (goal)
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s :
  (↑((fun (x : (↑X.toTopCat : Type u)) ↦
          Classical.choose (p := fun (R : CommRingCat.{u}) ↦
            Nonempty.{u + 1}
              (X.restrict (U :=
                  Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                    (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                            Classical.choose (p := fun (U : OpenNhds x) ↦
                              ∃ (R : CommRingCat.{u}),
                                Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                              ⋯)
                          x) :
                      TopologicalSpace.Opens (↑X.toTopCat : Type u)))
                  (f :=
                  (Opens.inclusion'
                      (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                              Classical.choose (p := fun (U : OpenNhds x) ↦
                                ∃ (R : CommRingCat.{u}),
                                  Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                ⋯)
                            x) :
                        TopologicalSpace.Opens (↑X.toTopCat : Type u)) :
                    Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                        (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                                Classical.choose (p := fun (U : OpenNhds x) ↦
                                  ∃ (R : CommRingCat.{u}),
                                    Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                  ⋯)
                              x) :
                          TopologicalSpace.Opens (↑X.toTopCat : Type u)) ⟶
                      X.toTopCat))
                  ⋯ ≅
                Spec.toLocallyRingedSpace.obj (op R)))
            ⋯)
        (Cover.idx X.affineCover a)) :
    Type u)
hxV :
  x ∈
    (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u)))
hVU :
  (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u))) ⊆
    U'
⊢ Set.image (α := ↥(X.affineCover.X (Cover.idx X.affineCover a))) (⇑(X.affineCover.f (Cover.idx X.affineCover a)))
      (Opens.carrier (PrimeSpectrum.basicOpen s)) ⊆
    U
have h_nhds : Subset (α := Set ↥(X.affineCover.X (Cover.idx X.affineCover a))) (Opens.carrier (PrimeSpectrum.basicOpen s))
  (⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U)
Tactic: rw [Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1}
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
              (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) } ∈
    (precoverage P).coverings W
have rw : (∀ (x : ↥W),
    ∃ (i :
      PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
        { I₀ := 𝒰.I₀,
          X := fun (x : 𝒰.I₀) ↦
            (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
          f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }),
      Membership.mem (γ := Set ↥W)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := 𝒰.I₀,
                X := fun (x : 𝒰.I₀) ↦
                  (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                      (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
                f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
                PreZeroHypercover.{u_1, u, u + 1} W }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := 𝒰.I₀,
                X := fun (x : 𝒰.I₀) ↦
                  (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                      (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
                f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
                PreZeroHypercover.{u_1, u, u + 1} W }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
        { I₀ := 𝒰.I₀,
          X := fun (x : 𝒰.I₀) ↦
            (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
          f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }),
    P
      (PreZeroHypercover.f
        { I₀ := 𝒰.I₀,
          X := fun (x : 𝒰.I₀) ↦
            (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
          f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
          PreZeroHypercover.{u_1, u, u + 1} W }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
x : ↥W
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
hy : ∃ (y : ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)), ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) y = x
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
              (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }),
    Membership.mem (γ := Set ↥W)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                    (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                    (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
      x
have h : Membership.mem (γ := Set ↥W)
  (Set.range (ι :=
    ↥(PreZeroHypercover.X
        { I₀ := 𝒰.I₀,
          X := fun (x : 𝒰.I₀) ↦
            (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
          f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
          PreZeroHypercover.{u_1, u, u + 1} W }
        i))
    ⇑(PreZeroHypercover.f
        { I₀ := 𝒰.I₀,
          X := fun (x : 𝒰.I₀) ↦
            (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
                (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
          f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
          PreZeroHypercover.{u_1, u, u + 1} W }
        i))
  x
Tactic: use i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
            (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
      f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }
⊢ P
    (PreZeroHypercover.f
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
              (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) :
        PreZeroHypercover.{u_1, u, u + 1} W }
      j)
have refine_2 : P (X :=
  (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X j) S) (Z := OverClass.asOver X S) (Hom.asOver f S)
      (Hom.asOver (𝒰.f j) S)).left)
  (Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f j) S)))
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
j :
  PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
    { I₀ := 𝒰.I₀,
      X := fun (x : 𝒰.I₀) ↦
        (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X x) S) (Z := OverClass.asOver X S)
            (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
      f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }
⊢ P (X :=
    (pullback (X := OverClass.asOver W S) (Y := OverClass.asOver (𝒰.X j) S) (Z := OverClass.asOver X S) (Hom.asOver f S)
        (Hom.asOver (𝒰.f j) S)).left)
    (Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f j) S)))
have refine_2 : P (X :=
  pullback (X := Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver W S)) (Y :=
    Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver (𝒰.X j) S)) (Z :=
    Functor.obj (C := Over S) (Over.forget S) (OverClass.asOver X S))
    (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver f S))
    (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver (𝒰.f j) S)))
  (pullback.fst (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver f S))
    (CategoryTheory.Functor.map (Over.forget S) (Hom.asOver (𝒰.f j) S)))
Tactic: rw [← Over.forget_map, ← PreservesPullback.iso_hom_fst, P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1}
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
              (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) } ∈
    (precoverage P).coverings W
have rw : (∀ (x : ↥W),
    ∃ (i :
      PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
        { I₀ := 𝒰.I₀,
          X := fun (x : 𝒰.I₀) ↦
            (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
          f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }),
      Membership.mem (γ := Set ↥W)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := 𝒰.I₀,
                X := fun (x : 𝒰.I₀) ↦
                  (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                      (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
                f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
                PreZeroHypercover.{u_1, u, u + 1} W }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := 𝒰.I₀,
                X := fun (x : 𝒰.I₀) ↦
                  (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                      (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
                f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
                PreZeroHypercover.{u_1, u, u + 1} W }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
        { I₀ := 𝒰.I₀,
          X := fun (x : 𝒰.I₀) ↦
            (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
          f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }),
    P
      (PreZeroHypercover.f
        { I₀ := 𝒰.I₀,
          X := fun (x : 𝒰.I₀) ↦
            (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
          f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
          PreZeroHypercover.{u_1, u, u + 1} W }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Over (goal)
Goal:
P : MorphismProperty Scheme
S : Scheme
inst : P.IsStableUnderBaseChange
inst_1 : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : W ⟶ X
inst_2 : W.Over S
inst_3 : X.Over S
inst_4 : Cover.Over S (P := P) 𝒰
inst_5 : Hom.IsOver f S
x : ↥W
i : (Precoverage.ZeroHypercover.pullback₂ f 𝒰).I₀
hy : ∃ (y : ↥((Precoverage.ZeroHypercover.pullback₂ f 𝒰).X i)), ((Precoverage.ZeroHypercover.pullback₂ f 𝒰).f i) y = x
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := W)
      { I₀ := 𝒰.I₀,
        X := fun (x : 𝒰.I₀) ↦
          (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
              (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
        f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }),
    Membership.mem (γ := Set ↥W)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                    (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := 𝒰.I₀,
              X := fun (x : 𝒰.I₀) ↦
                (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                    (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
              f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
              PreZeroHypercover.{u_1, u, u + 1} W }
            i))
      x
have h : Membership.mem (γ := Set ↥W)
  (Set.range (ι :=
    ↥(PreZeroHypercover.X
        { I₀ := 𝒰.I₀,
          X := fun (x : 𝒰.I₀) ↦
            (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
          f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
          PreZeroHypercover.{u_1, u, u + 1} W }
        i))
    ⇑(PreZeroHypercover.f
        { I₀ := 𝒰.I₀,
          X := fun (x : 𝒰.I₀) ↦
            (pullback (X := OverClass.asOver (𝒰.X x) S) (Y := OverClass.asOver W S) (Z := OverClass.asOver X S)
                (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
          f := fun (x : 𝒰.I₀) ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) :
          PreZeroHypercover.{u_1, u, u + 1} W }
        i))
  x
Tactic: use i