-- Mathlib/AlgebraicGeometry/Spec.lean
theorem stalkMap_toStalk {R S : CommRingCat.{u}} (f : R ⟶ S) (p : PrimeSpectrum S) :
    toStalk R (PrimeSpectrum.comap f.hom p) ≫ (Spec.sheafedSpaceMap f).stalkMap p =
      f ≫ toStalk S p

Proof state:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toOpen ↑R ⊤ ≫
      (structureSheaf ↑R).presheaf.germ ⊤ ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p) trivial ≫
        PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p =
    f ≫ toOpen ↑S ⊤ ≫ (structureSheaf ↑S).presheaf.germ ⊤ p trivial

Tactic:
erw [PresheafedSpace.stalkMap_germ (Spec.sheafedSpaceMap f) ⊤ p trivial]

Result:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toOpen ↑R ⊤ ≫
      (Spec.sheafedSpaceMap f).c.app (op ⊤) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).base).obj ⊤) p
          trivial =
    f ≫ toOpen ↑S ⊤ ≫ (structureSheaf ↑S).presheaf.germ ⊤ p trivial

Proof state:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toOpen ↑R ⊤ ≫
      (Spec.sheafedSpaceMap f).c.app (op ⊤) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).base).obj ⊤) p
          trivial =
    f ≫ toOpen ↑S ⊤ ≫ (structureSheaf ↑S).presheaf.germ ⊤ p trivial

Tactic:
rw [Spec.sheafedSpaceMap_c_app]

Result:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toOpen ↑R ⊤ ≫
      CommRingCat.ofHom
          (comap (CommRingCat.Hom.hom f) (unop (op ⊤)) ((TopologicalSpace.Opens.map (Spec.topMap f)).obj (unop (op ⊤)))
            ⋯) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).base).obj ⊤) p
          trivial =
    f ≫ toOpen ↑S ⊤ ≫ (structureSheaf ↑S).presheaf.germ ⊤ p trivial

Proof state:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toStalk (↑R) ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p) ≫
      PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p =
    f ≫ toStalk (↑S) p

Tactic:
rw [← toOpen_germ S ⊤ p trivial, ← toOpen_germ R ⊤ (PrimeSpectrum.comap f.hom p) trivial,
  Category.assoc]

Result:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toOpen ↑R ⊤ ≫
      (structureSheaf ↑R).presheaf.germ ⊤ ((PrimeSpectrum.comap (CommRingCat.Hom.hom f)) p) trivial ≫
        PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f) p =
    f ≫ toOpen ↑S ⊤ ≫ (structureSheaf ↑S).presheaf.germ ⊤ p trivial

Proof state:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      toOpen (↑S) ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap (CommRingCat.Hom.hom f))) ⊤) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).base).obj ⊤) p
          trivial =
    f ≫ toOpen ↑S ⊤ ≫ (structureSheaf ↑S).presheaf.germ ⊤ p trivial

Tactic:
rfl

Result:
no goals

Proof state:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toOpen ↑R ⊤ ≫
      CommRingCat.ofHom
          (comap (CommRingCat.Hom.hom f) (unop (op ⊤)) ((TopologicalSpace.Opens.map (Spec.topMap f)).obj (unop (op ⊤)))
            ⋯) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).base).obj ⊤) p
          trivial =
    f ≫ toOpen ↑S ⊤ ≫ (structureSheaf ↑S).presheaf.germ ⊤ p trivial

Tactic:
erw [toOpen_comp_comap_assoc]

Result:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      toOpen (↑S) ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap (CommRingCat.Hom.hom f))) ⊤) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).base).obj ⊤) p
          trivial =
    f ≫ toOpen ↑S ⊤ ≫ (structureSheaf ↑S).presheaf.germ ⊤ p trivial