-- Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean
lemma generate_presieveOfSections
    {U V : X.AffineZariskiSite} {s : Set Γ(X, U.toOpens)} {f : V ⟶ U} :
    Sieve.generate (presieveOfSections U s) f ↔ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens

Proof state:
case mk.mp.intro.mk.intro.up.up.intro.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ X.basicOpen f₁ ≤ X.basicOpen f₂

Tactic:
exact X.basicOpen_le _

Result:
no goals

Proof state:
case mk.mpr.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₁ : ↑Γ(X, U.toOpens)
hf₁s : f₁ ∈ s
f₂ : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen (f₁ * f₂))
f : ⟨X.basicOpen (f₁ * f₂), hV⟩ ⟶ U
⊢ X.basicOpen ((f₂ |_ (U.basicOpen f₁).toOpens) ⋯) = toOpens ⟨X.basicOpen (f₁ * f₂), hV⟩

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

Result:
no goals

Proof state:
X : Scheme
U V : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f : V ⟶ U
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f ↔ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = V.toOpens

Tactic:
obtain ⟨V, hV⟩ := V

Result:
case mk
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f : ⟨V, hV⟩ ⟶ U
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f ↔ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩

Proof state:
case mk.mp.intro.mk.intro.up.up.intro.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨X.basicOpen f₁, hV⟩

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

Result:
case mk.mp.intro.mk.intro.up.up.intro.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ X.basicOpen (f₂ * f₃) = toOpens ⟨X.basicOpen f₁, hV⟩

Proof state:
case mk.mp.intro.mk.intro.up.up.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
⊢ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨X.basicOpen f₁, hV⟩

Tactic:
obtain ⟨f₃, hf₃⟩ := U.2.basicOpen_basicOpen_is_basicOpen f₂ f₁

Result:
case mk.mp.intro.mk.intro.up.up.intro.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨X.basicOpen f₁, hV⟩

Proof state:
case mk
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f : ⟨V, hV⟩ ⟶ U
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f ↔ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩

Tactic:
constructor

Result:
case mk.mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f : ⟨V, hV⟩ ⟶ U
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f → ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩

case mk.mpr
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f : ⟨V, hV⟩ ⟶ U
⊢ (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩) → (Sieve.generate (U.presieveOfSections s)).arrows f

Proof state:
case mk.mp.intro.mk.intro.up.up.intro.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ X.basicOpen (f₂ * f₃) = toOpens ⟨X.basicOpen f₁, hV⟩

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

Result:
case mk.mp.intro.mk.intro.up.up.intro.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ X.basicOpen f₁ ≤ X.basicOpen f₂

Proof state:
case mk.mpr.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₁ : ↑Γ(X, U.toOpens)
hf₁s : f₁ ∈ s
f₂ : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen (f₁ * f₂))
f : ⟨X.basicOpen (f₁ * f₂), hV⟩ ⟶ U
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f

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

Result:
case mk.mpr.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₁ : ↑Γ(X, U.toOpens)
hf₁s : f₁ ∈ s
f₂ : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen (f₁ * f₂))
f : ⟨X.basicOpen (f₁ * f₂), hV⟩ ⟶ U
⊢ X.basicOpen ((f₂ |_ (U.basicOpen f₁).toOpens) ⋯) = toOpens ⟨X.basicOpen (f₁ * f₂), hV⟩

Proof state:
case mk.mpr
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f : ⟨V, hV⟩ ⟶ U
⊢ (∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩) → (Sieve.generate (U.presieveOfSections s)).arrows f

Tactic:
rintro ⟨f₁, hf₁s, f₂, rfl⟩

Result:
case mk.mpr.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₁ : ↑Γ(X, U.toOpens)
hf₁s : f₁ ∈ s
f₂ : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen (f₁ * f₂))
f : ⟨X.basicOpen (f₁ * f₂), hV⟩ ⟶ U
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f

Proof state:
case mk.mp.intro.mk.intro.up.up.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hf₁ : X.basicOpen f₁ = toOpens ⟨V, hV⟩
⊢ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩

Tactic:
subst hf₁

Result:
case mk.mp.intro.mk.intro.up.up.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
⊢ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨X.basicOpen f₁, hV⟩

Proof state:
case mk.mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f : ⟨V, hV⟩ ⟶ U
⊢ (Sieve.generate (U.presieveOfSections s)).arrows f → ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩

Tactic:
rintro ⟨⟨W, hW⟩, ⟨f₁, hf₁⟩, -, ⟨f₂, hf₂s, rfl⟩, rfl⟩

Result:
case mk.mp.intro.mk.intro.up.up.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
V : X.Opens
hV : IsAffineOpen V
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hf₁ : X.basicOpen f₁ = toOpens ⟨V, hV⟩
⊢ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨V, hV⟩