-- 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✝ 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)

Tactic:
obtain ⟨S, rfl⟩ := hY

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

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

Tactic:
have := this _ (g ≫ f) (g.base ⁻¹' Z) (hZ.preimage g.continuous)

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)
inst : QuasiCompact (g ≫ f)
this :
  StableUnderSpecialization (⇑(ConcreteCategory.hom (g ≫ f).base) '' (⇑(ConcreteCategory.hom g.base) ⁻¹' Z)) →
    (∃ R_1, Spec R = Spec R_1) →
      IsClosed (⇑(ConcreteCategory.hom (g ≫ f).base) '' (⇑(ConcreteCategory.hom g.base) ⁻¹' Z))
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

Proof state:
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)
⊢ CompactSpace ↑↑(Spec R).toPresheafedSpace

Tactic:
infer_instance

Result:
no goals

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

Tactic:
obtain ⟨R, rfl⟩ := hX

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

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
⊢ topologically (@IsClosedMap) f

Tactic:
rw [IsLocalAtTarget.iff_of_openCover (P := topologically @IsClosedMap) Y.affineCover]

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

Tactic:
have inst : QuasiCompact (g ≫ f) := HasAffineProperty.iff_of_isAffine.mpr (by infer_instance)

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)
inst : QuasiCompact (g ≫ f)
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

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 (g ≫ f).base) '' (⇑(ConcreteCategory.hom g.base) ⁻¹' Z)) →
    (∃ R_1, Spec R = Spec R_1) →
      IsClosed (⇑(ConcreteCategory.hom (g ≫ f).base) '' (⇑(ConcreteCategory.hom g.base) ⁻¹' Z))
⊢ IsClosed (⇑(ConcreteCategory.hom f.base) '' Z)

Tactic:
simp_rw [Scheme.comp_base, TopCat.comp_app, ← Set.image_image,
  Set.image_preimage_eq _ hg] at this

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