-- Mathlib/AlgebraicGeometry/Stalk.lean
@[reassoc]
lemma germ_stalkClosedPointTo_Spec_fromSpecStalk
    {x : X} (f : X.presheaf.stalk x ⟶ R) [IsLocalHom f.hom] (U : Opens X) (hU) :
    X.presheaf.germ U _ hU ≫ stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
      X.presheaf.germ U x (by simpa using hU) ≫ f

Proof state:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
this✝ : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U ((ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R)) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
simp only [TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes_assoc,
  germ_stalkClosedPointTo, comp_app,
  fromSpecStalk_app (X := X) (x := x) this, Category.assoc, Iso.trans_hom,
  Functor.mapIso_hom, Hom.naturality_assoc, ← Functor.map_comp_assoc,
  (Spec.map f).app_eq_appLE, Hom.appLE_map_assoc, Hom.map_appLE_assoc]

Result:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
this✝ : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫ (ΓSpecIso (X.presheaf.stalk x)).inv ≫ Hom.appLE (Spec.map f) ⊤ ⊤ ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f

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
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
⊢ x ∈ U

Tactic:
simpa using hU

Result:
no goals

Proof state:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
this✝ : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫
      (ΓSpecIso (X.presheaf.stalk x)).inv ≫
        Hom.appLE (Spec.map f) ⊤ ((Opens.map (Spec.map f).base).obj ⊤) ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
rw [← (Spec.map f).app_eq_appLE, ΓSpecIso_naturality, Iso.inv_hom_id_assoc]

Result:
no goals

Proof state:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
⊢ (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) = x

Tactic:
rw [comp_base_apply, Spec_closedPoint, fromSpecStalk_closedPoint]

Result:
no goals

Proof state:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
⊢ X.presheaf.germ U ((ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R)) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
have : (Spec.map f ≫ X.fromSpecStalk x).base (closedPoint R) = x := by
  rw [comp_base_apply, Spec_closedPoint, fromSpecStalk_closedPoint]

Result:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
this : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) = x
⊢ X.presheaf.germ U ((ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R)) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f

Proof state:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
this : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) = x
⊢ X.presheaf.germ U ((ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R)) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
have : x ∈ U := this ▸ hU

Result:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
this✝ : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U ((ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R)) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f

Proof state:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
this✝ : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫ (ΓSpecIso (X.presheaf.stalk x)).inv ≫ Hom.appLE (Spec.map f) ⊤ ⊤ ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
simp_rw [← Opens.map_top (Spec.map f).base]

Result:
X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↑↑X.toPresheafedSpace
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) ∈ U
this✝ : (ConcreteCategory.hom (Spec.map f ≫ X.fromSpecStalk x).base) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫
      (ΓSpecIso (X.presheaf.stalk x)).inv ≫
        Hom.appLE (Spec.map f) ⊤ ((Opens.map (Spec.map f).base).obj ⊤) ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f