-- 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
i : 𝒰.J
x : ↥⊤
⊢ (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (𝒰.map i).base) ↑x) ∉ Y.basicOpen s

Tactic:
exact (Y.mem_zeroLocus_iff I _).mp (hI ▸ Set.mem_range_self ((𝒰.map i).base x.val)) s hs

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
⊢ Function.Surjective ⇑(ConcreteCategory.hom f.base)

Tactic:
haveI (i : 𝒰.J) : IsAffine (𝒰.obj i) := Scheme.isAffine_affineCover X _

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)
⊢ Function.Surjective ⇑(ConcreteCategory.hom 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
i : 𝒰.J
⊢ IsNilpotent ((ConcreteCategory.hom (Scheme.Hom.app (𝒰.map i) ⊤)) ((ConcreteCategory.hom (Scheme.Hom.appTop f)) s))

Tactic:
rw [Scheme.isNilpotent_iff_basicOpen_eq_bot]

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
⊢ (𝒰.obj i).basicOpen
      ((ConcreteCategory.hom (Scheme.Hom.app (𝒰.map i) ⊤)) ((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))
⊢ Function.Surjective ⇑(ConcreteCategory.hom f.base)

Tactic:
obtain ⟨I, hI⟩ := (Scheme.eq_zeroLocus_of_isClosed_of_isAffine Y (Set.range f.base)).mp hfcl

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
⊢ Function.Surjective ⇑(ConcreteCategory.hom 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
⊢ Function.Surjective ⇑(ConcreteCategory.hom f.base)

Tactic:
let 𝒰 : X.OpenCover := X.affineCover.finiteSubcover

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
⊢ Function.Surjective ⇑(ConcreteCategory.hom 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
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:
intro x

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 ((𝒰.obj i).evaluation ⊤ ↑x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app (𝒰.map i) ⊤)) ((ConcreteCategory.hom (Scheme.Hom.appTop f)) s)) =
    0

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)
⊢ Function.Surjective ⇑(ConcreteCategory.hom f.base)

Tactic:
apply Set.range_eq_univ.mp

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)
⊢ Set.range ⇑(ConcreteCategory.hom f.base) = Set.univ