-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
@[stacks 01K9]
lemma isClosedMap_iff_specializingMap (f : X ⟶ Y) [QuasiCompact f] :
    IsClosedMap f.base ↔ SpecializingMap f.base

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base) ↔ SpecializingMap ⇑(ConcreteCategory.hom f.base)

Tactic:
refine ⟨fun h ↦ h.specializingMap, fun H ↦ ?_⟩

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base)

Proof state:
case intro
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↑↑X.toPresheafedSpace
hZ : IsClosed Z
H : StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z)
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

Tactic:
wlog hX : ∃ R, X = Spec R

Result:
case intro.inr
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↑↑X.toPresheafedSpace
hZ : IsClosed Z
H : StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z)
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [inst : QuasiCompact f] (Z : Set ↑↑X.toPresheafedSpace),
    IsClosed Z →
      StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z) →
        (∃ R, X = Spec R) → IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)
hX : ¬∃ R, X = Spec R
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↑↑X.toPresheafedSpace
hZ : IsClosed Z
H : StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z)
hX : ∃ R, X = Spec R
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

Proof state:
case intro.inr
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↑↑X.toPresheafedSpace
hZ : IsClosed Z
H : StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z)
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [inst : QuasiCompact f] (Z : Set ↑↑X.toPresheafedSpace),
    IsClosed Z →
      StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z) →
        (∃ R, X = Spec R) → IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)
hX : ¬∃ R, X = Spec R
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

Tactic:
obtain ⟨R, g, hg⟩ :=
  compactSpace_iff_exists.mp ((quasiCompact_over_affine_iff f).mp inferInstance)

Result:
case intro.inr.intro.intro
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↑↑X.toPresheafedSpace
hZ : IsClosed Z
H : StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z)
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [inst : QuasiCompact f] (Z : Set ↑↑X.toPresheafedSpace),
    IsClosed Z →
      StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z) →
        (∃ R, X = Spec R) → IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)
hX : ¬∃ R, X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective ⇑(ConcreteCategory.hom g.base)
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : QuasiCompact f],
    SpecializingMap ⇑(ConcreteCategory.hom f.base) → (∃ R, Y = Spec R) → IsClosedMap ⇑(ConcreteCategory.hom f.base)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.1
⊢ topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
haveI hqc : QuasiCompact (Y.affineCover.pullbackHom f i) :=
    IsLocalAtTarget.of_isPullback (.of_hasPullback _ _) inferInstance

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : QuasiCompact f],
    SpecializingMap ⇑(ConcreteCategory.hom f.base) → (∃ R, Y = Spec R) → IsClosedMap ⇑(ConcreteCategory.hom f.base)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.1
hqc : QuasiCompact (Scheme.Cover.pullbackHom Y.affineCover f i)
⊢ topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)

Proof state:
case intro
S R : CommRingCat
f : Spec R ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↑↑(Spec R).toPresheafedSpace
hZ : IsClosed Z
H : StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z)
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

Tactic:
obtain ⟨φ, rfl⟩ := Spec.homEquiv.symm.surjective f

Result:
case intro.intro
S R : CommRingCat
Z : Set ↑↑(Spec R).toPresheafedSpace
hZ : IsClosed Z
φ : S ⟶ R
inst✝ : QuasiCompact (Spec.homEquiv.symm φ)
H : StableUnderSpecialization (⇑(ConcreteCategory.hom (Spec.homEquiv.symm φ).base) '' Z)
⊢ IsClosed (⇑(ConcreteCategory.hom (Spec.homEquiv.symm φ).base) '' Z)

Proof state:
case intro
X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base)

Tactic:
clear * - H

Result:
case intro
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base)

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : QuasiCompact f],
    SpecializingMap ⇑(ConcreteCategory.hom f.base) → (∃ R, Y = Spec R) → IsClosedMap ⇑(ConcreteCategory.hom f.base)
hY : ¬∃ R, Y = Spec R
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base)

Tactic:
show topologically @IsClosedMap f

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : QuasiCompact f],
    SpecializingMap ⇑(ConcreteCategory.hom f.base) → (∃ R, Y = Spec R) → IsClosedMap ⇑(ConcreteCategory.hom f.base)
hY : ¬∃ R, Y = Spec R
⊢ topologically (@IsClosedMap) f

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : QuasiCompact f],
    SpecializingMap ⇑(ConcreteCategory.hom f.base) → (∃ R, Y = Spec R) → IsClosedMap ⇑(ConcreteCategory.hom f.base)
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.1), topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
intro i

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : QuasiCompact f],
    SpecializingMap ⇑(ConcreteCategory.hom f.base) → (∃ R, Y = Spec R) → IsClosedMap ⇑(ConcreteCategory.hom f.base)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.1
⊢ topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)

Proof state:
case intro.inr.intro.intro
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↑↑X.toPresheafedSpace
hZ : IsClosed Z
H : StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z)
this✝ :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [inst : QuasiCompact f] (Z : Set ↑↑X.toPresheafedSpace),
    IsClosed Z →
      StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z) →
        (∃ R, X = Spec R) → IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)
hX : ¬∃ R, X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective ⇑(ConcreteCategory.hom g.base)
inst : QuasiCompact (g ≫ f)
this :
  StableUnderSpecialization (⇑(ConcreteCategory.hom f.base) '' Z) →
    (∃ R_1, Spec R = Spec R_1) → IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

Tactic:
exact this H ⟨_, rfl⟩

Result:
no goals

Proof state:
case intro.intro
S R : CommRingCat
Z : Set ↑↑(Spec R).toPresheafedSpace
hZ : IsClosed Z
φ : S ⟶ R
inst✝ : QuasiCompact (Spec.homEquiv.symm φ)
H : StableUnderSpecialization (⇑(ConcreteCategory.hom (Spec.homEquiv.symm φ).base) '' Z)
⊢ IsClosed (⇑(ConcreteCategory.hom (Spec.homEquiv.symm φ).base) '' Z)

Tactic:
exact PrimeSpectrum.isClosed_image_of_stableUnderSpecialization φ.hom Z hZ H

Result:
no goals