-- Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
theorem isField_of_universallyClosed (f : X ⟶ Spec (.of K)) [IsIntegral X] [UniversallyClosed f] :
    IsField Γ(X, ⊤)

Proof state:
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
⊢ IsField ↑Γ(X, ⊤)

Tactic:
let F := (Scheme.ΓSpecIso _).inv ≫ f.appTop

Result:
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
⊢ IsField ↑Γ(X, ⊤)

Proof state:
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
⊢ (CommRingCat.Hom.hom F).IsIntegral

Tactic:
apply RingHom.isIntegral_respectsIso.2 (e := (Scheme.ΓSpecIso _).symm.commRingCatIsoToRingEquiv)

Result:
case x
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
⊢ (Scheme.Hom.appTop f).hom'.IsIntegral

Proof state:
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
this : (CommRingCat.Hom.hom F).IsIntegral
⊢ IsField ↑Γ(X, ⊤)

Tactic:
algebraize [F.hom]

Result:
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
this : (CommRingCat.Hom.hom F).IsIntegral
algInst✝ : Algebra ↑(CommRingCat.of K) ↑Γ(X, ⊤) := (CommRingCat.Hom.hom F).toAlgebra
algebraizeInst✝ : Algebra.IsIntegral ↑(CommRingCat.of K) ↑Γ(X, ⊤)
⊢ IsField ↑Γ(X, ⊤)

Proof state:
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
⊢ IsField ↑Γ(X, ⊤)

Tactic:
have : F.hom.IsIntegral := by
  apply RingHom.isIntegral_respectsIso.2 (e := (Scheme.ΓSpecIso _).symm.commRingCatIsoToRingEquiv)
  exact isIntegral_appTop_of_universallyClosed f

Result:
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
this : (CommRingCat.Hom.hom F).IsIntegral
⊢ IsField ↑Γ(X, ⊤)

Proof state:
case x
X : Scheme
K : Type u
inst✝² : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝¹ : IsIntegral X
inst✝ : UniversallyClosed f
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
⊢ (Scheme.Hom.appTop f).hom'.IsIntegral

Tactic:
exact isIntegral_appTop_of_universallyClosed f

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
F : CommRingCat.of K ⟶ Γ(X, ⊤) := (Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ Scheme.Hom.appTop f
this : (CommRingCat.Hom.hom F).IsIntegral
algInst✝ : Algebra ↑(CommRingCat.of K) ↑Γ(X, ⊤) := (CommRingCat.Hom.hom F).toAlgebra
algebraizeInst✝ : Algebra.IsIntegral ↑(CommRingCat.of K) ↑Γ(X, ⊤)
⊢ IsField ↑Γ(X, ⊤)

Tactic:
exact isField_of_isIntegral_of_isField' (Field.toIsField K)

Result:
no goals