-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
erw :
  Eq (α := CommRingCat.of (↑R : Type u) ⟶ (Spec.sheafedSpaceObj S).presheaf.stalk p)
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheafInType (↑R : Type u) (↑R : Type u)))
          (op ⊤)))
      (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheafInType (↑R : Type u) (↑R : Type u)))
            (op ⊤))))
      ((Spec.sheafedSpaceMap f).hom.c.app (op ⊤) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).hom.base).obj ⊤) p
          trivial))
    (f ≫
      CategoryStruct.comp (Y :=
        CommRingCat.of
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheafInType (↑S : Type u) (↑S : Type u)))
            (op ⊤)))
        (CommRingCat.ofHom
          (algebraMap (↑S : Type u)
            (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheafInType (↑S : Type u) (↑S : Type u)))
              (op ⊤))))
        (TopCat.Presheaf.germ (structurePresheafInCommRingCat (↑S : Type u)) ⊤ p trivial))
⊢ Eq (α := CommRingCat.of (↑R : Type u) ⟶ (Spec.sheafedSpaceObj S).presheaf.stalk p)
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheafInType (↑R : Type u) (↑R : Type u)))
          (op ⊤)))
      (CommRingCat.ofHom
        (algebraMap (↑R : Type u)
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (structureSheafInType (↑R : Type u) (↑R : Type u)))
            (op ⊤))))
      (TopCat.Presheaf.germ (structurePresheafInCommRingCat (↑R : Type u)) ⊤
          (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) trivial ≫
        PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p))
    (f ≫
      CategoryStruct.comp (Y :=
        CommRingCat.of
          (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
              (structureSheafInType (↑S : Type u) (↑S : Type u)))
            (op ⊤)))
        (CommRingCat.ofHom
          (algebraMap (↑S : Type u)
            (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)))
                (structureSheafInType (↑S : Type u) (↑S : Type u)))
              (op ⊤))))
        (TopCat.Presheaf.germ (structurePresheafInCommRingCat (↑S : Type u)) ⊤ p trivial))

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

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap_germ, trivial, AlgebraicGeometry.Spec.sheafedSpaceMap, CategoryTheory.InducedCategory.Hom.hom, Top.top