-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
/-- If `f : X ⟶ Y` is a morphism of schemes with quasi-compact source and affine target, `f`
has a closed image and `f` induces an injection on global sections, then
`f` is surjective. -/
lemma surjective_of_isClosed_range_of_injective [CompactSpace X]
    (hfcl : IsClosed (Set.range f.base)) (hfinj : Function.Injective (f.appTop)) :
    Function.Surjective f.base

Proof state:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
⊢ s ∈ ↑(nilradical ↑Γ(Y, ⊤))

Tactic:
simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
  Submodule.mem_toAddSubmonoid, SetLike.mem_coe, mem_nilradical, ← IsNilpotent.map_iff hfinj]

Result:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
⊢ IsNilpotent ((ConcreteCategory.hom (Scheme.Hom.appTop f)) s)

Proof state:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
i : 𝒰.J
x : ↥⊤
h : (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (𝒰.map i).base) ↑x) ∉ Y.basicOpen s
⊢ (ConcreteCategory.hom (Scheme.Hom.residueFieldMap (𝒰.map i ≫ f) ↑x))
      ((ConcreteCategory.hom (Y.Γevaluation ((ConcreteCategory.hom (𝒰.map i ≫ f).base) ↑x))) s) =
    0

Tactic:
simpa only [Scheme.comp_base, TopCat.coe_comp, Function.comp_apply,
  Scheme.residueFieldMap_comp, CommRingCat.comp_apply, map_eq_zero,
  Scheme.evaluation_eq_zero_iff_not_mem_basicOpen]

Result:
no goals

Proof state:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
⊢ IsNilpotent ((ConcreteCategory.hom (Scheme.Hom.appTop f)) s)

Tactic:
refine Scheme.isNilpotent_of_isNilpotent_cover _ 𝒰 (fun i ↦ ?_)

Result:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
i : 𝒰.J
⊢ IsNilpotent ((ConcreteCategory.hom (Scheme.Hom.app (𝒰.map i) ⊤)) ((ConcreteCategory.hom (Scheme.Hom.appTop f)) s))

Proof state:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ Set.range ⇑(ConcreteCategory.hom f.base) = Set.univ

Tactic:
apply hI ▸ (Scheme.zeroLocus_eq_top_iff_subset_nilradical _).mpr

Result:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ ↑I ⊆ ↑(nilradical ↑Γ(Y, ⊤))

Proof state:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ ↑I ⊆ ↑(nilradical ↑Γ(Y, ⊤))

Tactic:
intro s hs

Result:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
⊢ s ∈ ↑(nilradical ↑Γ(Y, ⊤))

Proof state:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
i : 𝒰.J
x : ↥⊤
⊢ (ConcreteCategory.hom ((𝒰.obj i).evaluation ⊤ ↑x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app (𝒰.map i) ⊤)) ((ConcreteCategory.hom (Scheme.Hom.appTop f)) s)) =
    0

Tactic:
suffices h : f.base ((𝒰.map i).base x.val) ∉ Y.basicOpen s by
  erw [← Scheme.Γevaluation_naturality_apply (𝒰.map i ≫ f)]
  simpa only [Scheme.comp_base, TopCat.coe_comp, Function.comp_apply,
    Scheme.residueFieldMap_comp, CommRingCat.comp_apply, map_eq_zero,
    Scheme.evaluation_eq_zero_iff_not_mem_basicOpen]

Result:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
i : 𝒰.J
x : ↥⊤
⊢ (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (𝒰.map i).base) ↑x) ∉ Y.basicOpen s