-- Mathlib/AlgebraicGeometry/FunctionField.lean
theorem functionField_isFractionRing_of_isAffineOpen [IsIntegral X] (U : X.Opens)
    (hU : IsAffineOpen U) [Nonempty U] :
    IsFractionRing Γ(X, U) X.functionField

Proof state:
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ IsFractionRing ↑Γ(X, U) ↑X.functionField

Tactic:
haveI : IsAffine _ := hU

Result:
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
⊢ IsFractionRing ↑Γ(X, U) ↑X.functionField

Proof state:
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : IsAffine ↑U
this : IsIntegral ↑U
⊢ IsLocalization (nonZeroDivisors ↑Γ(X, U)) ↑(X.presheaf.stalk (genericPoint ↑↑X.toPresheafedSpace))

Tactic:
convert hU.isLocalization_stalk ⟨genericPoint X,
  (((genericPoint_spec X).mem_open_set_iff U.isOpen).mpr (by simpa using ‹Nonempty U›))⟩ using 1

Result:
case h.e'_3.h
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : IsAffine ↑U
this : IsIntegral ↑U
⊢ nonZeroDivisors ↑Γ(X, U) = (hU.primeIdealOf ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩).asIdeal.primeCompl

Proof state:
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
⊢ IsFractionRing ↑Γ(X, U) ↑X.functionField

Tactic:
haveI : IsIntegral U :=
  @isIntegral_of_isAffine_of_isDomain _ _ _
    (by rw [Scheme.Opens.toScheme_presheaf_obj, Opens.isOpenEmbedding_obj_top]; infer_instance)

Result:
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : IsAffine ↑U
this : IsIntegral ↑U
⊢ IsFractionRing ↑Γ(X, U) ↑X.functionField

Proof state:
case h.e'_3.h.h
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : IsAffine ↑U
this : IsIntegral ↑U
x✝ : ↑Γ(X, U)
⊢ x✝ ∈ nonZeroDivisors ↑Γ(X, U) ↔ x✝ ∈ ⊥.asIdeal.primeCompl

Tactic:
exact mem_nonZeroDivisors_iff_ne_zero

Result:
no goals

Proof state:
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : IsAffine ↑U
this : IsIntegral ↑U
⊢ IsFractionRing ↑Γ(X, U) ↑X.functionField

Tactic:
delta IsFractionRing Scheme.functionField

Result:
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : IsAffine ↑U
this : IsIntegral ↑U
⊢ IsLocalization (nonZeroDivisors ↑Γ(X, U)) ↑(X.presheaf.stalk (genericPoint ↑↑X.toPresheafedSpace))

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

Tactic:
simpa using ‹Nonempty U›

Result:
no goals

Proof state:
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
⊢ IsDomain ↑Γ(X, U)

Tactic:
infer_instance

Result:
no goals

Proof state:
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
⊢ IsDomain ↑Γ(↑U, ⊤)

Tactic:
rw [Scheme.Opens.toScheme_presheaf_obj, Opens.isOpenEmbedding_obj_top]

Result:
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this : IsAffine ↑U
⊢ IsDomain ↑Γ(X, U)

Proof state:
case h.e'_3.h
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : IsAffine ↑U
this : IsIntegral ↑U
⊢ nonZeroDivisors ↑Γ(X, U) = ⊥.asIdeal.primeCompl

Tactic:
ext

Result:
case h.e'_3.h.h
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : IsAffine ↑U
this : IsIntegral ↑U
x✝ : ↑Γ(X, U)
⊢ x✝ ∈ nonZeroDivisors ↑Γ(X, U) ↔ x✝ ∈ ⊥.asIdeal.primeCompl

Proof state:
case h.e'_3.h
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : IsAffine ↑U
this : IsIntegral ↑U
⊢ nonZeroDivisors ↑Γ(X, U) = (hU.primeIdealOf ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩).asIdeal.primeCompl

Tactic:
rw [hU.primeIdealOf_genericPoint, genericPoint_eq_bot_of_affine]

Result:
case h.e'_3.h
X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : IsAffine ↑U
this : IsIntegral ↑U
⊢ nonZeroDivisors ↑Γ(X, U) = ⊥.asIdeal.primeCompl