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

Proof state:
case a.inr.intro.intro.refine_2
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)
this✝ : x ∈ closure (Set.range ⇑(ConcreteCategory.hom (Cover.pullbackHom 𝒰 f i).base))
this :
  (ConcreteCategory.hom (𝒰.map i).base) x ∈
    closure (Set.range ⇑(ConcreteCategory.hom ((Cover.pullbackCover 𝒰 f).map i ≫ f).base))
⊢ (ConcreteCategory.hom (𝒰.map i).base) x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
exact closure_mono (Set.range_comp_subset_range _ _) this

Result:
no goals

Proof state:
case intro.intro
X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst✝ : QuasiCompact (Spec.map φ)
⊢ (ker (Spec.map φ)).support ⊆ closure (Set.range ⇑(ConcreteCategory.hom (Spec.map φ).base))

Tactic:
rw [ker_of_isAffine, support_ofIdealTop, Spec_zeroLocus, ← Ideal.coe_comap,
  RingHom.comap_ker, ← PrimeSpectrum.closure_range_comap, ← CommRingCat.hom_comp,
  ← Scheme.ΓSpecIso_inv_naturality]

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

Proof state:
case a.inr
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
x : ↑↑Y.toPresheafedSpace
hx : x ∈ f.ker.support
𝒰 : Y.OpenCover := Y.affineCover
⊢ x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x

Result:
case a.inr.intro.intro
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
⊢ (ConcreteCategory.hom (𝒰.map i).base) x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Proof state:
case intro.inr
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
⊢ x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
obtain ⟨_, ⟨i, rfl⟩, hx⟩ := (f.iUnion_support_ker_openCover_map_comp 𝒰).ge hx

Result:
case intro.inr.intro.intro.intro
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
⊢ x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Proof state:
case intro.inr
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 ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
let 𝒰 := X.affineCover.finiteSubcover

Result:
case intro.inr
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
⊢ x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Proof state:
X✝ Y✝ X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
hY : ∃ S, Y = Spec S
⊢ f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
obtain ⟨S, rfl⟩ := hY

Result:
case intro
X✝ Y X : Scheme
S : CommRingCat
f : X.Hom (Spec S)
inst✝ : QuasiCompact f
⊢ f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Proof state:
case a.inr
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
⊢ f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
intro x hx

Result:
case a.inr
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
x : ↑↑Y.toPresheafedSpace
hx : x ∈ f.ker.support
⊢ x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Proof state:
case a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑(ConcreteCategory.hom f.base)) ⊆ f.ker.support

Tactic:
rw [(isClosed_support _).closure_subset_iff]

Result:
case a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
⊢ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ f.ker.support

Proof state:
case a.inr
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
x : ↑↑Y.toPresheafedSpace
hx : x ∈ f.ker.support
⊢ x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
let 𝒰 := Y.affineCover

Result:
case a.inr
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
x : ↑↑Y.toPresheafedSpace
hx : x ∈ f.ker.support
𝒰 : Y.OpenCover := Y.affineCover
⊢ x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))