-- 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 ⊤))))
      (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).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))
have erw : Eq (α := CommRingCat.of (↑R : Type u) ⟶ (Spec.sheafedSpaceObj S).presheaf.stalk p)
  (CommRingCat.ofHom (CommRingCat.Hom.hom 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)))
                (structureSheaf (↑S : Type u)))
              (op
                ((TopologicalSpace.Opens.comap
                      { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := sorry :
                        C(PrimeSpectrum (↑S : Type u), PrimeSpectrum (↑R : Type u)) } :
                    (a : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u))) →
                      TopologicalSpace.Opens (PrimeSpectrum (↑S : Type u)))
                  ⊤))) :
          Type u))
      (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)))
                  (structureSheaf (↑S : Type u)))
                (op
                  ((TopologicalSpace.Opens.comap
                        { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := sorry :
                          C(PrimeSpectrum (↑S : Type u), PrimeSpectrum (↑R : Type u)) } :
                      (a : TopologicalSpace.Opens (PrimeSpectrum (↑R : Type u))) →
                        TopologicalSpace.Opens (PrimeSpectrum (↑S : Type u)))
                    ⊤))) :
            Type u)))
      ((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 [toOpen_comp_comap_assoc]