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

Tactic:
exact isOpen_iUnion fun i ↦ (fT.continuous.1 _ (Ti i).2).inter (p.continuous.1 _ (U i).2)

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))ᶜ
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

Tactic:
suffices ∃ i, fT.base z ∈ Ti i ∧ p.base z ∈ U i from hz (by simpa)

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
⊢ ∃ i, (ConcreteCategory.hom fT.base) z ∈ Ti i ∧ (ConcreteCategory.hom p.base) z ∈ U i

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

Tactic:
let p : pullback f q ⟶ X := pullback.fst f q

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

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

Tactic:
let φ : MvPolynomial 𝒰.J K →+* MvPolynomial 𝒰.J K :=
  (MvPolynomial.aeval fun i : 𝒰.J ↦ if i ∈ σ then MvPolynomial.X i else 0).toRingHom

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