-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem isLocalization_stalk (x : U) :
    IsLocalization.AtPrime (X.presheaf.stalk x) (hU.primeIdealOf x).asIdeal

Proof state:
case mk
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hx : (ConcreteCategory.hom hU.fromSpec.base) y ∈ U
hy : y = hU.primeIdealOf ⟨(ConcreteCategory.hom hU.fromSpec.base) y, hx⟩
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨(ConcreteCategory.hom hU.fromSpec.base) y, hx⟩)) y.asIdeal

Tactic:
exact hU.isLocalization_stalk' y hx

Result:
no goals

Proof state:
case mk
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hU.primeIdealOf ⟨x, hx⟩).asIdeal

Tactic:
set y := hU.primeIdealOf ⟨x, hx⟩ with hy

Result:
case mk
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : PrimeSpectrum ↑Γ(X, U) := hU.primeIdealOf ⟨x, hx⟩
hy : y = hU.primeIdealOf ⟨x, hx⟩
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal

Proof state:
case mk
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : PrimeSpectrum ↑Γ(X, U) := hU.primeIdealOf ⟨x, hx⟩
hy : y = hU.primeIdealOf ⟨x, hx⟩
this : (ConcreteCategory.hom hU.fromSpec.base) y = x
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal

Tactic:
clear_value y

Result:
case mk
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : PrimeSpectrum ↑Γ(X, U)
hy : y = hU.primeIdealOf ⟨x, hx⟩
this : (ConcreteCategory.hom hU.fromSpec.base) y = x
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑x)) (hU.primeIdealOf x).asIdeal

Tactic:
rcases x with ⟨x, hx⟩

Result:
case mk
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hU.primeIdealOf ⟨x, hx⟩).asIdeal

Proof state:
case mk
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : PrimeSpectrum ↑Γ(X, U) := hU.primeIdealOf ⟨x, hx⟩
hy : y = hU.primeIdealOf ⟨x, hx⟩
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal

Tactic:
have : hU.fromSpec.base y = x := hy ▸ hU.fromSpec_primeIdealOf ⟨x, hx⟩

Result:
case mk
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : PrimeSpectrum ↑Γ(X, U) := hU.primeIdealOf ⟨x, hx⟩
hy : y = hU.primeIdealOf ⟨x, hx⟩
this : (ConcreteCategory.hom hU.fromSpec.base) y = x
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal

Proof state:
case mk
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
y : PrimeSpectrum ↑Γ(X, U)
hy : y = hU.primeIdealOf ⟨x, hx⟩
this : (ConcreteCategory.hom hU.fromSpec.base) y = x
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal

Tactic:
subst this

Result:
case mk
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum ↑Γ(X, U)
hx : (ConcreteCategory.hom hU.fromSpec.base) y ∈ U
hy : y = hU.primeIdealOf ⟨(ConcreteCategory.hom hU.fromSpec.base) y, hx⟩
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨(ConcreteCategory.hom hU.fromSpec.base) y, hx⟩)) y.asIdeal