-- 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
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
⊢ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ f.ker.support

Tactic:
exact f.range_subset_ker_support

Result:
no goals

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

Tactic:
have inst : QuasiCompact (𝒰.map i ≫ f) := HasAffineProperty.iff_of_isAffine.mpr
  (by show CompactSpace (Spec _); infer_instance)

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

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

Tactic:
have inst : QuasiCompact (𝒰.pullbackHom f i) :=
  MorphismProperty.pullback_snd _ _ inferInstance

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
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (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
hX : ∃ R, X = Spec R
⊢ f.ker.support ⊆ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
obtain ⟨R, rfl⟩ := hX

Result:
case intro
X Y : Scheme
S R : CommRingCat
f : (Spec R).Hom (Spec S)
inst✝ : QuasiCompact f
⊢ f.ker.support ⊆ 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
⊢ x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›

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

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

Tactic:
exact (ConcreteCategory.bijective_of_isIso ((𝒰.map i).appIso ⊤).inv).2

Result:
no goals

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

Tactic:
rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.comp_base, 𝒰.pullbackHom_map] at 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 (Set.range ⇑(ConcreteCategory.hom ((Cover.pullbackCover 𝒰 f).map i ≫ f).base))
⊢ (ConcreteCategory.hom (𝒰.map i).base) x ∈ closure (Set.range ⇑(ConcreteCategory.hom f.base))

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

Tactic:
wlog hX : ∃ R, X = Spec R generalizing X S

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

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

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

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

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