-- Mathlib/AlgebraicGeometry/Stalk.lean
@[reassoc]
lemma Spec_stalkClosedPointTo_fromSpecStalk :
    Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk _ = f

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ ↑U
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk ((ConcreteCategory.hom f.base) (closedPoint ↑R)) = f

Tactic:
have := IsAffineOpen.Spec_map_appLE_fromSpec f hU (isAffineOpen_top _)
  (preimage_eq_top_of_closedPoint_mem f hxU).ge

Result:
case intro.intro.intro.intro.intro
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ ↑U
this : Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = ⋯.fromSpec ≫ f
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk ((ConcreteCategory.hom f.base) (closedPoint ↑R)) = f

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ ↑U
this : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk ((ConcreteCategory.hom f.base) (closedPoint ↑R)) = f

Tactic:
rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc,
  germ_stalkClosedPointTo]

Result:
case intro.intro.intro.intro.intro
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ ↑U
this : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op ≪≫ ΓSpecIso R).hom) ≫
      IsAffineOpen.fromSpec hU =
    f

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ ↑U
this : Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = ⋯.fromSpec ≫ f
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk ((ConcreteCategory.hom f.base) (closedPoint ↑R)) = f

Tactic:
rw [IsAffineOpen.fromSpec_top, Iso.eq_inv_comp, isoSpec_Spec_hom] at this

Result:
case intro.intro.intro.intro.intro
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ ↑U
this : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk ((ConcreteCategory.hom f.base) (closedPoint ↑R)) = f

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ ↑U
this : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op ≪≫ ΓSpecIso R).hom) ≫
      IsAffineOpen.fromSpec hU =
    f

Tactic:
simpa only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Category.assoc,
  Hom.app_eq_appLE, Hom.appLE_map_assoc, Spec.map_comp_assoc]

Result:
no goals

Proof state:
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk ((ConcreteCategory.hom f.base) (closedPoint ↑R)) = f

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (isBasis_affine_open X).exists_subset_of_mem_open
  (Set.mem_univ (f.base (closedPoint R))) isOpen_univ

Result:
case intro.intro.intro.intro.intro
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : (ConcreteCategory.hom f.base) (closedPoint ↑R) ∈ ↑U
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk ((ConcreteCategory.hom f.base) (closedPoint ↑R)) = f