-- Mathlib/AlgebraicGeometry/Stalk.lean
@[stacks 01J7]
lemma range_fromSpecStalk {x : X} :
    Set.range (X.fromSpecStalk x).base = { y | y ⤳ x }

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base) = {y | y ⤳ x}

Tactic:
ext y

Result:
case h
X : Scheme
x y : ↑↑X.toPresheafedSpace
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base) ↔ y ∈ {y | y ⤳ x}

Proof state:
case h.mpr
X : Scheme
x y : ↑↑X.toPresheafedSpace
hy : y ⤳ x
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base)

Tactic:
have := fromSpecStalk_closedPoint (x := y)

Result:
case h.mpr
X : Scheme
x y : ↑↑X.toPresheafedSpace
hy : y ⤳ x
this : (ConcreteCategory.hom (X.fromSpecStalk y).base) (closedPoint ↑(X.presheaf.stalk y)) = y
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base)

Proof state:
case h
X : Scheme
x y : ↑↑X.toPresheafedSpace
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base) ↔ y ∈ {y | y ⤳ x}

Tactic:
constructor

Result:
case h.mp
X : Scheme
x y : ↑↑X.toPresheafedSpace
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base) → y ∈ {y | y ⤳ x}

case h.mpr
X : Scheme
x y : ↑↑X.toPresheafedSpace
⊢ y ∈ {y | y ⤳ x} → y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base)

Proof state:
case h.mpr
X : Scheme
x y : ↑↑X.toPresheafedSpace
hy : y ⤳ x
this :
  (ConcreteCategory.hom (Spec.map (X.presheaf.stalkSpecializes hy) ≫ X.fromSpecStalk x).base)
      (closedPoint ↑(X.presheaf.stalk y)) =
    y
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base)

Tactic:
exact ⟨_, this⟩

Result:
no goals

Proof state:
case h.mp.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
y : ↑↑(Spec (X.presheaf.stalk x)).toPresheafedSpace
⊢ (ConcreteCategory.hom (X.fromSpecStalk x).base) y ∈ {y | y ⤳ x}

Tactic:
exact ((IsLocalRing.specializes_closedPoint y).map (X.fromSpecStalk x).base.hom.2).trans
  (specializes_of_eq fromSpecStalk_closedPoint)

Result:
no goals

Proof state:
case h.mpr
X : Scheme
x y : ↑↑X.toPresheafedSpace
hy : y ⤳ x
this : (ConcreteCategory.hom (X.fromSpecStalk y).base) (closedPoint ↑(X.presheaf.stalk y)) = y
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base)

Tactic:
rw [← Spec_map_stalkSpecializes_fromSpecStalk hy] at this

Result:
case h.mpr
X : Scheme
x y : ↑↑X.toPresheafedSpace
hy : y ⤳ x
this :
  (ConcreteCategory.hom (Spec.map (X.presheaf.stalkSpecializes hy) ≫ X.fromSpecStalk x).base)
      (closedPoint ↑(X.presheaf.stalk y)) =
    y
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base)

Proof state:
case h.mpr
X : Scheme
x y : ↑↑X.toPresheafedSpace
⊢ y ∈ {y | y ⤳ x} → y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base)

Tactic:
rintro (hy : y ⤳ x)

Result:
case h.mpr
X : Scheme
x y : ↑↑X.toPresheafedSpace
hy : y ⤳ x
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base)

Proof state:
case h.mp
X : Scheme
x y : ↑↑X.toPresheafedSpace
⊢ y ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecStalk x).base) → y ∈ {y | y ⤳ x}

Tactic:
rintro ⟨y, rfl⟩

Result:
case h.mp.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
y : ↑↑(Spec (X.presheaf.stalk x)).toPresheafedSpace
⊢ (ConcreteCategory.hom (X.fromSpecStalk x).base) y ∈ {y | y ⤳ x}