awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰_1 : X.OpenCover
inst : Category.{v_1, ?u.61286} 𝒰_1.I₀
inst_1 : Cover.LocallyDirected.{v_1, u, ?u.61286} (P := IsOpenImmersion) 𝒰_1
𝒰 : OpenCover.{u_1, u} X
inst_2 : Category.{v_2, u_1} 𝒰.I₀
inst_3 : Cover.LocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰
Y : Scheme
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans (P := IsOpenImmersion) 𝒰 hij ≫ g j = g i
i j : 𝒰.I₀
⊢ Eq (α := pullback (𝒰.f i) (𝒰.f j) ⟶ Y) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ g i) (pullback.snd (𝒰.f i) (𝒰.f j) ≫ g j)
have h₁ : ∀ (x : (Cover.intersectionOfLocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰 i j).I₀),
  (Cover.intersectionOfLocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰 i j).f x ≫
      pullback.fst (𝒰.f i) (𝒰.f j) ≫ g i =
    (Cover.intersectionOfLocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰 i j).f x ≫
      pullback.snd (𝒰.f i) (𝒰.f j) ≫ g j
Tactic: apply (𝒰.intersectionOfLocallyDirected i j).hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X_1 : Scheme
𝒰_1 : X_1.OpenCover
inst : Category.{v_1, ?u.66091} 𝒰_1.I₀
inst_1 : Cover.LocallyDirected.{v_1, u, ?u.66091} (P := IsOpenImmersion) 𝒰_1
S : Scheme
X : Over S
𝒰 : OpenCover.{u_1, u} X.left
inst_2 : Category.{v_2, u_1} 𝒰.I₀
inst_3 : Cover.LocallyDirected.{v_2, u, u_1} (P := IsOpenImmersion) 𝒰
Y : Over S
g : (i : 𝒰.I₀) → 𝒰.X i ⟶ Y.left
h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), Cover.trans (P := IsOpenImmersion) 𝒰 hij ≫ g j = g i
w : ∀ (i : 𝒰.I₀), g i ≫ Y.hom = 𝒰.f i ≫ X.hom
⊢ glueMorphismsOfLocallyDirected.{v_2, u, u_1} 𝒰 g ⋯ ≫ Y.hom = X.hom
have h₁ : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ glueMorphismsOfLocallyDirected.{v_2, u, u_1} 𝒰 g sorry ≫ Y.hom = 𝒰.f x ≫ X.hom
Tactic: apply 𝒰.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i : 𝒰.I₀
⊢ IsOpenImmersion.lift (𝒰.f i) (𝒰.f i) ⋯ = 𝟙 (𝒰.X i)
have rw : IsOpenImmersion.lift (𝒰.f i) (𝒰.f i) sorry ≫ 𝒰.f i = 𝟙 (𝒰.X i) ≫ 𝒰.f i
Tactic: rw [← cancel_mono (𝒰.f i)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j k : 𝒰.I₀
hij : i ⟶ j
hjk : j ⟶ k
⊢ IsOpenImmersion.lift (𝒰.f k) (𝒰.f i) ⋯ =
    IsOpenImmersion.lift (𝒰.f j) (𝒰.f i) ⋯ ≫ IsOpenImmersion.lift (𝒰.f k) (𝒰.f j) ⋯
have rw : IsOpenImmersion.lift (𝒰.f k) (𝒰.f i) sorry ≫ 𝒰.f k =
  (IsOpenImmersion.lift (𝒰.f j) (𝒰.f i) sorry ≫ IsOpenImmersion.lift (𝒰.f k) (𝒰.f j) sorry) ≫ 𝒰.f k
Tactic: rw [← cancel_mono (𝒰.f _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (hypothesis)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
⊢ ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x
have this : Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
  ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
Tactic: have : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈
      (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).opensRange := ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
⊢ ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x
have obtain : ∀ (k : 𝒰.I₀)
  (h :
    (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
      Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
  (y : ↥(𝒰.X k)) (hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)),
  ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) sorry) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) sorry) sorry) y = x
Tactic: obtain ⟨k, ⟨k, rfl⟩, ⟨y, hy⟩, h⟩ := TopologicalSpace.Opens.isBasis_iff_nbhd.mp H this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
⊢ ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x
have refine_1 : Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f i)
Tactic: refine ⟨k, homOfLE <| hle.mpr <| le_trans h ?_, homOfLE <| hle.mpr <| le_trans h ?_, y, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
refine_1 :
  Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f i)
⊢ ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x
have refine_2 : Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
Tactic: refine ⟨k, homOfLE <| hle.mpr <| le_trans h ?_, homOfLE <| hle.mpr <| le_trans h ?_, y, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
refine_1 :
  Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f i)
refine_2 :
  Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
⊢ ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x
have refine_3 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine ⟨k, homOfLE <| hle.mpr <| le_trans h ?_, homOfLE <| hle.mpr <| le_trans h ?_, y, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
⊢ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f i)
have refine_1 : 𝒰.f i ''ᵁ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j)) ≤ Hom.opensRange (𝒰.f i)
Tactic: rw [Scheme.Hom.opensRange_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
⊢ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
have refine_2 : 𝒰.f j ''ᵁ Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.snd (𝒰.f i) (𝒰.f j)) ≤ Hom.opensRange (𝒰.f j)
Tactic: simp_rw [pullback.condition, Scheme.Hom.opensRange_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis.{u} (α := ↥X) (Set.range fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this :
  Membership.mem (α := ↥X) (Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i))
    ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
k : 𝒰.I₀
h :
  (fun (i : 𝒰.I₀) ↦ Hom.opensRange (𝒰.f i)) k ≤
    Hom.opensRange (X := pullback (𝒰.f i) (𝒰.f j)) (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : Eq (α := ↥X) ((𝒰.f k) y : ↥X) ((pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x : ↥X)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have refine_3 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).isOpenEmbedding.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
⊢ PreZeroHypercover.presieve₀
      { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
        f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι } ∈
    (precoverage IsOpenImmersion).coverings X
have rw : (∀ (x : ↥X),
    ∃ (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
          f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
              i))
        x) ∧
  ∀
    (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
          f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
    IsOpenImmersion
      (PreZeroHypercover.f
        { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
          f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
        i)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := (↑X.affineOpens : Type u),
                  X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := (↑X.affineOpens : Type u),
                  X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
          i)
have refine : ∀ (x : ↥X),
  ∃ (i :
    PreZeroHypercover.I₀ (C := Scheme) (S := X)
      { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
        f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
      x
Tactic: refine ⟨fun x ↦ ?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
x : ↥X
⊢ ∃ (i :
    PreZeroHypercover.I₀ (C := Scheme) (S := X)
      { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
        f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
      x
have h : Membership.mem (γ := Set ↥X)
  (Set.range (ι :=
    ↥(PreZeroHypercover.X (S := X)
        { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
          f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
        (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
          (sorry.choose (p := fun (U' : TopologicalSpace.Opens ↥X) ↦ U' ∈ X.affineOpens ∧ x ∈ U' ∧ U' ≤ ⊤)) sorry)))
    ⇑(PreZeroHypercover.f
        { I₀ := (↑X.affineOpens : Type u), X := fun (U : (↑X.affineOpens : Type u)) ↦ (↑(↑U : X.Opens) : Scheme),
          f := fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens).ι }
        (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
          (sorry.choose (p := fun (U' : TopologicalSpace.Opens ↥X) ↦ U' ∈ X.affineOpens ∧ x ∈ U' ∧ U' ≤ ⊤)) sorry)))
  x
Tactic: use ⟨(isBasis_iff_nbhd.mp X.isBasis_affineOpens (mem_top x)).choose,
      (isBasis_iff_nbhd.mp X.isBasis_affineOpens (mem_top x)).choose_spec.1⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
i j : X.directedAffineCover.I₀
⊢ i ≤ j ↔ Hom.opensRange (X.directedAffineCover.f i) ≤ Hom.opensRange (X.directedAffineCover.f j)
have simp : i ≤ j ↔ i ≤ j
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.Directed (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
⊢ TopologicalSpace.Opens.IsBasis.{u} (α := ↥X)
    (Set.range fun (i : X.directedAffineCover.I₀) ↦ Hom.opensRange (X.directedAffineCover.f i))
have h : (Set.range fun (i : X.directedAffineCover.I₀) ↦ Hom.opensRange (X.directedAffineCover.f i)) = X.affineOpens
Tactic: convert! X.isBasis_affineOpens
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X : Scheme
inst : JointlySurjective K
𝒰 : Cover.{u_1, u} K X
x : ↥X
⊢ ∃ (i : 𝒰.I₀) (y : ↥(𝒰.X i)), (𝒰.f i) y = x
have obtain : ∀ ⦃Y : Scheme.{u}⦄ (i : 𝒰.I₀) (y : ↥(𝒰.X i)) (hy : (𝒰.f i) y = x), ∃ (i : 𝒰.I₀) (y : ↥(𝒰.X i)), (𝒰.f i) y = x
Tactic: obtain ⟨Y, g, ⟨i⟩, y, hy⟩ := JointlySurjective.exists_eq 𝒰.presieve₀ 𝒰.mem₀ x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
inst : JointlySurjective K
X : Scheme
𝒰 : Cover.{u_1, u} K X
⊢ Eq.{u + 1} (α := Set ↥X) (⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) Set.univ
have rw : ∀ (x : ↥X), Membership.mem (γ := Set ↥X) (⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x
Tactic: rw [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
inst : JointlySurjective K
X : Scheme
𝒰 : Cover.{u_1, u} K X
x : ↥X
⊢ Membership.mem (γ := Set ↥X) (⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x
have rw : ∃ (i : 𝒰.I₀), Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) x
Tactic: rw [Set.mem_iUnion]
-- 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
inst_1 : JointlySurjective K
inst_2 : Nonempty.{u + 1} ↥X
𝒰 : Cover.{u_1, u} K X
⊢ Nonempty.{u_1 + 1} 𝒰.I₀
have obtain : ∀ (i : 𝒰.I₀), (∃ (y : ↥(𝒰.X i)), (𝒰.f i) y = inst_2.some) → Nonempty.{u_1 + 1} 𝒰.I₀
Tactic: obtain ⟨i, _⟩ := 𝒰.exists_eq ‹Nonempty X›.some
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X Y Z : Scheme
𝒰 : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
J : Type u_1
obj : J → Scheme
map : (j : J) → obj j ⟶ X
covers : ∀ (x : ↥X), ∃ (j : J) (y : ↥(obj j)), (map j) y = x
map_prop : ∀ (j : J), P (map j)
⊢ 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 simp_rw : (∀ (x : ↥X), ∃ (i : J) (y : ↥(obj i)), (map i) y = x) ∧ ∀ (i : J), P (map i)
Tactic: simp_rw [presieve₀_mem_precoverage_iff, Set.mem_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (hypothesis)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
P Q : MorphismProperty Scheme
X : Scheme
R : Presieve X
h : R ∈ (precoverage P).coverings X
x : ↥X
hR : R ∈ jointlySurjectivePrecoverage.coverings X
right : R ∈ P.precoverage.coverings X
⊢ ∃ (Y : Scheme.{u}) (g : Y ⟶ X), R g ∧ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥Y) ⇑g) x
have 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
Tactic: rw [jointlySurjectivePrecoverage, Presieve.mem_comap_jointlySurjectivePrecoverage_iff] at hR
Cleared hypotheses: hR, right
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Cover.MorphismProperty (goal)
Goal:
K : Precoverage Scheme
X_1 Y Z : Scheme
𝒰 : Cover K X_1
f : X_1 ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
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.{u}) (g : Y ⟶ X), R g ∧ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥Y) ⇑g) x
have obtain : ∀ (Y : Scheme.{u}) (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
Tactic: obtain ⟨Y, g, hg, heq⟩ := hR x