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

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
inst✝¹ : LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
inst✝ : JacobsonSpace ↑↑Y.toPresheafedSpace
inst : JacobsonSpace ↑↑(Y.affineCover.obj i).toPresheafedSpace
e : ↑↑((Scheme.Cover.pullbackCover Y.affineCover f).obj i).toPresheafedSpace ≃ₜ
  ↑(Set.range ⇑(ConcreteCategory.hom ((Scheme.Cover.pullbackCover Y.affineCover f).map i).base)) :=
  Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom ((Scheme.Cover.pullbackCover Y.affineCover f).map i).base) ⋯
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Scheme.Cover.pullbackCover Y.affineCover f).map i))

Tactic:
have := this (Y.affineCover.pullbackHom f i) ⟨_, rfl⟩

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)
inst✝ : JacobsonSpace ↑↑Y.toPresheafedSpace
inst : JacobsonSpace ↑↑(Y.affineCover.obj i).toPresheafedSpace
e : ↑↑((Scheme.Cover.pullbackCover Y.affineCover f).obj i).toPresheafedSpace ≃ₜ
  ↑(Set.range ⇑(ConcreteCategory.hom ((Scheme.Cover.pullbackCover Y.affineCover f).map i).base)) :=
  Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom ((Scheme.Cover.pullbackCover Y.affineCover f).map i).base) ⋯
this : JacobsonSpace ↑↑((Scheme.Cover.pullbackCover Y.affineCover f).obj i).toPresheafedSpace
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Scheme.Cover.pullbackCover Y.affineCover f).map i))

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
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
⊢ JacobsonSpace ↑↑(Spec S).toPresheafedSpace

Tactic:
have := PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mpr ‹_›

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
this : IsJacobsonRing ↑R
⊢ JacobsonSpace ↑↑(Spec S).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
inst✝ : LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
inst : JacobsonSpace ↑↑Y.toPresheafedSpace
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Scheme.Cover.pullbackCover Y.affineCover f).map i))

Tactic:
have inst : JacobsonSpace (Y.affineCover.obj i) :=
  .of_isOpenEmbedding (Y.affineCover.map i).isOpenEmbedding

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)
inst✝ : JacobsonSpace ↑↑Y.toPresheafedSpace
inst : JacobsonSpace ↑↑(Y.affineCover.obj i).toPresheafedSpace
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange ((Scheme.Cover.pullbackCover Y.affineCover f).map i))

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
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
this : IsJacobsonRing ↑R
⊢ JacobsonSpace ↑↑(Spec S).toPresheafedSpace

Tactic:
exact PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace.mp (isJacobsonRing_of_finiteType (A := R))

Result:
no goals

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

Tactic:
obtain ⟨R, rfl⟩ := hY

Result:
case intro
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
⊢ 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
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

Tactic:
rw [(Scheme.OpenCover.isOpenCover_opensRange (Y.affineCover.pullbackCover f)).jacobsonSpace_iff]

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),
    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), JacobsonSpace ↥(Scheme.Hom.opensRange (X.affineCover.map i))

Tactic:
intro i

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
⊢ JacobsonSpace ↥(Scheme.Hom.opensRange (X.affineCover.map i))

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

Tactic:
have : RingHom.FiniteType φ.hom := HasRingHomProperty.Spec_iff.mp ‹_›

Result:
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