-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
⊢ 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))
have 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))
Tactic: erw [PresheafedSpace.stalkMap_germ (Spec.sheafedSpaceMap f).hom ⊤ p trivial]