-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
theorem iSup_eq_of_mem_grothendieck (hR : Sieve.generate R ∈ Opens.grothendieckTopology X U) :
    iSup (coveringOfPresieve U R) = U

Proof state:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) ≤ U

Tactic:
refine iSup_le ?_

Result:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ ∀ (i : (V : Opens ↑X) × { f // R f }), coveringOfPresieve U R i ≤ U

Proof state:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
f : (V : Opens ↑X) × { f // R f }
⊢ coveringOfPresieve U R f ≤ U

Tactic:
exact f.2.1.le

Result:
no goals

Proof state:
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) = U

Tactic:
apply le_antisymm

Result:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) ≤ U

case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ U ≤ iSup (coveringOfPresieve U R)

Proof state:
case a.intro.intro.intro.intro.intro.intro.intro
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
V : Opens ↑X
iVU : V ⟶ U
hxV : x ∈ V
W : Opens ↑X
iVW : V ⟶ W
iWU : W ⟶ U
hiWU : R iWU
⊢ ∃ i, x ∈ ↑(coveringOfPresieve U R i)

Tactic:
exact ⟨⟨W, ⟨iWU, hiWU⟩⟩, iVW.le hxV⟩

Result:
no goals

Proof state:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ ∀ (i : (V : Opens ↑X) × { f // R f }), coveringOfPresieve U R i ≤ U

Tactic:
intro f

Result:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
f : (V : Opens ↑X) × { f // R f }
⊢ coveringOfPresieve U R f ≤ U

Proof state:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ U ≤ iSup (coveringOfPresieve U R)

Tactic:
intro x hxU

Result:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup (coveringOfPresieve U R))

Proof state:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ ↑(coveringOfPresieve U R i)

Tactic:
obtain ⟨V, iVU, ⟨W, iVW, iWU, hiWU, -⟩, hxV⟩ := hR x hxU

Result:
case a.intro.intro.intro.intro.intro.intro.intro
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
V : Opens ↑X
iVU : V ⟶ U
hxV : x ∈ V
W : Opens ↑X
iVW : V ⟶ W
iWU : W ⟶ U
hiWU : R iWU
⊢ ∃ i, x ∈ ↑(coveringOfPresieve U R i)

Proof state:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup (coveringOfPresieve U R))

Tactic:
rw [Opens.coe_iSup, Set.mem_iUnion]

Result:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ ↑(coveringOfPresieve U R i)