-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
theorem spec_of_surjective {R S : CommRingCat} (f : R ⟶ S) (h : Function.Surjective f) :
    IsClosedImmersion (Spec.map f) where
  base_closed := PrimeSpectrum.isClosedEmbedding_comap_of_surjective _ _ h
  surj_on_stalks x

Proof state:
R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↑↑(Spec S).toPresheafedSpace
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f

Tactic:
exact RingHom.surjective_respectsIso

Result:
no goals

Proof state:
R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↑↑(Spec S).toPresheafedSpace
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (Spec.map f) x))

Tactic:
apply (MorphismProperty.arrow_mk_iso_iff
  (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f))
  (Scheme.arrowStalkMapSpecIso f x)).mpr

Result:
R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↑↑(Spec S).toPresheafedSpace
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso
⊢ RingHom.toMorphismProperty (fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f)
    (CommRingCat.ofHom
      (Localization.localRingHom ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) x).asIdeal x.asIdeal
        (CommRingCat.Hom.hom f) ⋯))

Proof state:
R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↑↑(Spec S).toPresheafedSpace
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso
⊢ RingHom.toMorphismProperty (fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f)
    (CommRingCat.ofHom
      (Localization.localRingHom ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) x).asIdeal x.asIdeal
        (CommRingCat.Hom.hom f) ⋯))

Tactic:
exact RingHom.surjective_localRingHom_of_surjective f.hom h x.asIdeal

Result:
no goals

Proof state:
R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↑↑(Spec S).toPresheafedSpace
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (Spec.map f) x))

Tactic:
haveI : (RingHom.toMorphismProperty (fun f ↦ Function.Surjective f)).RespectsIso := by
  rw [← RingHom.toMorphismProperty_respectsIso_iff]
  exact RingHom.surjective_respectsIso

Result:
R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↑↑(Spec S).toPresheafedSpace
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (Spec.map f) x))

Proof state:
R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↑↑(Spec S).toPresheafedSpace
⊢ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f).RespectsIso

Tactic:
rw [← RingHom.toMorphismProperty_respectsIso_iff]

Result:
R S : CommRingCat
f : R ⟶ S
h : Function.Surjective ⇑(ConcreteCategory.hom f)
x : ↑↑(Spec S).toPresheafedSpace
⊢ RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f