-- Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean
nonrec lemma LocallyOfFiniteType.jacobsonSpace
  (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace Y] : JacobsonSpace X

Proof state:
case intro.intro
R : CommRingCat
inst✝¹ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
this : (CommRingCat.Hom.hom φ).FiniteType
⊢ JacobsonSpace ↑↑(Spec S).toPresheafedSpace

Tactic:
algebraize [φ.hom]

Result:
case intro.intro
R : CommRingCat
inst✝¹ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
this : (CommRingCat.Hom.hom φ).FiniteType
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
⊢ JacobsonSpace ↑↑(Spec S).toPresheafedSpace

Proof state:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
hX : ∃ S, X = Spec S
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

Tactic:
obtain ⟨S, rfl⟩ := hX

Result:
case intro
R : CommRingCat
inst✝¹ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
S : CommRingCat
f : Spec S ⟶ Spec R
inst✝ : LocallyOfFiniteType f
⊢ JacobsonSpace ↑↑(Spec S).toPresheafedSpace

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑Y.toPresheafedSpace
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

Tactic:
wlog hY : ∃ S, Y = Spec S

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑Y.toPresheafedSpace
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : LocallyOfFiniteType f] [inst : JacobsonSpace ↑↑Y.toPresheafedSpace],
    (∃ S, Y = Spec S) → JacobsonSpace ↑↑X.toPresheafedSpace
hY : ¬∃ S, Y = Spec S
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑Y.toPresheafedSpace
hY : ∃ S, Y = Spec S
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑Y.toPresheafedSpace
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : LocallyOfFiniteType f] [inst : JacobsonSpace ↑↑Y.toPresheafedSpace],
    (∃ S, Y = Spec S) → JacobsonSpace ↑↑X.toPresheafedSpace
hY : ¬∃ S, Y = Spec S
i : (Scheme.Cover.pullbackCover Y.affineCover f).J
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Scheme.Cover.pullbackCover Y.affineCover f).map i))

Tactic:
have inst : LocallyOfFiniteType (Y.affineCover.pullbackHom f i) :=
  MorphismProperty.pullback_snd _ _ inferInstance

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑Y.toPresheafedSpace
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : LocallyOfFiniteType f] [inst : JacobsonSpace ↑↑Y.toPresheafedSpace],
    (∃ S, Y = Spec S) → JacobsonSpace ↑↑X.toPresheafedSpace
hY : ¬∃ S, Y = Spec S
i : (Scheme.Cover.pullbackCover Y.affineCover f).J
inst : LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Scheme.Cover.pullbackCover Y.affineCover f).map i))

Proof state:
case intro.inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
this✝ :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [inst : LocallyOfFiniteType f]
    [inst : JacobsonSpace ↑↑(Spec R).toPresheafedSpace], (∃ S, X = Spec S) → JacobsonSpace ↑↑X.toPresheafedSpace
hX : ¬∃ S, X = Spec S
inst : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
i : X.affineCover.J
this : JacobsonSpace ↑↑(X.affineCover.obj i).toPresheafedSpace
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange (X.affineCover.map i))

Tactic:
let e := Homeomorph.ofIsEmbedding _ (X.affineCover.map i).isOpenEmbedding.isEmbedding

Result:
case intro.inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
this✝ :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [inst : LocallyOfFiniteType f]
    [inst : JacobsonSpace ↑↑(Spec R).toPresheafedSpace], (∃ S, X = Spec S) → JacobsonSpace ↑↑X.toPresheafedSpace
hX : ¬∃ S, X = Spec S
inst : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
i : X.affineCover.J
this : JacobsonSpace ↑↑(X.affineCover.obj i).toPresheafedSpace
e : ↑↑(X.affineCover.obj i).toPresheafedSpace ≃ₜ ↑(Set.range ⇑(ConcreteCategory.hom (X.affineCover.map i).base)) :=
  Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom (X.affineCover.map i).base) ⋯
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange (X.affineCover.map i))

Proof state:
case intro
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

Tactic:
wlog hX : ∃ S, X = Spec S

Result:
case intro.inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [inst : LocallyOfFiniteType f]
    [inst : JacobsonSpace ↑↑(Spec R).toPresheafedSpace], (∃ S, X = Spec S) → JacobsonSpace ↑↑X.toPresheafedSpace
hX : ¬∃ S, X = Spec S
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
hX : ∃ S, X = Spec S
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

Proof state:
case intro.inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [inst : LocallyOfFiniteType f]
    [inst : JacobsonSpace ↑↑(Spec R).toPresheafedSpace], (∃ S, X = Spec S) → JacobsonSpace ↑↑X.toPresheafedSpace
hX : ¬∃ S, X = Spec S
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

Tactic:
have inst : JacobsonSpace (Spec R) := ‹_›

Result:
case intro.inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [inst : LocallyOfFiniteType f]
    [inst : JacobsonSpace ↑↑(Spec R).toPresheafedSpace], (∃ S, X = Spec S) → JacobsonSpace ↑↑X.toPresheafedSpace
hX : ¬∃ S, X = Spec S
inst : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

Proof state:
case intro.inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
this✝ :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [inst : LocallyOfFiniteType f]
    [inst : JacobsonSpace ↑↑(Spec R).toPresheafedSpace], (∃ S, X = Spec S) → JacobsonSpace ↑↑X.toPresheafedSpace
hX : ¬∃ S, X = Spec S
inst : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
i : X.affineCover.J
this : JacobsonSpace ↑↑(X.affineCover.obj i).toPresheafedSpace
e : ↑↑(X.affineCover.obj i).toPresheafedSpace ≃ₜ ↑(Set.range ⇑(ConcreteCategory.hom (X.affineCover.map i).base)) :=
  Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom (X.affineCover.map i).base) ⋯
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange (X.affineCover.map i))

Tactic:
exact .of_isClosedEmbedding e.symm.isClosedEmbedding

Result:
no goals