-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
lemma isCompact_iff_exists {U : X.Opens} :
    IsCompact (U : Set X) ↔ ∃ R, ∃ f : Spec R ⟶ X, Set.range f.base = U

Proof state:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
⊢ Function.Surjective ⇑(ConcreteCategory.hom (IsOpenImmersion.lift U.ι f ⋯).base)

Tactic:
rw [← Set.range_eq_univ]

Result:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
⊢ Set.range ⇑(ConcreteCategory.hom (IsOpenImmersion.lift U.ι f ⋯).base) = Set.univ

Proof state:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)
R : CommRingCat
f : Spec R ⟶ ↑U
hf : Function.Surjective ⇑(ConcreteCategory.hom f.base)
⊢ Set.range ⇑(ConcreteCategory.hom (f ≫ U.ι).base) = ↑U

Tactic:
simp [hf.range_comp]

Result:
no goals

Proof state:
case a
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
⊢ (fun a => (ConcreteCategory.hom U.ι.base) a) ''
      Set.range ⇑(ConcreteCategory.hom (IsOpenImmersion.lift U.ι f ⋯).base) =
    ↑U

Tactic:
rwa [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.comp_base, IsOpenImmersion.lift_fac]

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
⊢ ∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)

Tactic:
refine ⟨R, IsOpenImmersion.lift U.ι f (by simp [hf]), ?_⟩

Result:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
⊢ Function.Surjective ⇑(ConcreteCategory.hom (IsOpenImmersion.lift U.ι f ⋯).base)

Proof state:
case a
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
⊢ (fun x => ⇑(ConcreteCategory.hom U.ι.base) '' x)
      (Set.range ⇑(ConcreteCategory.hom (IsOpenImmersion.lift U.ι f ⋯).base)) =
    (fun x => ⇑(ConcreteCategory.hom U.ι.base) '' x) Set.univ

Tactic:
simp only [Set.image_univ, Scheme.Opens.range_ι]

Result:
case a
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
⊢ (fun a => (ConcreteCategory.hom U.ι.base) a) ''
      Set.range ⇑(ConcreteCategory.hom (IsOpenImmersion.lift U.ι f ⋯).base) =
    ↑U

Proof state:
X : Scheme
U : X.Opens
⊢ IsCompact ↑U ↔ ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U

Tactic:
refine isCompact_iff_compactSpace.trans ((compactSpace_iff_exists (X := U)).trans ?_)

Result:
X : Scheme
U : X.Opens
⊢ (∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)) ↔ ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U

Proof state:
X : Scheme
U : X.Opens
⊢ (∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)) ↔ ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U

Tactic:
refine ⟨fun ⟨R, f, hf⟩ ↦ ⟨R, f ≫ U.ι, by simp [hf.range_comp]⟩, fun ⟨R, f, hf⟩ ↦ ?_⟩

Result:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
⊢ ∃ R f, Function.Surjective ⇑(ConcreteCategory.hom f.base)

Proof state:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑(ConcreteCategory.hom f.base) = ↑U
⊢ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ Set.range ⇑(ConcreteCategory.hom U.ι.base)

Tactic:
simp [hf]

Result:
no goals