-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma Hom.support_ker (f : X.Hom Y) [QuasiCompact f] :
    f.ker.support = closure (Set.range f.base)

Proof state:
X✝ Y X : Scheme
S : CommRingCat
f : X.Hom (Spec S)
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X.Hom (Spec S)) [inst : QuasiCompact f],
    (∃ R, X = Spec R) → f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))
hX : ¬∃ R, X = Spec R
x : ↑↑(Spec S).toPresheafedSpace
hx✝ : x ∈ f.ker.support
inst : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.J
hx : x ∈ (fun i => (ker (𝒰.map i ≫ f)).support) i
⊢ CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace

Tactic:
show CompactSpace (Spec _)

Result:
X✝ Y X : Scheme
S : CommRingCat
f : X.Hom (Spec S)
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X.Hom (Spec S)) [inst : QuasiCompact f],
    (∃ R, X = Spec R) → f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))
hX : ¬∃ R, X = Spec R
x : ↑↑(Spec S).toPresheafedSpace
hx✝ : x ∈ f.ker.support
inst : CompactSpace ↑↑X.toPresheafedSpace
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.J
hx : x ∈ (fun i => (ker (𝒰.map i ≫ f)).support) i
⊢ CompactSpace ↑↑(Spec ⋯.choose).toPresheafedSpace

Proof state:
case a.inr.intro.intro.refine_1
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
this :
  ∀ {X Y : Scheme} (f : X.Hom Y) [inst : QuasiCompact f],
    (∃ S, Y = Spec S) → f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hx : (ConcreteCategory.hom (𝒰.map i).base) x ∈ f.ker.support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (ConcreteCategory.hom (𝒰.map i).base) x ∈
    Y.zeroLocus ↑(f.ker.ideal ⟨𝒰.map i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩) ∩ Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base)

Tactic:
exact ⟨((support_inter _ _).le ⟨hx, by simp⟩).1, ⟨_, rfl⟩⟩

Result:
no goals

Proof state:
case a.inr.intro.intro.refine_1
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
this :
  ∀ {X Y : Scheme} (f : X.Hom Y) [inst : QuasiCompact f],
    (∃ S, Y = Spec S) → f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hx : (ConcreteCategory.hom (𝒰.map i).base) x ∈ f.ker.support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ x ∈ (𝒰.obj i).zeroLocus ↑((ker (Cover.pullbackHom 𝒰 f i)).ideal ⟨⊤, ⋯⟩)

Tactic:
rw [← (𝒰.map i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
  ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i)
    ((𝒰.pullbackCover f).map i) (𝒰.map i) (IsPullback.of_hasPullback _ _).flip,
  Ideal.coe_comap, Set.image_preimage_eq]

Result:
case a.inr.intro.intro.refine_1
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
this :
  ∀ {X Y : Scheme} (f : X.Hom Y) [inst : QuasiCompact f],
    (∃ S, Y = Spec S) → f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hx : (ConcreteCategory.hom (𝒰.map i).base) x ∈ f.ker.support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (ConcreteCategory.hom (𝒰.map i).base) x ∈
    Y.zeroLocus ↑(f.ker.ideal ⟨𝒰.map i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩) ∩ Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base)

case a.inr.intro.intro.refine_1.h
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
this :
  ∀ {X Y : Scheme} (f : X.Hom Y) [inst : QuasiCompact f],
    (∃ S, Y = Spec S) → f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.J
x : ↑↑(𝒰.obj i).toPresheafedSpace
hx : (ConcreteCategory.hom (𝒰.map i).base) x ∈ f.ker.support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (appIso (𝒰.map i) ↑⟨⊤, ⋯⟩).inv)

Proof state:
case intro.intro
X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst✝ : QuasiCompact (Spec.map φ)
⊢ closure (Set.range ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom (φ ≫ (ΓSpecIso R).inv)))) ⊆
    closure (Set.range ⇑(ConcreteCategory.hom (Spec.map φ).base))

Tactic:
simp only [CommRingCat.hom_comp, PrimeSpectrum.comap_comp, ContinuousMap.coe_comp]

Result:
case intro.intro
X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst✝ : QuasiCompact (Spec.map φ)
⊢ closure
      (Set.range
        (⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom φ)) ∘
          ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv)))) ⊆
    closure (Set.range ⇑(ConcreteCategory.hom (Spec.map φ).base))