awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰 : Cover K X_1
f : X_1 ⟶ Z
g_1 : Y_1 ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g_1
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
h : R ∈ (precoverage P).coverings X
x : ↥X
hR :
  ∀ (x : forget.obj X),
    ∃ (Y : Scheme.{u}) (f : Y ⟶ X),
      R f ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
          (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map f)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
          x
right : R ∈ P.precoverage.coverings X
Y : Scheme
g : Y ⟶ X
hg : R g
heq :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) (forget.obj X)))
    (Set.range (ι := (fun (X : Type u) ↦ X) (forget.obj Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map g)) :
        (a : (fun (X : Type u) ↦ X) (forget.obj Y)) → (fun (X : Type u) ↦ X) (forget.obj X)))
    x
⊢ ∃ (Y : Scheme.{u}) (g : Y ⟶ X), R g ∧ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥Y) ⇑g) x
have right : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥Y) ⇑g) x
Tactic: use Y, g, hg
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X Y Z : Scheme
𝒰_1 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : JointlySurjective K
𝒰 : Cover.{u_1, u} K X
h : ∀ (j : 𝒰.I₀), Q (𝒰.f j)
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1} 𝒰.toPreZeroHypercover ∈ (precoverage Q).coverings X
have rw : (∀ (x : ↥X), ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x) ∧
  ∀ (i : 𝒰.I₀), Q (𝒰.f i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1} { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X } ∈
    (precoverage P).coverings X
have rw : (∀ (x : ↥X),
    ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
          ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
        x) ∧
  ∀ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    P ({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
⊢ (∀ (x : ↥X),
      ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
            ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
          x) ∧
    ∀ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      P ({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i)
have refine_1 : ∀ (x : ↥X),
  ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
        ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
      x
Tactic: refine ⟨fun x ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
refine_1 :
  ∀ (x : ↥X),
    ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
          ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
        x
⊢ (∀ (x : ↥X),
      ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
            ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
          x) ∧
    ∀ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      P ({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i)
have refine_2 : ∀ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
  P ({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i)
Tactic: refine ⟨fun x ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
x : ↥X
⊢ ∃ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i))
        ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i))
      x
have refine_1 : ∀ (i : 𝒰.I₀) (y : ↥(𝒰.X i)),
  ∃ (i_1 : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (α := ↥X) (γ := Set ↥X)
      (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i_1))
        ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i_1))
      ((𝒰.f i) y : ↥X)
Tactic: obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
i : 𝒰.I₀
y : ↥(𝒰.X i)
⊢ ∃ (i_1 : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (α := ↥X) (γ := Set ↥X)
      (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i_1))
        ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i_1))
      ((𝒰.f i) y : ↥X)
have refine_1 : ∀ (i : J) (y : ↥(𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i))),
  ∃ (i_1 : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (α := ↥X) (γ := Set ↥X)
      (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i_1))
        ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i_1))
      ((𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)) y : ↥X)
Tactic: obtain ⟨i, rfl⟩ := e₁.surjective i
Cleared hypotheses: i, y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
i : J
y : ↥(𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i))
⊢ ∃ (i_1 : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (α := ↥X) (γ := Set ↥X)
      (Set.range (ι := ↥({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.X i_1))
        ⇑({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i_1))
      ((𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)) y : ↥X)
have h₁ : Eq (α := ↥X)
  (({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i) ((e₂ i).inv y : ↥(obj i)) : ↥X)
  ((𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)) y : ↥X)
Tactic: use i, (e₂ i).inv y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
inst_1 : P.RespectsIso
X : Scheme
𝒰 : Cover.{u_2, u} (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : Equiv.{u_1 + 1, u_2 + 1} J 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i)
⊢ ∀ (i : { I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    P ({ I₀ := J, X := obj, f := map : PreZeroHypercover.{u_1, u, u + 1} X }.f i)
have refine_2 : ∀ (i : J), P (X := 𝒰.X ((e₁ : (a : J) → 𝒰.I₀) i)) (𝒰.f ((e₁ : (a : J) → 𝒰.I₀) i))
Tactic: simp_rw [h, MorphismProperty.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰_1 : Cover K X_1
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f_1) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1} (𝒰.add f) ∈ (precoverage P).coverings X
have rw : (∀ (x : ↥X),
    ∃ (i : (𝒰.add f).I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥((𝒰.add f).X i)) ⇑((𝒰.add f).f i)) x) ∧
  ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y_1 Z : Scheme
𝒰_1 : Cover K X_1
f_1 : X_1 ⟶ Z
g : Y_1 ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f_1) g
P Q : MorphismProperty Scheme
X Y : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
f : Y ⟶ X
hf : P f
⊢ (∀ (x : ↥X),
      ∃ (i : (𝒰.add f).I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥((𝒰.add f).X i)) ⇑((𝒰.add f).f i)) x) ∧
    ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)
have refine : ∀ (i : (𝒰.add f).I₀), P ((𝒰.add f).f i)
Tactic: refine ⟨fun x ↦ ⟨some <| 𝒰.idx x, 𝒰.covers x⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1}
      { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X } ∈
    (precoverage P).coverings X
have rw : (∀ (x : ↥X),
    ∃ (i :
      { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
          PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                  PreZeroHypercover.{u_1, u, u + 1} X }.X
              i))
          ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                  PreZeroHypercover.{u_1, u, u + 1} X }.f
              i))
        x) ∧
  ∀
    (i :
      { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
          PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    P
      ({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
            PreZeroHypercover.{u_1, u, u + 1} X }.f
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
⊢ (∀ (x : ↥X),
      ∃ (i :
        { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
            PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                    PreZeroHypercover.{u_1, u, u + 1} X }.X
                i))
            ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                    PreZeroHypercover.{u_1, u, u + 1} X }.f
                i))
          x) ∧
    ∀
      (i :
        { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
            PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
      P
        ({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
              PreZeroHypercover.{u_1, u, u + 1} X }.f
          i)
have refine : ∀ (x : ↥X),
  ∃ (i :
    { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.X
            i))
        ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.f
            i))
      x
Tactic: refine ⟨fun x ↦ ?_, 𝒰.map_prop⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
x : ↥X
⊢ ∃ (i :
    { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.X
            i))
        ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.f
            i))
      x
have obtain : ∀ (y : ↥(Spec (𝒰.X (P := P) (𝒰.idx (P := P) x)))) (hy : (𝒰.f (P := P) (𝒰.idx (P := P) x)) y = x),
  ∃ (i :
    { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.X
            i))
        ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.f
            i))
      x
Tactic: obtain ⟨y, hy⟩ := 𝒰.covers x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
x : ↥X
y : ↥(Spec (𝒰.X (P := P) (𝒰.idx (P := P) x)))
hy : (𝒰.f (P := P) (𝒰.idx (P := P) x)) y = x
⊢ ∃ (i :
    { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.X
            i))
        ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.f
            i))
      x
have w : { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
    PreZeroHypercover.{u_1, u, u + 1} X }.I₀
Tactic: use 𝒰.idx x, y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
x : ↥X
y : ↥(Spec (𝒰.X (P := P) (𝒰.idx (P := P) x)))
hy : (𝒰.f (P := P) (𝒰.idx (P := P) x)) y = x
w :
  { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
      PreZeroHypercover.{u_1, u, u + 1} X }.I₀
⊢ ∃ (i :
    { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.X
            i))
        ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.f
            i))
      x
have w₁ : ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X }.X
    (𝒰.idx (P := P) x))
Tactic: use 𝒰.idx x, y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰_1 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
𝒰 : AffineCover.{u_1, u} P X
x : ↥X
y : ↥(Spec (𝒰.X (P := P) (𝒰.idx (P := P) x)))
hy : (𝒰.f (P := P) (𝒰.idx (P := P) x)) y = x
w :
  { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
      PreZeroHypercover.{u_1, u, u + 1} X }.I₀
w₁ :
  ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
          PreZeroHypercover.{u_1, u, u + 1} X }.X
      (𝒰.idx (P := P) x))
⊢ ∃ (i :
    { I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
        PreZeroHypercover.{u_1, u, u + 1} X }.I₀),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.X
            i))
        ⇑({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) :
                PreZeroHypercover.{u_1, u, u + 1} X }.f
            i))
      x
have h : ({ I₀ := 𝒰.I₀ (P := P), X := fun (j : 𝒰.I₀ (P := P)) ↦ Spec (𝒰.X (P := P) j), f := 𝒰.f (P := P) }.f (𝒰.idx (P := P) x))
    y =
  x
Tactic: use 𝒰.idx x, y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X Y Z : Scheme
𝒰_1 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
𝒰 : Cover.{v, u} (precoverage P) X
⊢ PreZeroHypercover.presieve₀ { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) } ∈
    (precoverage P).coverings X
have rw : (∀ (x : ↥X),
    ∃ (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
    P
      (PreZeroHypercover.f
        { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X Y Z : Scheme
𝒰_1 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰_1.I₀), HasPullback (𝒰_1.f x ≫ f) g
P Q : MorphismProperty Scheme
𝒰 : Cover.{v, u} (precoverage P) X
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
      P
        (PreZeroHypercover.f
          { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } i)
have refine : ∀ (x : ↥X),
  ∃ (i :
    PreZeroHypercover.I₀ (C := Scheme) (S := X)
      { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } i))
        ⇑(PreZeroHypercover.f
            { I₀ := ↥X, X := fun (x : ↥X) ↦ 𝒰.X (𝒰.idx x), f := fun (x : ↥X) ↦ 𝒰.f (𝒰.idx x) : PreZeroHypercover X } i))
      x
Tactic: refine ⟨fun x ↦ ?_, fun i ↦ 𝒰.map_prop _⟩