-- Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean
lemma presieveOfSections_eq_ofArrows (U : X.AffineZariskiSite) (s : Set Γ(X, U.toOpens)) :
    presieveOfSections U s = .ofArrows _ (fun i : s ↦ homOfLE (U.basicOpen_le i.1))

Proof state:
case refine_2.mk.mk
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x✝¹ : X.AffineZariskiSite
f✝ : ↑Γ(X, U.toOpens)
Y : X.AffineZariskiSite
f : ↑Γ(X, U.toOpens)
hfs : f ∈ s
hV : IsAffineOpen (X.basicOpen ↑⟨f, hfs⟩)
x✝ : ⟨X.basicOpen ↑⟨f, hfs⟩, hV⟩ ⟶ U
hf : X.basicOpen f✝ = toOpens ⟨X.basicOpen ↑⟨f, hfs⟩, hV⟩
⊢ U.presieveOfSections s { down := { down := ⋯ } }

Tactic:
exact ⟨f, hfs, rfl⟩

Result:
no goals

Proof state:
case refine_1.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x✝¹ : X.AffineZariskiSite
f✝ f : ↑Γ(X, U.toOpens)
hfs : f ∈ s
hV : IsAffineOpen (X.basicOpen f)
x✝ : ⟨X.basicOpen f, hV⟩ ⟶ U
hf : X.basicOpen f✝ = toOpens ⟨X.basicOpen f, hV⟩
⊢ Presieve.ofArrows (fun i => U.basicOpen ↑i) (fun i => homOfLE ⋯) { down := { down := ⋯ } }

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

Result:
no goals

Proof state:
case refine_1
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
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 s { down := { down := ⋯ } } →
    Presieve.ofArrows (fun i => U.basicOpen ↑i) (fun i => homOfLE ⋯) { down := { down := ⋯ } }

Tactic:
rintro ⟨f, hfs, rfl⟩

Result:
case refine_1.intro.intro
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x✝¹ : X.AffineZariskiSite
f✝ f : ↑Γ(X, U.toOpens)
hfs : f ∈ s
hV : IsAffineOpen (X.basicOpen f)
x✝ : ⟨X.basicOpen f, hV⟩ ⟶ U
hf : X.basicOpen f✝ = toOpens ⟨X.basicOpen f, hV⟩
⊢ Presieve.ofArrows (fun i => U.basicOpen ↑i) (fun i => homOfLE ⋯) { down := { down := ⋯ } }

Proof state:
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
⊢ U.presieveOfSections s = Presieve.ofArrows (fun i => U.basicOpen ↑i) fun i => homOfLE ⋯

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

Result:
case refine_1
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
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 s { down := { down := ⋯ } } →
    Presieve.ofArrows (fun i => U.basicOpen ↑i) (fun i => homOfLE ⋯) { down := { down := ⋯ } }

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

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

Tactic:
rintro ⟨⟨f, hfs⟩⟩

Result:
case refine_2.mk.mk
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
x✝¹ : X.AffineZariskiSite
f✝ : ↑Γ(X, U.toOpens)
Y : X.AffineZariskiSite
f : ↑Γ(X, U.toOpens)
hfs : f ∈ s
hV : IsAffineOpen (X.basicOpen ↑⟨f, hfs⟩)
x✝ : ⟨X.basicOpen ↑⟨f, hfs⟩, hV⟩ ⟶ U
hf : X.basicOpen f✝ = toOpens ⟨X.basicOpen ↑⟨f, hfs⟩, hV⟩
⊢ U.presieveOfSections s { down := { down := ⋯ } }