-- 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
⊢ ⋃ i ∈ s, ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f) = ⋃ i ∈ Set.range g, ↑↑i

Tactic:
apply le_antisymm <;> apply Set.iUnion₂_subset

Result:
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 ∈ s, ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f) ⊆ ⋃ i ∈ Set.range g, ↑↑i

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 ∈ Set.range g, ↑↑i ⊆ ⋃ i ∈ s, ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f)

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
⊢ X.toRingedSpace.basicOpen ((ConcreteCategory.hom (X.toRingedSpace.presheaf.map this.op)) f) ∈ X.affineOpens

Tactic:
exact IsAffineOpen.basicOpen V.1.prop _

Result:
no goals

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
⊢ ∃ s, s.Finite ∧ ↑(X.basicOpen f) = ⋃ i ∈ s, ↑↑i

Tactic:
let g : s → X.affineOpens := by
  intro V
  use V.1 ⊓ X.basicOpen f
  have : V.1.1 ⟶ U := by
    apply homOfLE; change _ ⊆ (U : Set X); rw [e]
    convert Set.subset_iUnion₂ (s := fun (U : X.affineOpens) (_ : U ∈ s) => (U : Set X))
      V V.prop using 1
  erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op]
  exact IsAffineOpen.basicOpen V.1.prop _

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, ⋯⟩
⊢ ∃ s, s.Finite ∧ ↑(X.basicOpen f) = ⋃ 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
V : ↑s
⊢ ↑↑V ⟶ U

Tactic:
apply homOfLE

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 ≤ U

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⟩) ⊆ ⋃ i ∈ s, ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f)

Tactic:
refine Set.Subset.trans ?_ (Set.subset_iUnion₂ j hj)

Result:
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)

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
⊢ ∃ s, s.Finite ∧ ↑(X.basicOpen f) = ⋃ i ∈ s, ↑↑i

Tactic:
refine ⟨Set.range g, Set.finite_range g, ?_⟩

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
⊢ ↑(X.basicOpen f) = ⋃ i ∈ Set.range g, ↑↑i

Proof state:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
⊢ IsCompact ↑(X.basicOpen f)

Tactic:
refine ((isCompactOpen_iff_eq_finset_affine_union _).mpr ?_).1

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

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
⊢ ↑↑V ⊓ X.basicOpen f ∈ X.affineOpens

Tactic:
have : V.1.1 ⟶ U := by
  apply homOfLE; change _ ⊆ (U : Set X); rw [e]
  convert Set.subset_iUnion₂ (s := fun (U : X.affineOpens) (_ : U ∈ s) => (U : Set X))
    V V.prop using 1

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
⊢ ↑↑V ⊓ X.basicOpen f ∈ X.affineOpens

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⟩
⊢ ↑↑⟨i, hi⟩ ⊆ ⋃ i ∈ s, ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f)

Tactic:
rw [← hj']

Result:
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⟩) ⊆ ⋃ i ∈ s, ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f)

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 ∈ s, ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f) ⊆ ⋃ i ∈ Set.range g, ↑↑i

Tactic:
intro i hi

Result:
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

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 ∈ Set.range g, ↑↑i ⊆ ⋃ i ∈ s, ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f)

Tactic:
rintro ⟨i, hi⟩ ⟨⟨j, hj⟩, hj'⟩

Result:
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⟩
⊢ ↑↑⟨i, hi⟩ ⊆ ⋃ i ∈ s, ↑↑i ∩ ↑(X.toRingedSpace.basicOpen f)

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, ⋯⟩
⊢ ∃ s, s.Finite ∧ ↑(X.basicOpen f) = ⋃ i ∈ s, ↑↑i

Tactic:
haveI : Finite s := hs.to_subtype

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
⊢ ∃ 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:
change _ ⊆ (U : Set X)

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 ⊆ ↑U