-- Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean
lemma generate_presieveOfSections_mem_grothendieckTopology
    {U : X.AffineZariskiSite} {s : Set Γ(X, U.toOpens)} :
    Sieve.generate (presieveOfSections U s) ∈ grothendieckTopology X U ↔ Ideal.span s = ⊤

Proof state:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
f : ↑Γ(X, ↑U)
hfs : f ∈ s
hxf : x ∈ X.basicOpen f
⊢ x ∈ (U.basicOpen (f * 1)).toOpens

Tactic:
simpa using hxf

Result:
no goals

Proof state:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
⊢ (∃ V f, (Sieve.generate (U.presieveOfSections s)).arrows f ∧ x ∈ V.toOpens) ↔ x ∈ ⨆ f, X.basicOpen ↑f

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]

Result:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
⊢ (∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens) ↔ ∃ i ∈ s, x ∈ X.basicOpen i

Proof state:
case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
⊢ (∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens) → ∃ i ∈ s, x ∈ X.basicOpen i

Tactic:
simp only [basicOpen_mul]

Result:
case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
⊢ (∃ V, (∃ f ∈ s, ∃ g, X.basicOpen f ⊓ X.basicOpen g = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens) → ∃ i ∈ s, x ∈ X.basicOpen i

Proof state:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
⊢ Sieve.generate (U.presieveOfSections s) ∈ (grothendieckTopology X) U ↔ Ideal.span s = ⊤

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

Result:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
⊢ (∀ x ∈ U.toOpens, ∃ V f, (Sieve.generate (U.presieveOfSections s)).arrows f ∧ x ∈ V.toOpens) ↔
    ∀ ⦃x : ↑↑X.toPresheafedSpace⦄, x ∈ ↑U → x ∈ ⨆ f, X.basicOpen ↑f

Proof state:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
⊢ (∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens) ↔ ∃ i ∈ s, x ∈ X.basicOpen i

Tactic:
constructor

Result:
case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
⊢ (∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens) → ∃ i ∈ s, x ∈ X.basicOpen i

case mpr
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
⊢ (∃ i ∈ s, x ∈ X.basicOpen i) → ∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens

Proof state:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
⊢ (∀ x ∈ U.toOpens, ∃ V f, (Sieve.generate (U.presieveOfSections s)).arrows f ∧ x ∈ V.toOpens) ↔
    ∀ ⦃x : ↑↑X.toPresheafedSpace⦄, x ∈ ↑U → x ∈ ⨆ f, X.basicOpen ↑f

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

Result:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
⊢ (∃ V f, (Sieve.generate (U.presieveOfSections s)).arrows f ∧ x ∈ V.toOpens) ↔ x ∈ ⨆ f, X.basicOpen ↑f

Proof state:
case mpr.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
f : ↑Γ(X, ↑U)
hfs : f ∈ s
hxf : x ∈ X.basicOpen f
⊢ ∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens

Tactic:
refine ⟨U.basicOpen _, ⟨f, hfs, 1, rfl⟩, ⟨_, rfl⟩, by simpa using hxf⟩

Result:
no goals

Proof state:
case mpr
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
⊢ (∃ i ∈ s, x ∈ X.basicOpen i) → ∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens

Tactic:
rintro ⟨f, hfs, hxf⟩

Result:
case mpr.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
f : ↑Γ(X, ↑U)
hfs : f ∈ s
hxf : x ∈ X.basicOpen f
⊢ ∃ V, (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens

Proof state:
case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
⊢ (∃ V, (∃ f ∈ s, ∃ g, X.basicOpen f ⊓ X.basicOpen g = V.toOpens) ∧ ∃ x_1, x ∈ V.toOpens) → ∃ i ∈ s, x ∈ X.basicOpen i

Tactic:
rintro ⟨⟨V, hV⟩, ⟨f, hfs, g, rfl⟩, -, hxV⟩

Result:
case mp.intro.mk.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
f : ↑Γ(X, U.toOpens)
hfs : f ∈ s
g : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen f ⊓ X.basicOpen g)
hxV : x ∈ toOpens ⟨X.basicOpen f ⊓ X.basicOpen g, hV⟩
⊢ ∃ i ∈ s, x ∈ X.basicOpen i

Proof state:
case mp.intro.mk.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x : ↑↑X.toPresheafedSpace
hx : x ∈ U.toOpens
f : ↑Γ(X, U.toOpens)
hfs : f ∈ s
g : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen f ⊓ X.basicOpen g)
hxV : x ∈ toOpens ⟨X.basicOpen f ⊓ X.basicOpen g, hV⟩
⊢ ∃ i ∈ s, x ∈ X.basicOpen i

Tactic:
exact ⟨f, hfs, hxV.1⟩

Result:
no goals