-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
theorem isCompact_basicOpen (X : Scheme) {U : X.Opens} (hU : IsCompact (U : Set X))
    (f : Γ(X, U)) : IsCompact (X.basicOpen f : Set X)

Proof state:
case intro.intro
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
g : ↑s → ↑X.affineOpens := fun V => ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ ↑U ∩ ↑(X.toRingedSpace.basicOpen f) = ⋃ i ∈ Set.range g, ↑↑i

Tactic:
rw [e, Set.iUnion₂_inter]

Result:
case intro.intro
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
g : ↑s → ↑X.affineOpens := fun V => ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ ⋃ i ∈ s, ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f) = ⋃ i ∈ Set.range g, ↑↑i

Proof state:
case intro.intro.a.h.mk.intro.mk
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
g : ↑s → ↑X.affineOpens := fun V => ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
i : X.Opens
hi : i ∈ X.affineOpens
j : ↑X.affineOpens
hj : j ∈ s
hj' : g ⟨j, hj⟩ = ⟨i, hi⟩
⊢ ↑↑(g ⟨j, hj⟩) ⊆ ↑↑j ∩ ↑(X.toRingedSpace.basicOpen f)

Tactic:
exact Set.Subset.rfl

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
⊢ ∃ s, s.Finite ∧ ↑(X.basicOpen f) = ⋃ i ∈ s, ↑↑i

Tactic:
obtain ⟨s, hs, e⟩ := (isCompactOpen_iff_eq_finset_affine_union _).mp ⟨hU, U.isOpen⟩

Result:
case intro.intro
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
⊢ ∃ s, s.Finite ∧ ↑(X.basicOpen f) = ⋃ i ∈ s, ↑↑i

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
V : ↑s
⊢ ↑↑↑V ⊆ ↑U

Tactic:
rw [e]

Result:
case h
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
V : ↑s
⊢ ↑↑↑V ⊆ ⋃ i ∈ s, ↑↑i

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
⊢ ↑s → ↑X.affineOpens

Tactic:
intro V

Result:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
V : ↑s
⊢ ↑X.affineOpens

Proof state:
case intro.intro.a.h
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
g : ↑s → ↑X.affineOpens := fun V => ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
i : ↑X.affineOpens
hi : i ∈ s
⊢ ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f) ⊆ ⋃ i ∈ Set.range g, ↑↑i

Tactic:
exact Set.Subset.trans (Set.Subset.rfl : _ ≤ g ⟨i, hi⟩)
  (@Set.subset_iUnion₂ _ _ _
    (fun (i : X.affineOpens) (_ : i ∈ Set.range g) => (i : Set X.toPresheafedSpace)) _
    (Set.mem_range_self ⟨i, hi⟩))

Result:
no goals

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
V : ↑s
⊢ ↑↑↑V ⊆ ⋃ i ∈ s, ↑↑i

Tactic:
convert Set.subset_iUnion₂ (s := fun (U : X.affineOpens) (_ : U ∈ s) => (U : Set X))
  V V.prop using 1

Result:
no goals

Proof state:
case property
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
V : ↑s
this : ↑↑V ⟶ U
⊢ ↑↑V ⊓ X.basicOpen f ∈ X.affineOpens

Tactic:
erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op]

Result:
case property
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
V : ↑s
this : ↑↑V ⟶ U
⊢ X.toRingedSpace.basicOpen ((ConcreteCategory.hom (X.toRingedSpace.presheaf.map this.op)) f) ∈ X.affineOpens

Proof state:
case intro.intro
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
g : ↑s → ↑X.affineOpens := fun V => ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ ↑(X.basicOpen f) = ⋃ i ∈ Set.range g, ↑↑i

Tactic:
refine (Set.inter_eq_right.mpr
          (SetLike.coe_subset_coe.2 <| RingedSpace.basicOpen_le _ _)).symm.trans ?_

Result:
case intro.intro
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
g : ↑s → ↑X.affineOpens := fun V => ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ ↑U ∩ ↑(X.toRingedSpace.basicOpen f) = ⋃ i ∈ Set.range g, ↑↑i

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
V : ↑s
⊢ ↑X.affineOpens

Tactic:
use V.1 ⊓ X.basicOpen f

Result:
case property
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : ↑U = ⋃ i ∈ s, ↑↑i
V : ↑s
⊢ ↑↑V ⊓ X.basicOpen f ∈ X.affineOpens