awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
f₂ : (↑Γ(X, U.toOpens) : Type u)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f₂) hW)) : Type u)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : (↑Γ(X, (↑U : X.Opens)) : Type u)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ ∃ f ∈ s,
    ∃ (g : (↑Γ(X, U.toOpens) : Type u)),
      X.basicOpen (f * g) = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f₁) hV)

Tactic:
⟨f₂, hf₂s, f₃, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
f₂ : (↑Γ(X, U.toOpens) : Type u)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f₂) hW)) : Type u)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : (↑Γ(X, (↑U : X.Opens)) : Type u)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
mp : X.basicOpen (f₂ * f₃) = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f₁) hV)
⊢ ∃ f ∈ s,
    ∃ (g : (↑Γ(X, U.toOpens) : Type u)),
      X.basicOpen (f * g) = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f₁) hV)

Tactic:
refine ⟨f₂, hf₂s, f₃, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
f₂ : (↑Γ(X, U.toOpens) : Type u)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f₂) hW)) : Type u)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : (↑Γ(X, (↑U : X.Opens)) : Type u)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
mp : X.basicOpen f₁ ≤ X.basicOpen f₂
⊢ X.basicOpen (f₂ * f₃) = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f₁) hV)

Tactic:
rw [X.basicOpen_mul, hf₃, inf_eq_right]

Premises used: AlgebraicGeometry.Scheme.basicOpen_mul, inf_eq_right
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
f₂ : (↑Γ(X, U.toOpens) : Type u)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f₂) hW)) : Type u)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : (↑Γ(X, (↑U : X.Opens)) : Type u)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ X.basicOpen f₁ ≤ X.basicOpen f₂

Tactic:
X.basicOpen_le _

Premises used: Set.Mem, setOf, AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
f₂ : (↑Γ(X, U.toOpens) : Type u)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : (↑Γ(X, toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f₂) hW)) : Type u)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : (↑Γ(X, (↑U : X.Opens)) : Type u)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ X.basicOpen f₁ ≤ X.basicOpen f₂

Tactic:
exact X.basicOpen_le _

Premises used: AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
f₁ : (↑Γ(X, U.toOpens) : Type u)
hf₁s : f₁ ∈ s
f₂ : (↑Γ(X, U.toOpens) : Type u)
hV : IsAffineOpen (X.basicOpen (f₁ * f₂))
f : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen (f₁ * f₂)) hV ⟶ U
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f

Tactic:
⟨U.basicOpen f₁, ⟨f₂ |_ _, ?_⟩, ⟨f₁, rfl⟩, ⟨f₁, hf₁s, rfl⟩, rfl⟩

Premises used: TopCat.Presheaf.restrictOpen, PLift.up, AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen, And.intro, Exists.intro, ULift.up, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
f₁ : (↑Γ(X, U.toOpens) : Type u)
hf₁s : f₁ ∈ s
f₂ : (↑Γ(X, U.toOpens) : Type u)
hV : IsAffineOpen (X.basicOpen (f₁ * f₂))
f : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen (f₁ * f₂)) hV ⟶ U
mpr :
  X.basicOpen
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) f₂ (U.basicOpen f₁).toOpens ⋯) =
    toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen (f₁ * f₂)) hV)
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f

Tactic:
refine ⟨U.basicOpen f₁, ⟨f₂ |_ _, ?_⟩, ⟨f₁, rfl⟩, ⟨f₁, hf₁s, rfl⟩, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
f₁ : (↑Γ(X, U.toOpens) : Type u)
hf₁s : f₁ ∈ s
f₂ : (↑Γ(X, U.toOpens) : Type u)
hV : IsAffineOpen (X.basicOpen (f₁ * f₂))
f : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen (f₁ * f₂)) hV ⟶ U
⊢ X.basicOpen
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) f₂ (U.basicOpen f₁).toOpens ⋯) =
    toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen (f₁ * f₂)) hV)

Tactic:
(X.basicOpen_res _ _).trans (X.basicOpen_mul _ _).symm

Premises used: TopCat.Presheaf.restrict, AlgebraicGeometry.Scheme.basicOpen_mul, AlgebraicGeometry.Scheme.basicOpen_res, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
f₁ : (↑Γ(X, U.toOpens) : Type u)
hf₁s : f₁ ∈ s
f₂ : (↑Γ(X, U.toOpens) : Type u)
hV : IsAffineOpen (X.basicOpen (f₁ * f₂))
f : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen (f₁ * f₂)) hV ⟶ U
⊢ X.basicOpen
      (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) f₂ (U.basicOpen f₁).toOpens ⋯) =
    toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen (f₁ * f₂)) hV)

Tactic:
exact (X.basicOpen_res _ _).trans (X.basicOpen_mul _ _).symm

Premises used: AlgebraicGeometry.Scheme.basicOpen_mul, AlgebraicGeometry.Scheme.basicOpen_res, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
rw :
  (∀ x ∈ U.toOpens,
      ∃ (V : X.AffineZariskiSite) (f : V ⟶ U), (Sieve.generate (U.presieveOfSections s)).arrows f ∧ x ∈ V.toOpens) ↔
    ∀ ⦃x : ↥X⦄,
      x ∈ (↑U : X.Opens) →
        Membership.mem (γ := X.Opens) (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u))) x
⊢ Sieve.generate (U.presieveOfSections s) ∈ (grothendieckTopology X : (a : X.AffineZariskiSite) → Set (Sieve a)) U ↔
    Eq (α := Ideal (↑Γ(X, U.toOpens) : Type u)) (Ideal.span s) ⊤

Tactic:
rw [← U.2.self_le_iSup_basicOpen_iff, mem_grothendieckTopology, SetLike.le_def]

Premises used: AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, SetLike.le_def, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
⊢ (∀ x ∈ U.toOpens,
      ∃ (V : X.AffineZariskiSite) (f : V ⟶ U), (Sieve.generate (U.presieveOfSections s)).arrows f ∧ x ∈ V.toOpens) ↔
    ∀ ⦃x : ↥X⦄,
      x ∈ (↑U : X.Opens) →
        Membership.mem (γ := X.Opens) (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u))) x

Tactic:
forall₂_congr fun x hx ↦ ?_

Premises used: Set.Mem, forall₂_congr
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
refine :
  ∀ (x : ↥X) (hx : x ∈ U.toOpens),
    (∃ (V : X.AffineZariskiSite) (f : V ⟶ U), (Sieve.generate (U.presieveOfSections s)).arrows f ∧ x ∈ V.toOpens) ↔
      Membership.mem (γ := X.Opens) (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u))) x
⊢ (∀ x ∈ U.toOpens,
      ∃ (V : X.AffineZariskiSite) (f : V ⟶ U), (Sieve.generate (U.presieveOfSections s)).arrows f ∧ x ∈ V.toOpens) ↔
    ∀ ⦃x : ↥X⦄,
      x ∈ (↑U : X.Opens) →
        Membership.mem (γ := X.Opens) (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u))) x

Tactic:
refine forall₂_congr fun x hx ↦ ?_

Premises used: forall₂_congr
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : ↥X
hx : x ∈ U.toOpens
simp :
  (∃ (V : X.AffineZariskiSite),
      (∃ f ∈ s, ∃ (g : (↑Γ(X, U.toOpens) : Type u)), X.basicOpen (f * g) = V.toOpens) ∧
        ∃ (x_1 : V ⟶ U), x ∈ V.toOpens) ↔
    ∃ i ∈ s, x ∈ X.basicOpen i
⊢ (∃ (V : X.AffineZariskiSite) (f : V ⟶ U), (Sieve.generate (U.presieveOfSections s)).arrows f ∧ x ∈ V.toOpens) ↔
    Membership.mem (γ := X.Opens) (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u))) x

Tactic:
simp only [exists_and_left, TopologicalSpace.Opens.iSup_mk,
    TopologicalSpace.Opens.carrier_eq_coe, Set.iUnion_coe_set, TopologicalSpace.Opens.mem_mk,
    Set.mem_iUnion, SetLike.mem_coe, exists_prop, generate_presieveOfSections]

Premises used: TopologicalSpace.Opens.iSup_mk, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections, Set.mem_iUnion, Set.iUnion_coe_set, exists_and_left, exists_prop, TopologicalSpace.Opens.carrier_eq_coe, SetLike.mem_coe, TopologicalSpace.Opens.mem_mk
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : ↥X
hx : x ∈ U.toOpens
mp :
  (∃ (V : X.AffineZariskiSite),
      (∃ f ∈ s, ∃ (g : (↑Γ(X, U.toOpens) : Type u)), X.basicOpen (f * g) = V.toOpens) ∧
        ∃ (x_1 : V ⟶ U), x ∈ V.toOpens) →
    ∃ i ∈ s, x ∈ X.basicOpen i
mpr :
  (∃ i ∈ s, x ∈ X.basicOpen i) →
    ∃ (V : X.AffineZariskiSite),
      (∃ f ∈ s, ∃ (g : (↑Γ(X, U.toOpens) : Type u)), X.basicOpen (f * g) = V.toOpens) ∧ ∃ (x_1 : V ⟶ U), x ∈ V.toOpens
⊢ (∃ (V : X.AffineZariskiSite),
      (∃ f ∈ s, ∃ (g : (↑Γ(X, U.toOpens) : Type u)), X.basicOpen (f * g) = V.toOpens) ∧
        ∃ (x_1 : V ⟶ U), x ∈ V.toOpens) ↔
    ∃ i ∈ s, x ∈ X.basicOpen i

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : ↥X
hx : x ∈ U.toOpens
mp :
  (∃ (V : X.AffineZariskiSite),
      (∃ f ∈ s, ∃ (g : (↑Γ(X, U.toOpens) : Type u)), X.basicOpen f ⊓ X.basicOpen g = V.toOpens) ∧
        ∃ (x_1 : V ⟶ U), x ∈ V.toOpens) →
    ∃ i ∈ s, x ∈ X.basicOpen i
⊢ (∃ (V : X.AffineZariskiSite),
      (∃ f ∈ s, ∃ (g : (↑Γ(X, U.toOpens) : Type u)), X.basicOpen (f * g) = V.toOpens) ∧
        ∃ (x_1 : V ⟶ U), x ∈ V.toOpens) →
    ∃ i ∈ s, x ∈ X.basicOpen i

Tactic:
simp only [basicOpen_mul]

Premises used: AlgebraicGeometry.Scheme.basicOpen_mul
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : ↥X
hx : x ∈ U.toOpens
f : (↑Γ(X, U.toOpens) : Type u)
hfs : f ∈ s
g : (↑Γ(X, U.toOpens) : Type u)
hV : IsAffineOpen (X.basicOpen f ⊓ X.basicOpen g)
hxV : x ∈ toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f ⊓ X.basicOpen g) hV)
⊢ ∃ i ∈ s, x ∈ X.basicOpen i

Tactic:
⟨f, hfs, hxV.1⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : ↥X
hx : x ∈ U.toOpens
f : (↑Γ(X, U.toOpens) : Type u)
hfs : f ∈ s
g : (↑Γ(X, U.toOpens) : Type u)
hV : IsAffineOpen (X.basicOpen f ⊓ X.basicOpen g)
hxV : x ∈ toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f ⊓ X.basicOpen g) hV)
⊢ ∃ i ∈ s, x ∈ X.basicOpen i

Tactic:
exact ⟨f, hfs, hxV.1⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : ↥X
hx : x ∈ U.toOpens
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
hfs : f ∈ s
hxf : x ∈ X.basicOpen f
⊢ x ∈ (U.basicOpen (f * 1)).toOpens

Tactic:
simpa using hxf
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : ↥X
hx : x ∈ U.toOpens
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
hfs : f ∈ s
hxf : x ∈ X.basicOpen f
⊢ ∃ (V : X.AffineZariskiSite),
    (∃ f ∈ s, ∃ (g : (↑Γ(X, U.toOpens) : Type u)), X.basicOpen (f * g) = V.toOpens) ∧ ∃ (x_1 : V ⟶ U), x ∈ V.toOpens

Tactic:
refine ⟨U.basicOpen _, ⟨f, hfs, 1, rfl⟩, ⟨_, rfl⟩, by simpa using hxf⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
rw :
  S ∈ (grothendieckTopology X : (a : X.AffineZariskiSite) → Set (Sieve a)) U ↔
    Sieve.generate (U.presieveOfSections (sectionsOfPresieve S.arrows)) ∈
      (grothendieckTopology X : (a : X.AffineZariskiSite) → Set (Sieve a)) U
rw₁ :
  S ∈ (grothendieckTopology X : (a : X.AffineZariskiSite) → Set (Sieve a)) U ↔
    Sieve.generate S.arrows ∈ (grothendieckTopology X : (a : X.AffineZariskiSite) → Set (Sieve a)) U
rw₂ rw₃ :
  S ∈ (grothendieckTopology X : (a : X.AffineZariskiSite) → Set (Sieve a)) U ↔
    S ∈ (grothendieckTopology X : (a : X.AffineZariskiSite) → Set (Sieve a)) U
⊢ S ∈ (grothendieckTopology X : (a : X.AffineZariskiSite) → Set (Sieve a)) U ↔
    Eq (α := Ideal (↑Γ(X, U.toOpens) : Type u)) (Ideal.span (sectionsOfPresieve S.arrows)) ⊤

Tactic:
rw [← generate_presieveOfSections_mem_grothendieckTopology, presieveOfSections_sectionsOfPresieve,
    Sieve.generate_sieve]

Premises used: CategoryTheory.Sieve.generate_sieve, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_sectionsOfPresieve
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
rw :
  (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
          i)
⊢ PreZeroHypercover.presieve₀
      { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
        f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι } ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
          i)

Tactic:
⟨fun x ↦ ?_, inferInstance⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
refine :
  ∀ (x : ↥X),
    ∃ (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
          f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
                f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
                f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
              i))
        x
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
                  f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := X)
          { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
            f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
          i)

Tactic:
refine ⟨fun x ↦ ?_, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
x : ↥X
obtain :
  ∀ (U : (↑X.affineOpens : Type u)) (hxU : x ∈ (↑U : X.Opens)),
    ∃ (i :
      PreZeroHypercover.I₀ (C := Scheme) (S := X)
        { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
          f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
      Membership.mem (γ := Set ↥X)
        (Set.range (ι :=
          ↥(PreZeroHypercover.X
              { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
                f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
              i))
          ⇑(PreZeroHypercover.f
              { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
                f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
              i))
        x
⊢ ∃ (i :
    PreZeroHypercover.I₀ (C := Scheme) (S := X)
      { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
        f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
      x

Tactic:
obtain ⟨U, hxU⟩ := TopologicalSpace.Opens.mem_iSup.mp
      ((iSup_affineOpens_eq_top X).ge (Set.mem_univ x))

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, Eq.ge, TopologicalSpace.Opens.mem_iSup, Iff.mp, Set.mem_univ
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
x : ↥X
U : (↑X.affineOpens : Type u)
hxU : x ∈ (↑U : X.Opens)
⊢ ∃ (i :
    PreZeroHypercover.I₀ (C := Scheme) (S := X)
      { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
        f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
      x

Tactic:
⟨U, ⟨x, hxU⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
x : ↥X
U : (↑X.affineOpens : Type u)
hxU : x ∈ (↑U : X.Opens)
⊢ ∃ (i :
    PreZeroHypercover.I₀ (C := Scheme) (S := X)
      { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
        f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι }),
    Membership.mem (γ := Set ↥X)
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := X.AffineZariskiSite, X := fun (U : X.AffineZariskiSite) ↦ (↑(↑U : X.Opens) : Scheme),
              f := fun (U : X.AffineZariskiSite) ↦ (↑U : X.Opens).ι : PreZeroHypercover X }
            i))
      x

Tactic:
exact ⟨U, ⟨x, hxU⟩, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
⊢ a ∈ (↑U : X.Opens)

Tactic:
have haU : a ∈ U.1 := (pullback.fst U.1.ι V.1.ι x).2
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x
haU : a ∈ (↑U : X.Opens)
unfold :
  Membership.mem (α := ↥X) (↑V : X.Opens)
    ((pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U : X.Opens).ι) x : ↥X)
⊢ a ∈ (↑V : X.Opens)

Tactic:
unfold a