-- Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean
lemma presieveOfSections_sectionsOfPresieve {U : X.AffineZariskiSite} (P : Presieve U) :
    presieveOfSections U (sectionsOfPresieve P) = P

Proof state:
case refine_1.intro.intro
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
f w✝ : ↑Γ(X, U.toOpens)
H : w✝ ∈ sectionsOfPresieve P
hV : IsAffineOpen (X.basicOpen w✝)
x✝ : ⟨X.basicOpen w✝, hV⟩ ⟶ U
hf : X.basicOpen f = toOpens ⟨X.basicOpen w✝, hV⟩
⊢ P { down := { down := ⋯ } }

Tactic:
exact H

Result:
no goals

Proof state:
case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
f : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen f)
x✝ : ⟨X.basicOpen f, hV⟩ ⟶ U
H : P { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }

Tactic:
exact ⟨_, H, rfl⟩

Result:
no goals

Proof state:
case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ P { down := { down := ⋯ } } → U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }

Tactic:
intro H

Result:
case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
H : P { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }

Proof state:
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
⊢ U.presieveOfSections (sectionsOfPresieve P) = P

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

Result:
case refine_1
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } } → P { down := { down := ⋯ } }

case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ P { down := { down := ⋯ } } → U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }

Proof state:
case refine_1
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } } → P { down := { down := ⋯ } }

Tactic:
rintro ⟨_, H, rfl⟩

Result:
case refine_1.intro.intro
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
f w✝ : ↑Γ(X, U.toOpens)
H : w✝ ∈ sectionsOfPresieve P
hV : IsAffineOpen (X.basicOpen w✝)
x✝ : ⟨X.basicOpen w✝, hV⟩ ⟶ U
hf : X.basicOpen f = toOpens ⟨X.basicOpen w✝, hV⟩
⊢ P { down := { down := ⋯ } }

Proof state:
case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
V : X.Opens
hV : IsAffineOpen V
x✝ : ⟨V, hV⟩ ⟶ U
f : ↑Γ(X, U.toOpens)
hf : X.basicOpen f = toOpens ⟨V, hV⟩
H : P { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }

Tactic:
obtain rfl : _ = V := hf

Result:
case refine_2
X : Scheme
U : X.AffineZariskiSite
P : Presieve U
x✝¹ : X.AffineZariskiSite
f : ↑Γ(X, U.toOpens)
hV : IsAffineOpen (X.basicOpen f)
x✝ : ⟨X.basicOpen f, hV⟩ ⟶ U
H : P { down := { down := ⋯ } }
⊢ U.presieveOfSections (sectionsOfPresieve P) { down := { down := ⋯ } }