-- Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
/-- If `X` is universally closed over a field, then `X` is quasi-compact. -/
lemma compactSpace_of_universallyClosed
    {K} [Field K] (f : X ⟶ Spec (.of K)) [UniversallyClosed f] : CompactSpace X

Proof state:
case intro.intro.intro.intro
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.J → X.Opens := fun i => Scheme.Hom.opensRange (𝒰.map i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.J K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.J → T.Opens := fun i => basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↑↑(pullback f q).toPresheafedSpace := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑(ConcreteCategory.hom fT.base) '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.J K →ₐ[K] K := aeval fun x => 1
t : ↑↑T.toPresheafedSpace := (ConcreteCategory.hom (Spec.map (CommRingCat.ofHom ψ.toRingHom)).base) default
ht : ∀ (i : 𝒰.J), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.J K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.J := vars g
φ : MvPolynomial 𝒰.J K →+* MvPolynomial 𝒰.J K := (aeval fun i => if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↑↑T.toPresheafedSpace := (ConcreteCategory.hom (Spec.map (CommRingCat.ofHom φ)).base) t
ht'g : t' ∈ basicOpen g
h : t' ∉ ⇑(ConcreteCategory.hom fT.base) '' Z
⊢ ⋃ i ∈ σ, (U i).carrier = Set.univ

Tactic:
rw [Set.iUnion₂_eq_univ_iff]

Result:
case intro.intro.intro.intro
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.J → X.Opens := fun i => Scheme.Hom.opensRange (𝒰.map i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.J K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.J → T.Opens := fun i => basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↑↑(pullback f q).toPresheafedSpace := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑(ConcreteCategory.hom fT.base) '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.J K →ₐ[K] K := aeval fun x => 1
t : ↑↑T.toPresheafedSpace := (ConcreteCategory.hom (Spec.map (CommRingCat.ofHom ψ.toRingHom)).base) default
ht : ∀ (i : 𝒰.J), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.J K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.J := vars g
φ : MvPolynomial 𝒰.J K →+* MvPolynomial 𝒰.J K := (aeval fun i => if i ∈ σ then MvPolynomial.X i else 0).toRingHom
t' : ↑↑T.toPresheafedSpace := (ConcreteCategory.hom (Spec.map (CommRingCat.ofHom φ)).base) t
ht'g : t' ∈ basicOpen g
h : t' ∉ ⇑(ConcreteCategory.hom fT.base) '' Z
⊢ ∀ (a : ↑↑X.toPresheafedSpace), ∃ i, ∃ (_ : i ∈ σ), a ∈ (U i).carrier

Proof state:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.J → X.Opens := fun i => Scheme.Hom.opensRange (𝒰.map i)
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
let T : Scheme := Spec (.of <| MvPolynomial 𝒰.J K)

Result:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.J → X.Opens := fun i => Scheme.Hom.opensRange (𝒰.map i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.J K))
⊢ CompactSpace ↑↑X.toPresheafedSpace

Proof state:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.J → X.Opens := fun i => Scheme.Hom.opensRange (𝒰.map i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.J K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.J → T.Opens := fun i => basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↑↑(pullback f q).toPresheafedSpace := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑(ConcreteCategory.hom fT.base) '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.J K →ₐ[K] K := aeval fun x => 1
t : ↑↑T.toPresheafedSpace := (ConcreteCategory.hom (Spec.map (CommRingCat.ofHom ψ.toRingHom)).base) default
ht : ∀ (i : 𝒰.J), t ∈ Ti i
htZc : t ∈ Zc
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
obtain ⟨U', ⟨g, rfl⟩, htU', hU'le⟩ := Opens.isBasis_iff_nbhd.mp isBasis_basic_opens htZc

Result:
case intro.intro.intro.intro
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.J → X.Opens := fun i => Scheme.Hom.opensRange (𝒰.map i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.J K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.J → T.Opens := fun i => basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↑↑(pullback f q).toPresheafedSpace := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑(ConcreteCategory.hom fT.base) '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.J K →ₐ[K] K := aeval fun x => 1
t : ↑↑T.toPresheafedSpace := (ConcreteCategory.hom (Spec.map (CommRingCat.ofHom ψ.toRingHom)).base) default
ht : ∀ (i : 𝒰.J), t ∈ Ti i
htZc : t ∈ Zc
g : ↑(CommRingCat.of (MvPolynomial 𝒰.J K))
htU' : t ∈ basicOpen g
hU'le : basicOpen g ≤ Zc
⊢ CompactSpace ↑↑X.toPresheafedSpace

Proof state:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
let 𝒰 : X.OpenCover := X.affineCover

Result:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
⊢ CompactSpace ↑↑X.toPresheafedSpace

Proof state:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.J → X.Opens := fun i => Scheme.Hom.opensRange (𝒰.map i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.J K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.J → T.Opens := fun i => basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↑↑(pullback f q).toPresheafedSpace := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
have hZ : IsClosed Z := by
  simp only [Z, isClosed_compl_iff, Opens.coe_iSup, Opens.coe_inf, Opens.map_coe]
  exact isOpen_iUnion fun i ↦ (fT.continuous.1 _ (Ti i).2).inter (p.continuous.1 _ (U i).2)

Result:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.J → X.Opens := fun i => Scheme.Hom.opensRange (𝒰.map i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.J K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : 𝒰.J → T.Opens := fun i => basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↑↑(pullback f q).toPresheafedSpace := (↑(⨆ i, fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i))ᶜ
hZ : IsClosed Z
⊢ CompactSpace ↑↑X.toPresheafedSpace