-- Mathlib/AlgebraicGeometry/FunctionField.lean
theorem IsAffineOpen.primeIdealOf_genericPoint {X : Scheme} [IsIntegral X] {U : X.Opens}
    (hU : IsAffineOpen U) [h : Nonempty U] :
    hU.primeIdealOf
        ⟨genericPoint X,
          ((genericPoint_spec X).mem_open_set_iff U.isOpen).mpr (by simpa using h)⟩ =
      genericPoint (Spec Γ(X, U))

Proof state:
case h.e'_2.h.h.e'_6
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
e_1✝ : PrimeSpectrum ↑Γ(X, U) = ↑↑(Spec (X.presheaf.obj (op U))).toPresheafedSpace
⊢ ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = genericPoint ↑↑(↑U).toPresheafedSpace

Tactic:
apply Subtype.ext

Result:
case h.e'_2.h.h.e'_6.a
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
e_1✝ : PrimeSpectrum ↑Γ(X, U) = ↑↑(Spec (X.presheaf.obj (op U))).toPresheafedSpace
⊢ ↑⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = ↑(genericPoint ↑↑(↑U).toPresheafedSpace)

Proof state:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ hU.primeIdealOf ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = genericPoint ↑↑(Spec Γ(X, U)).toPresheafedSpace

Tactic:
haveI : IsAffine _ := hU

Result:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
⊢ hU.primeIdealOf ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = genericPoint ↑↑(Spec Γ(X, U)).toPresheafedSpace

Proof state:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
⊢ (ConcreteCategory.hom hU.isoSpec.hom.base) ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ =
    genericPoint ↑↑(Spec Γ(X, U)).toPresheafedSpace

Tactic:
convert
  genericPoint_eq_of_isOpenImmersion
    (U.toScheme.isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top).op))

Result:
case h.e'_2.h.h.e'_6
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
e_1✝ : PrimeSpectrum ↑Γ(X, U) = ↑↑(Spec (X.presheaf.obj (op U))).toPresheafedSpace
⊢ ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = genericPoint ↑↑(↑U).toPresheafedSpace

Proof state:
case h.e'_2.h.h.e'_6.a
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
e_1✝ : PrimeSpectrum ↑Γ(X, U) = ↑↑(Spec (X.presheaf.obj (op U))).toPresheafedSpace
⊢ ↑⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = ↑(genericPoint ↑↑(↑U).toPresheafedSpace)

Tactic:
exact (genericPoint_eq_of_isOpenImmersion U.ι).symm

Result:
no goals

Proof state:
X✝ : Scheme
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ (Set.univ ∩ ↑U).Nonempty

Tactic:
simpa using h

Result:
no goals

Proof state:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
⊢ hU.primeIdealOf ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = genericPoint ↑↑(Spec Γ(X, U)).toPresheafedSpace

Tactic:
delta IsAffineOpen.primeIdealOf

Result:
X : Scheme
inst✝ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
⊢ (ConcreteCategory.hom hU.isoSpec.hom.base) ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ =
    genericPoint ↑↑(Spec Γ(X, U)).toPresheafedSpace