-- Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
theorem finite_appTop_of_universallyClosed (f : X ⟶ Spec (.of K))
    [IsIntegral X] [UniversallyClosed f] [LocallyOfFiniteType f] :
    f.appTop.hom.Finite

Proof state:
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this✝¹ : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
this✝ : Field ↑Γ(X, ⊤) := ⋯.toField
this : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ ↑⟨U, hU⟩ ≤ f ⁻¹ᵁ ↑⟨⊤, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
  (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Result:
case intro.intro.intro.intro.intro
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Proof state:
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
have x : X := Nonempty.some inferInstance

Result:
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
letI := (isField_of_universallyClosed K f).toField

Result:
case intro.intro.intro.intro.intro
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this✝ : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
this : Field ↑Γ(X, ⊤) := ⋯.toField
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Proof state:
case intro.intro.intro.intro.intro.hfg
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this✝¹ : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
this✝ : Field ↑Γ(X, ⊤) := ⋯.toField
this : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).comp (CommRingCat.Hom.hom (Scheme.Hom.appTop f))).FiniteType

Tactic:
exact LocallyOfFiniteType.finiteType_of_affine_subset ⟨⊤, isAffineOpen_top _⟩ ⟨U, hU⟩ (by simp)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this✝ : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
this : Field ↑Γ(X, ⊤) := ⋯.toField
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
have : Nonempty U := ⟨⟨x, hxU⟩⟩

Result:
case intro.intro.intro.intro.intro
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this✝¹ : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
this✝ : Field ↑Γ(X, ⊤) := ⋯.toField
this : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
letI := ((Scheme.ΓSpecIso (.of K)).commRingCatIsoToRingEquiv.toMulEquiv.isField
  _ (Field.toIsField K)).toField

Result:
case intro.intro.intro.intro.intro
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this✝¹ : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
this✝ : Field ↑Γ(X, ⊤) := ⋯.toField
this : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
apply RingHom.finite_of_algHom_finiteType_of_isJacobsonRing (A := Γ(X, U))
  (g := (X.presheaf.map (homOfLE le_top).op).hom)

Result:
case intro.intro.intro.intro.intro.hfg
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this✝¹ : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
this✝ : Field ↑Γ(X, ⊤) := ⋯.toField
this : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).comp (CommRingCat.Hom.hom (Scheme.Hom.appTop f))).FiniteType