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

Tactic:
have inst : JacobsonSpace Y := ‹_›

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

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

Tactic:
exact .of_isClosedEmbedding e.symm.isClosedEmbedding

Result:
no goals

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:
have := this _ (X.affineCover.map i ≫ f) ⟨_, rfl⟩

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

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:
intro i

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 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))

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

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) ⋯
⊢ 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
⊢ JacobsonSpace ↑↑X.toPresheafedSpace

Tactic:
rw [X.affineCover.isOpenCover_opensRange.jacobsonSpace_iff]

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))