-- 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:
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
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
let t : T := (Spec.map <| CommRingCat.ofHom ψ.toRingHom).base default

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
⊢ 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))
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
let q : T ⟶ Spec (.of K) := Spec.map (CommRingCat.ofHom MvPolynomial.C)

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)
⊢ 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
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
let Zc : T.Opens := ⟨(fT.base '' Z)ᶜ, (fT.isClosedMap _ hZ).isOpen_compl⟩

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' := ⋯ }
⊢ 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
z : ↑↑(pullback f q).toPresheafedSpace
hz : z ∈ Z
hzt : (ConcreteCategory.hom fT.base) z = t
⊢ ∃ i, (ConcreteCategory.hom fT.base) z ∈ Ti i ∧ (ConcreteCategory.hom p.base) z ∈ U i

Tactic:
exact ⟨𝒰.f (p.base z), hzt ▸ ht _, by simpa [U] using 𝒰.covers (p.base z)⟩

Result:
no goals

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))ᶜ
⊢ IsClosed Z

Tactic:
simp only [Z, isClosed_compl_iff, Opens.coe_iSup, Opens.coe_inf, Opens.map_coe]

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))ᶜ
⊢ IsOpen (⋃ i, ⇑(ConcreteCategory.hom fT.base) ⁻¹' ↑(Ti i) ∩ ⇑(ConcreteCategory.hom p.base) ⁻¹' ↑(U i))