-- 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
⊢ ∀ (a : ↑↑X.toPresheafedSpace), ∃ i, ∃ (_ : i ∈ σ), a ∈ (U i).carrier

Tactic:
contrapose! h

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 : ∃ a, ∀ i ∈ σ, a ∉ (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
z : ↑↑(pullback f q).toPresheafedSpace
hz : z ∈ Z
hzt : (ConcreteCategory.hom fT.base) z = t
⊢ (ConcreteCategory.hom p.base) z ∈ U (𝒰.f ((ConcreteCategory.hom p.base) z))

Tactic:
simpa [U] using 𝒰.covers (p.base z)

Result:
no goals

Proof state:
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

Tactic:
suffices ∀ i, t ∈ (Ti i).comap (comap φ) → p.base z ∉ U i from ⟨z, by simpa [Z, p, fT, hzr], hzr⟩

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
⊢ ∀ (i : 𝒰.J), t ∈ (Opens.comap (comap φ)) (Ti i) → (ConcreteCategory.hom p.base) z ∉ U i