-- 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.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
x : ↑↑X.toPresheafedSpace
hx : ∀ i ∈ σ, x ∉ (U i).carrier
⊢ t' ∈ (fun a => (ConcreteCategory.hom fT.base) a) '' Z

Tactic:
obtain ⟨z, rfl, hzr⟩ := exists_preimage_pullback x t' (Subsingleton.elim (f.base x) (q.base t'))

Result:
case intro.intro.intro.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
z : ↑↑(pullback f q).toPresheafedSpace
hzr : (ConcreteCategory.hom (pullback.snd f q).base) z = t'
hx : ∀ i ∈ σ, (ConcreteCategory.hom (pullback.fst f q).base) z ∉ (U i).carrier
⊢ t' ∈ (fun a => (ConcreteCategory.hom fT.base) a) '' Z

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
⊢ t ∈ Zc

Tactic:
intro ⟨z, hz, hzt⟩

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
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
z : ↑↑(pullback f q).toPresheafedSpace
hz : z ∈ Z
hzt : (ConcreteCategory.hom fT.base) z = t
⊢ False

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 : ∃ a, ∀ i ∈ σ, a ∉ (U i).carrier
⊢ t' ∈ (fun a => (ConcreteCategory.hom fT.base) a) '' Z

Tactic:
obtain ⟨x, hx⟩ := h

Result:
case intro.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
x : ↑↑X.toPresheafedSpace
hx : ∀ i ∈ σ, x ∉ (U i).carrier
⊢ t' ∈ (fun a => (ConcreteCategory.hom fT.base) a) '' Z