awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : X.AffineZariskiSite
h : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V
x : ↥X
hx : x ∈ (toOpensFunctor X).obj U
obtain :
  ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u)) (hfU : X.basicOpen f ≤ (toOpensFunctor X).obj U)
    (hxf : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (toOpensFunctor X).obj U) x hx) : ↥X) ∈ X.basicOpen f),
    ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ (toOpensFunctor X).obj U),
      (Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h)).arrows f ∧ x ∈ U_1
⊢ ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ (toOpensFunctor X).obj U),
    (Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h)).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨f, hfU, hxf⟩ := V.2.exists_basicOpen_le ⟨x, hx⟩ (h.le hx)

Premises used: Quiver.Hom.le, Subtype.mk, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : X.AffineZariskiSite
h : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V
x : ↥X
hx : x ∈ (toOpensFunctor X).obj U
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfU : X.basicOpen f ≤ (toOpensFunctor X).obj U
hxf : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (toOpensFunctor X).obj U) x hx) : ↥X) ∈ X.basicOpen f
⊢ ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ (toOpensFunctor X).obj U),
    (Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h)).arrows f ∧ x ∈ U_1

Tactic:
⟨X.basicOpen f, homOfLE hfU, ⟨V.basicOpen f,
      ⟨_, (X.basicOpen_res f h.op).trans (inf_eq_right.mpr hfU)⟩, 𝟙 _,
      ⟨⟨f, rfl⟩, rfl⟩, rfl⟩, hxf⟩

Premises used: Iff.mpr, Quiver.Hom.op, CategoryTheory.CategoryStruct.id, PLift.up, AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen, CategoryTheory.homOfLE, And.intro, AlgebraicGeometry.Scheme.basicOpen, Exists.intro, AlgebraicGeometry.Scheme.basicOpen_res, ULift.up, inf_eq_right, rfl, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : X.AffineZariskiSite
h : (toOpensFunctor X).obj U ⟶ (toOpensFunctor X).obj V
x : ↥X
hx : x ∈ (toOpensFunctor X).obj U
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfU : X.basicOpen f ≤ (toOpensFunctor X).obj U
hxf : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (toOpensFunctor X).obj U) x hx) : ↥X) ∈ X.basicOpen f
⊢ ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ (toOpensFunctor X).obj U),
    (Sieve.functorPushforward (toOpensFunctor X) ((toOpensFunctor X).imageSieve h)).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨X.basicOpen f, homOfLE hfU, ⟨V.basicOpen f,
      ⟨_, (X.basicOpen_res f h.op).trans (inf_eq_right.mpr hfU)⟩, 𝟙 _,
      ⟨⟨f, rfl⟩, rfl⟩, rfl⟩, hxf⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
obtain :
  ∀ (V : TopologicalSpace.Opens ↥X) (hV : V ∈ X.affineOpens) (hxV : x ∈ (↑V : Set ↥X))
    (hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)),
    ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ U), (Sieve.coverByImage (toOpensFunctor X) U).arrows f ∧ x ∈ U_1
⊢ ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ U), (Sieve.coverByImage (toOpensFunctor X) U).arrows f ∧ x ∈ U_1

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open hx U.2

Premises used: TopologicalSpace.Opens.is_open', AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ U), (Sieve.coverByImage (toOpensFunctor X) U).arrows f ∧ x ∈ U_1

Tactic:
⟨V, homOfLE hVU, ⟨⟨V, hV⟩, 𝟙 _, homOfLE hVU, rfl⟩, hxV⟩

Premises used: CategoryTheory.CategoryStruct.id, Nonempty.intro, Subtype.mk, CategoryTheory.homOfLE, And.intro, Exists.intro, CategoryTheory.Presieve.CoverByImageStructure.mk, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ U), (Sieve.coverByImage (toOpensFunctor X) U).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨V, homOfLE hVU, ⟨⟨V, hV⟩, 𝟙 _, homOfLE hVU, rfl⟩, hxV⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
apply :
  ∀ (x : ↥X) (hxU : x ∈ (toOpensFunctor X).obj U),
    (∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ (toOpensFunctor X).obj U),
        (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1) →
      ∃ (V : X.AffineZariskiSite) (f : V ⟶ U), S.arrows f ∧ x ∈ V.toOpens
apply₁ :
  ∀ (x : ↥X) (hxU : x ∈ (toOpensFunctor X).obj U),
    (∃ (V : X.AffineZariskiSite) (f : V ⟶ U), S.arrows f ∧ x ∈ V.toOpens) →
      ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ (toOpensFunctor X).obj U),
        (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1
⊢ S ∈ (grothendieckTopology X : (a : X.AffineZariskiSite) → Set (Sieve a)) U ↔
    ∀ x ∈ U.toOpens, ∃ (V : X.AffineZariskiSite) (f : V ⟶ U), S.arrows f ∧ x ∈ V.toOpens

Tactic:
apply forall₂_congr fun x hxU ↦ ⟨?_, ?_⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
V : TopologicalSpace.Opens ↥X
hxV : x ∈ V
W : X.AffineZariskiSite
g : W ⟶ U
h : V ⟶ (toOpensFunctor X).obj W
hg : S.arrows g
⊢ ∃ (V : X.AffineZariskiSite) (f : V ⟶ U), S.arrows f ∧ x ∈ V.toOpens

Tactic:
⟨W, g, hg, h.le hxV⟩

Premises used: Quiver.Hom.le, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
V : TopologicalSpace.Opens ↥X
hxV : x ∈ V
W : X.AffineZariskiSite
g : W ⟶ U
h : V ⟶ (toOpensFunctor X).obj W
hg : S.arrows g
⊢ ∃ (V : X.AffineZariskiSite) (f : V ⟶ U), S.arrows f ∧ x ∈ V.toOpens

Tactic:
exact ⟨W, g, hg, h.le hxV⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
W : X.AffineZariskiSite
g : W ⟶ U
hg : S.arrows g
hxW : x ∈ W.toOpens
⊢ ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ (toOpensFunctor X).obj U),
    (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1

Tactic:
⟨W.toOpens, homOfLE (toOpens_mono g.le), ⟨W, g, 𝟙 _, hg, rfl⟩, hxW⟩

Premises used: Quiver.Hom.le, CategoryTheory.CategoryStruct.id, CategoryTheory.homOfLE, And.intro, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens_mono, AlgebraicGeometry.Scheme.AffineZariskiSite.toOpens, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↥X
hxU : x ∈ (toOpensFunctor X).obj U
W : X.AffineZariskiSite
g : W ⟶ U
hg : S.arrows g
hxW : x ∈ W.toOpens
⊢ ∃ (U_1 : TopologicalSpace.Opens ↥X) (f : U_1 ⟶ (toOpensFunctor X).obj U),
    (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨W.toOpens, homOfLE (toOpens_mono g.le), ⟨W, g, 𝟙 _, hg, rfl⟩, hxW⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
⊢ U.presieveOfSections (sectionsOfPresieve P) = P

Tactic:
funext₂ fun ⟨V, hV⟩ ⟨f, hf⟩ ↦ eq_iff_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, CategoryTheory.Presieve, _private.0.AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_sectionsOfPresieve.match_2, AlgebraicGeometry.Scheme.AffineZariskiSite.sectionsOfPresieve, _private.0.AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_sectionsOfPresieve.match_1, funext₂, Iff.intro, Eq, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections, eq_iff_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
refine_1 :
  ∀ (x : X.AffineZariskiSite) (V : X.Opens) (hV : IsAffineOpen V)
    (x : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV ⟶ U) (f : (↑Γ(X, U.toOpens) : Type u))
    (hf : X.basicOpen f = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)),
    U.presieveOfSections (sectionsOfPresieve P) (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)
        { down := { down := ⋯ } } →
      P (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV) { down := { down := ⋯ } }
refine_2 :
  ∀ (x : X.AffineZariskiSite) (V : X.Opens) (hV : IsAffineOpen V)
    (x : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV ⟶ U) (f : (↑Γ(X, U.toOpens) : Type u))
    (hf : X.basicOpen f = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)),
    P (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV) { down := { down := ⋯ } } →
      U.presieveOfSections (sectionsOfPresieve P) (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)
        { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) = P

Tactic:
refine funext₂ fun ⟨V, hV⟩ ⟨f, hf⟩ ↦ eq_iff_iff.mpr ⟨?_, ?_⟩

Premises used: funext₂
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x : X.AffineZariskiSite
f w : (↑Γ(X, U.toOpens) : Type u)
H : w ∈ sectionsOfPresieve P
hV : IsAffineOpen (X.basicOpen w)
x_1 : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen w) hV ⟶ U
hf : X.basicOpen f = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen w) hV)
⊢ P (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen w) hV) { down := { down := ⋯ } }

Tactic:
H

Premises used: Set.Mem, setOf, AlgebraicGeometry.Scheme.AffineZariskiSite.sectionsOfPresieve, AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen, CategoryTheory.homOfLE
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x : X.AffineZariskiSite
f w : (↑Γ(X, U.toOpens) : Type u)
H : w ∈ sectionsOfPresieve P
hV : IsAffineOpen (X.basicOpen w)
x_1 : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen w) hV ⟶ U
hf : X.basicOpen f = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen w) hV)
⊢ P (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen w) hV) { down := { down := ⋯ } }

Tactic:
exact H
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x_1 : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV ⟶ U
f : (↑Γ(X, U.toOpens) : Type u)
hf : X.basicOpen f = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)
H : P (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV) { down := { down := ⋯ } }
⊢ X.basicOpen f = V

Tactic:
hf
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x_1 : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV ⟶ U
f : (↑Γ(X, U.toOpens) : Type u)
hf : X.basicOpen f = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)
H : P (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV) { down := { down := ⋯ } }
refine_2 :
  ∀ (hV : IsAffineOpen (X.basicOpen f))
    (x : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV ⟶ U)
    (H : P (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV) { down := { down := ⋯ } }),
    U.presieveOfSections (sectionsOfPresieve P) (Y :=
      Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV) { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)
    { down := { down := ⋯ } }

Tactic:
obtain rfl : _ = V := hf

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x : X.AffineZariskiSite
f : (↑Γ(X, U.toOpens) : Type u)
hV : IsAffineOpen (X.basicOpen f)
x_1 : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV ⟶ U
H : P (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV) { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) (Y :=
    Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV) { down := { down := ⋯ } }

Tactic:
⟨_, H, rfl⟩

Premises used: And.intro, Exists.intro, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x : X.AffineZariskiSite
f : (↑Γ(X, U.toOpens) : Type u)
hV : IsAffineOpen (X.basicOpen f)
x_1 : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV ⟶ U
H : P (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV) { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) (Y :=
    Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV) { down := { down := ⋯ } }

Tactic:
exact ⟨_, H, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
⊢ Function.Surjective U.presieveOfSections

Tactic:
fun _ ↦ ⟨_, presieveOfSections_sectionsOfPresieve _⟩

Premises used: AlgebraicGeometry.Scheme.AffineZariskiSite.sectionsOfPresieve, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_sectionsOfPresieve, Exists.intro, Function.Surjective
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
⊢ U.presieveOfSections s =
    Presieve.ofArrows (fun (i : (↑s : Type u)) ↦ U.basicOpen (↑i : (↑Γ(X, U.toOpens) : Type u)))
      fun (i : (↑s : Type u)) ↦ homOfLE ⋯

Tactic:
funext₂ fun ⟨V, hV⟩ ⟨f, hf⟩ ↦ eq_iff_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen_le, CategoryTheory.Presieve, _private.0.AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_sectionsOfPresieve.match_2, _private.0.AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections_sectionsOfPresieve.match_1, AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen, funext₂, CategoryTheory.homOfLE, Iff.intro, Subtype.val, Eq, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections, CategoryTheory.Presieve.ofArrows, eq_iff_iff
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
refine_1 :
  ∀ (x : X.AffineZariskiSite) (V : X.Opens) (hV : IsAffineOpen V)
    (x : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV ⟶ U) (f : (↑Γ(X, U.toOpens) : Type u))
    (hf : X.basicOpen f = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)),
    U.presieveOfSections s (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV) { down := { down := ⋯ } } →
      Presieve.ofArrows (C := X.AffineZariskiSite) (X := U)
        (fun (i : (↑s : Type u)) ↦ U.basicOpen (↑i : (↑Γ(X, U.toOpens) : Type u))) fun (i : (↑s : Type u)) ↦ homOfLE ⋯
        (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV) { down := { down := ⋯ } }
refine_2 :
  ∀ (x : X.AffineZariskiSite) (V : X.Opens) (hV : IsAffineOpen V)
    (x : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV ⟶ U) (f : (↑Γ(X, U.toOpens) : Type u))
    (hf : X.basicOpen f = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)),
    Presieve.ofArrows (C := X.AffineZariskiSite) (X := U)
        (fun (i : (↑s : Type u)) ↦ U.basicOpen (↑i : (↑Γ(X, U.toOpens) : Type u))) fun (i : (↑s : Type u)) ↦ homOfLE ⋯
        (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV) { down := { down := ⋯ } } →
      U.presieveOfSections s (Y := Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV) { down := { down := ⋯ } }
⊢ U.presieveOfSections s =
    Presieve.ofArrows (fun (i : (↑s : Type u)) ↦ U.basicOpen (↑i : (↑Γ(X, U.toOpens) : Type u)))
      fun (i : (↑s : Type u)) ↦ homOfLE ⋯

Tactic:
refine funext₂ fun ⟨V, hV⟩ ⟨f, hf⟩ ↦ eq_iff_iff.mpr ⟨?_, ?_⟩

Premises used: funext₂
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : X.AffineZariskiSite
f_1 f : (↑Γ(X, U.toOpens) : Type u)
hfs : f ∈ s
hV : IsAffineOpen (X.basicOpen f)
x_1 : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV ⟶ U
hf : X.basicOpen f_1 = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV)
⊢ Presieve.ofArrows (C := X.AffineZariskiSite) (X := U)
    (fun (i : (↑s : Type u)) ↦ U.basicOpen (↑i : (↑Γ(X, U.toOpens) : Type u))) fun (i : (↑s : Type u)) ↦ homOfLE ⋯ (Y :=
    Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV) { down := { down := ⋯ } }

Tactic:
.mk (ι := s) ⟨f, hfs⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, Subtype.mk, AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen, CategoryTheory.homOfLE
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : X.AffineZariskiSite
f_1 f : (↑Γ(X, U.toOpens) : Type u)
hfs : f ∈ s
hV : IsAffineOpen (X.basicOpen f)
x_1 : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV ⟶ U
hf : X.basicOpen f_1 = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV)
⊢ Presieve.ofArrows (C := X.AffineZariskiSite) (X := U)
    (fun (i : (↑s : Type u)) ↦ U.basicOpen (↑i : (↑Γ(X, U.toOpens) : Type u))) fun (i : (↑s : Type u)) ↦ homOfLE ⋯ (Y :=
    Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) (X.basicOpen f) hV) { down := { down := ⋯ } }

Tactic:
exact .mk (ι := s) ⟨f, hfs⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : X.AffineZariskiSite
f_1 : (↑Γ(X, U.toOpens) : Type u)
Y : X.AffineZariskiSite
f : (↑Γ(X, U.toOpens) : Type u)
hfs : f ∈ s
hV :
  IsAffineOpen
    (X.basicOpen
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, U.toOpens) : Type u)) ↦ x ∈ s) f hfs) : (↑Γ(X, U.toOpens) : Type u)))
x_1 :
  Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U)
      (X.basicOpen
        (↑(Subtype.mk (p := fun (x : (↑Γ(X, U.toOpens) : Type u)) ↦ x ∈ s) f hfs) : (↑Γ(X, U.toOpens) : Type u)))
      hV ⟶
    U
hf :
  X.basicOpen f_1 =
    toOpens
      (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U)
        (X.basicOpen
          (↑(Subtype.mk (p := fun (x : (↑Γ(X, U.toOpens) : Type u)) ↦ x ∈ s) f hfs) : (↑Γ(X, U.toOpens) : Type u)))
        hV)
⊢ U.presieveOfSections s (Y :=
    Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U)
      (X.basicOpen
        (↑(Subtype.mk (p := fun (x : (↑Γ(X, U.toOpens) : Type u)) ↦ x ∈ s) f hfs) : (↑Γ(X, U.toOpens) : Type u)))
      hV)
    { down := { down := ⋯ } }

Tactic:
⟨f, hfs, rfl⟩

Premises used: And.intro, Exists.intro, AlgebraicGeometry.Scheme.AffineZariskiSite.presieveOfSections, rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
x : X.AffineZariskiSite
f_1 : (↑Γ(X, U.toOpens) : Type u)
Y : X.AffineZariskiSite
f : (↑Γ(X, U.toOpens) : Type u)
hfs : f ∈ s
hV :
  IsAffineOpen
    (X.basicOpen
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, U.toOpens) : Type u)) ↦ x ∈ s) f hfs) : (↑Γ(X, U.toOpens) : Type u)))
x_1 :
  Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U)
      (X.basicOpen
        (↑(Subtype.mk (p := fun (x : (↑Γ(X, U.toOpens) : Type u)) ↦ x ∈ s) f hfs) : (↑Γ(X, U.toOpens) : Type u)))
      hV ⟶
    U
hf :
  X.basicOpen f_1 =
    toOpens
      (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U)
        (X.basicOpen
          (↑(Subtype.mk (p := fun (x : (↑Γ(X, U.toOpens) : Type u)) ↦ x ∈ s) f hfs) : (↑Γ(X, U.toOpens) : Type u)))
        hV)
⊢ U.presieveOfSections s (Y :=
    Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U)
      (X.basicOpen
        (↑(Subtype.mk (p := fun (x : (↑Γ(X, U.toOpens) : Type u)) ↦ x ∈ s) f hfs) : (↑Γ(X, U.toOpens) : Type u)))
      hV)
    { down := { down := ⋯ } }

Tactic:
exact ⟨f, hfs, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U V : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
f : V ⟶ U
obtain :
  ∀ (V : X.Opens) (hV : IsAffineOpen V) {f : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV ⟶ U},
    (Sieve.generate (U.presieveOfSections s)).arrows f ↔
      ∃ f ∈ s,
        ∃ (g : (↑Γ(X, U.toOpens) : Type u)),
          X.basicOpen (f * g) = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f ↔
    ∃ f ∈ s, ∃ (g : (↑Γ(X, U.toOpens) : Type u)), X.basicOpen (f * g) = V.toOpens

Tactic:
obtain ⟨V, hV⟩ := V
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
V : X.Opens
hV : IsAffineOpen V
f : Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV ⟶ U
mp :
  (Sieve.generate (U.presieveOfSections s)).arrows f →
    ∃ f ∈ s,
      ∃ (g : (↑Γ(X, U.toOpens) : Type u)),
        X.basicOpen (f * g) = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)
mpr :
  (∃ f ∈ s,
      ∃ (g : (↑Γ(X, U.toOpens) : Type u)),
        X.basicOpen (f * g) = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)) →
    (Sieve.generate (U.presieveOfSections s)).arrows f
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f ↔
    ∃ f ∈ s,
      ∃ (g : (↑Γ(X, U.toOpens) : Type u)),
        X.basicOpen (f * g) = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Goal:
X : Scheme
U : X.AffineZariskiSite
s : Set (↑Γ(X, U.toOpens) : Type u)
V : X.Opens
hV : IsAffineOpen V
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)
hf₁ : X.basicOpen f₁ = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)
mp :
  ∀ (hV : IsAffineOpen (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)
⊢ ∃ f ∈ s,
    ∃ (g : (↑Γ(X, U.toOpens) : Type u)),
      X.basicOpen (f * g) = toOpens (Subtype.mk (p := fun (U : X.Opens) ↦ IsAffineOpen U) V hV)

Tactic:
subst hf₁
-- 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₁)
mp :
  ∀ (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)
⊢ ∃ 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:
obtain ⟨f₃, hf₃⟩ := U.2.basicOpen_basicOpen_is_basicOpen f₂ f₁

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen, Subtype.property