-- 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 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
inst : QuasiCompact (𝒰.map i ≫ f)
⊢ x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
exact closure_mono (Set.range_comp_subset_range _ _) (this S (𝒰.map i ≫ f) ⟨_, rfl⟩ hx)

Result:
no goals

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
⊢ f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
intro x hx

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

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 φ)) ∘
          ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv)))) ⊆
    closure (Set.range ⇑(ConcreteCategory.hom (Spec.map φ).base))

Tactic:
exact closure_mono (Set.range_comp_subset_range _ (Spec.map φ).base)

Result:
no goals

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

Tactic:
apply subset_antisymm

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

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

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

Tactic:
have := image_closure_subset_closure_image (f := (𝒰.map i).base)
  (𝒰.map i).base.1.2 (Set.mem_image_of_mem _ this)

Result:
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 (⇑(ConcreteCategory.hom (𝒰.map i).base) '' Set.range ⇑(ConcreteCategory.hom (Cover.pullbackHom 𝒰 f i).base))
⊢ (ConcreteCategory.hom (𝒰.map i).base) x ∈ closure (Set.range ⇑(ConcreteCategory.hom 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 ↑↑(Spec ⋯.choose).toPresheafedSpace

Tactic:
infer_instance

Result:
no goals

Proof state:
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
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (ConcreteCategory.hom (𝒰.map i).base) x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
have := this (𝒰.pullbackHom f i) ⟨_, rfl⟩
  ((support_inter _ ⟨⊤, isAffineOpen_top _⟩).ge ⟨?_, Set.mem_univ x⟩).1

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

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 ⟨⊤, ⋯⟩)

Proof state:
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 ∈ ↑↑⟨𝒰.map i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩

Tactic:
simp

Result:
no goals

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

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

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
⊢ f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))

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