-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
/-- A surjective closed immersion is an isomorphism when the target is reduced. -/
lemma isIso_of_isClosedImmersion_of_surjective {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsClosedImmersion f] [Surjective f] [IsReduced Y] :
    IsIso f

Proof state:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
⊢ Function.Surjective (ConcreteCategory.hom (Scheme.Hom.appTop f)).specComap

Tactic:
have : Surjective (Spec.map (f.appTop)) :=
  (MorphismProperty.arrow_mk_iso_iff @Surjective (arrowIsoSpecΓOfIsAffine f)).mp
  (inferInstanceAs (Surjective f))

Result:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
this : Surjective (Spec.map (Scheme.Hom.appTop f))
⊢ Function.Surjective (ConcreteCategory.hom (Scheme.Hom.appTop f)).specComap

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
⊢ ∀ (i : Y.affineCover.1), MorphismProperty.isomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
intro i

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
i : Y.affineCover.1
⊢ MorphismProperty.isomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
⊢ IsIso f

Tactic:
refine (IsLocalAtTarget.iff_of_openCover (P := .isomorphisms Scheme) Y.affineCover).mpr ?_

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
⊢ ∀ (i : Y.affineCover.1), MorphismProperty.isomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)

Proof state:
case hf
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
obtain ⟨hX, hf⟩ := HasAffineProperty.iff_of_isAffine.mp ‹IsClosedImmersion f›

Result:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Proof state:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
suffices RingHom.ker φ.hom ≤ nilradical _ by
  rwa [nilradical_eq_zero, Submodule.zero_eq_bot, le_bot_iff,
    ← RingHom.injective_iff_ker_eq_bot] at this

Result:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
⊢ RingHom.ker (CommRingCat.Hom.hom φ) ≤ nilradical ↑Γ(Y, ⊤)