-- Mathlib/AlgebraicGeometry/Stalk.lean
lemma stalkClosedPointTo_fromSpecStalk (x : X) :
    stalkClosedPointTo (X.fromSpecStalk x) =
      (X.presheaf.stalkCongr (by rw [fromSpecStalk_closedPoint]; rfl)).hom

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
⊢ X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ stalkClosedPointTo (X.fromSpecStalk x) = (X.presheaf.stalkCongr ⋯).hom

Tactic:
refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_

Result:
X : Scheme
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
⊢ X.presheaf.germ U ((ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U ((ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      (X.presheaf.stalkCongr ⋯).hom

Proof state:
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
x : ↑↑X.toPresheafedSpace
⊢ Inseparable ((ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x))) x

Tactic:
rw [fromSpecStalk_closedPoint]

Result:
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
x : ↑↑X.toPresheafedSpace
⊢ Inseparable x x

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
⊢ X.presheaf.germ U ((ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U ((ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      (X.presheaf.stalkCongr ⋯).hom

Tactic:
simp only [TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes, id_eq]

Result:
X : Scheme
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
⊢ X.presheaf.germ U ((ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
this : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x
⊢ X.presheaf.germ U ((ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯

Tactic:
convert germ_stalkClosedPointTo_Spec_fromSpecStalk (𝟙 (X.presheaf.stalk x)) U hxU

Result:
no goals

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
⊢ X.presheaf.germ U ((ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯

Tactic:
have : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x := by simp

Result:
X : Scheme
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
this : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x
⊢ X.presheaf.germ U ((ConcreteCategory.hom (X.fromSpecStalk x).base) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯

Proof state:
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
x : ↑↑X.toPresheafedSpace
⊢ Inseparable x x

Tactic:
rfl

Result:
no goals