-- 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
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base)

Tactic:
wlog hY : ∃ R, Y = Spec R

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
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base)

X✝ Y✝ X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
H : SpecializingMap ⇑(ConcreteCategory.hom f.base)
hY : ∃ R, Y = Spec R
⊢ 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
i : Y.affineCover.1
hqc : QuasiCompact (Scheme.Cover.pullbackHom Y.affineCover f i)
⊢ topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
refine this (Y.affineCover.pullbackHom f i) ?_ ⟨_, rfl⟩

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)
⊢ SpecializingMap ⇑(ConcreteCategory.hom (Scheme.Cover.pullbackHom Y.affineCover f i).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
i : Y.affineCover.1
hqc : QuasiCompact (Scheme.Cover.pullbackHom Y.affineCover f i)
⊢ SpecializingMap ⇑(ConcreteCategory.hom (Scheme.Cover.pullbackHom Y.affineCover f i).base)

Tactic:
exact IsLocalAtTarget.of_isPullback
  (P := topologically @SpecializingMap) (.of_hasPullback _ _) H

Result:
no goals

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

Tactic:
replace H := hZ.stableUnderSpecialization.image H

Result:
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)

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

Tactic:
intros Z hZ

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