-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
lemma Spec_iff {R : CommRingCat} {f : X ⟶ Spec R} :
    IsClosedImmersion f ↔ ∃ I : Ideal R, ∃ e : X ≅ Spec (.of <| R ⧸ I),
      f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Proof state:
case mp
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ IsClosedImmersion f → ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Tactic:
intro H

Result:
case mp
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
⊢ ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Proof state:
case mp.intro.refine_1
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ Function.Bijective ⇑φ.hom'.kerLift

Tactic:
exact ⟨φ.1.kerLift_injective, Ideal.Quotient.lift_surjective_of_surjective _ _
  (h₂.comp (Scheme.ΓSpecIso R).commRingCatIsoToRingEquiv.symm.surjective)⟩

Result:
no goals

Proof state:
case mp.intro.refine_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ f =
    X.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')) ≫
          (RingEquiv.ofBijective φ.hom'.kerLift ⋯).toCommRingCatIso.hom)

Tactic:
show f = X.isoSpec.hom ≫ Spec.map φ

Result:
case mp.intro.refine_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ f = X.isoSpec.hom ≫ Spec.map φ

Proof state:
case mpr.intro.intro
X : Scheme
R : CommRingCat
I : Ideal ↑R
e : X ≅ Spec (CommRingCat.of (↑R ⧸ I))
⊢ IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))

Tactic:
infer_instance

Result:
no goals

Proof state:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ IsClosedImmersion f ↔ ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Tactic:
constructor

Result:
case mp
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ IsClosedImmersion f → ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

case mpr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ (∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) → IsClosedImmersion f

Proof state:
case mp.intro.refine_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ f = X.isoSpec.hom ≫ Spec.map φ

Tactic:
simp only [Scheme.isoSpec, asIso_hom, Spec.map_comp, ← Scheme.toSpecΓ_naturality_assoc,
  ← SpecMap_ΓSpecIso_hom, φ]

Result:
case mp.intro.refine_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ f = f ≫ Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv

Proof state:
case mp.intro.refine_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ f =
    (X.isoSpec ≪≫ Scheme.Spec.mapIso (RingEquiv.ofBijective φ.hom'.kerLift ⋯).toCommRingCatIso.op).hom ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')))

Tactic:
simp only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Scheme.Spec_map,
  Quiver.Hom.unop_op, Category.assoc, ← Spec.map_comp]

Result:
case mp.intro.refine_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ f =
    X.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')) ≫
          (RingEquiv.ofBijective φ.hom'.kerLift ⋯).toCommRingCatIso.hom)

Proof state:
case mp.intro
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Tactic:
let φ := (Scheme.ΓSpecIso R).inv ≫ f.appTop

Result:
case mp.intro
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Proof state:
case mp.intro
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Tactic:
refine ⟨RingHom.ker φ.1, Scheme.isoSpec _ ≪≫ Scheme.Spec.mapIso
    (.op (RingEquiv.ofBijective φ.1.kerLift ?_).toCommRingCatIso), ?_⟩

Result:
case mp.intro.refine_1
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ Function.Bijective ⇑φ.hom'.kerLift

case mp.intro.refine_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ f =
    (X.isoSpec ≪≫
          Scheme.Spec.mapIso (RingEquiv.ofBijective φ.hom'.kerLift ?mp.intro.refine_1).toCommRingCatIso.op).hom ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (RingHom.ker φ.hom')))

Proof state:
case mpr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ (∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) → IsClosedImmersion f

Tactic:
rintro ⟨I, e, rfl⟩

Result:
case mpr.intro.intro
X : Scheme
R : CommRingCat
I : Ideal ↑R
e : X ≅ Spec (CommRingCat.of (↑R ⧸ I))
⊢ IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))

Proof state:
case mp.intro.refine_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : R ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso R).inv ≫ Scheme.Hom.appTop f
⊢ f = f ≫ Spec.map (Scheme.ΓSpecIso R).hom ≫ Spec.map (Scheme.ΓSpecIso R).inv

Tactic:
simp only [← Spec.map_comp, Iso.inv_hom_id, Spec.map_id, Category.comp_id]

Result:
no goals

Proof state:
case mp
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
⊢ ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Tactic:
obtain ⟨h₁, h₂⟩ := IsClosedImmersion.isAffine_surjective_of_isAffine f

Result:
case mp.intro
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H : IsClosedImmersion f
h₁ : IsAffine X
h₂ : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))