-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
lemma compactSpace_iff_exists :
    CompactSpace X ↔ ∃ R, ∃ f : Spec R ⟶ X, Function.Surjective f.base

Proof state:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (x : 𝒰.J), IsAffine (𝒰.obj x)
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((∐ 𝒰.obj).isoSpec.inv ≫ Sigma.desc 𝒰.map).base)

Tactic:
refine Function.Surjective.comp (g := (Sigma.desc 𝒰.map).base)
  (fun x ↦ ?_) (∐ 𝒰.obj).isoSpec.inv.surjective

Result:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (x : 𝒰.J), IsAffine (𝒰.obj x)
x : ↑↑X.toPresheafedSpace
⊢ ∃ a, (ConcreteCategory.hom (Sigma.desc 𝒰.map).base) a = x

Proof state:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (x : 𝒰.J), IsAffine (𝒰.obj x)
x : ↑↑X.toPresheafedSpace
⊢ ∃ a, (ConcreteCategory.hom (Sigma.desc 𝒰.map).base) a = x

Tactic:
obtain ⟨y, hy⟩ := 𝒰.covers x

Result:
case intro
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (x : 𝒰.J), IsAffine (𝒰.obj x)
x : ↑↑X.toPresheafedSpace
y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace
hy : (ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) y = x
⊢ ∃ a, (ConcreteCategory.hom (Sigma.desc 𝒰.map).base) a = x

Proof state:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (x : 𝒰.J), IsAffine (𝒰.obj x)
x : ↑↑X.toPresheafedSpace
y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace
hy : (ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) y = x
⊢ (ConcreteCategory.hom (Sigma.desc 𝒰.map).base) ((ConcreteCategory.hom (Sigma.ι 𝒰.obj (𝒰.f x)).base) y) = x

Tactic:
rw [← Scheme.comp_base_apply, Sigma.ι_desc, hy]

Result:
no goals

Proof state:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (x : 𝒰.J), IsAffine (𝒰.obj x)
⊢ ∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)

Tactic:
refine ⟨Γ(∐ 𝒰.obj, ⊤), (∐ 𝒰.obj).isoSpec.inv ≫ Sigma.desc 𝒰.map, ?_⟩

Result:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (x : 𝒰.J), IsAffine (𝒰.obj x)
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((∐ 𝒰.obj).isoSpec.inv ≫ Sigma.desc 𝒰.map).base)

Proof state:
case intro
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (x : 𝒰.J), IsAffine (𝒰.obj x)
x : ↑↑X.toPresheafedSpace
y : ↑↑(𝒰.obj (𝒰.f x)).toPresheafedSpace
hy : (ConcreteCategory.hom (𝒰.map (𝒰.f x)).base) y = x
⊢ ∃ a, (ConcreteCategory.hom (Sigma.desc 𝒰.map).base) a = x

Tactic:
exact ⟨(Sigma.ι 𝒰.obj (𝒰.f x)).base y, by rw [← Scheme.comp_base_apply, Sigma.ι_desc, hy]⟩

Result:
no goals

Proof state:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ ∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)

Tactic:
have (x : 𝒰.J) : IsAffine (𝒰.obj x) := X.isAffine_affineCover _

Result:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (x : 𝒰.J), IsAffine (𝒰.obj x)
⊢ ∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)

Proof state:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
⊢ ∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)

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

Result:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ ∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)

Proof state:
X : Scheme
⊢ CompactSpace ↑↑X.toPresheafedSpace ↔ ∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨R, f, hf⟩ ↦ ⟨hf.range_eq ▸ isCompact_range f.continuous⟩⟩

Result:
X : Scheme
h : CompactSpace ↑↑X.toPresheafedSpace
⊢ ∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)