-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
x : (↑R : Type u)
⊢ Eq (α := Localization.AtPrime p.asIdeal)
    (((stalkIso (↑S : Type u) p).toRingEquiv.symm :
          (a : (↑((structurePresheafInCommRingCat (↑S : Type u)).stalk p) : Type u)) → Localization.AtPrime p.asIdeal)
        ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p) :
            (a :
                (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk
                      (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
                  Type u)) →
              (↑((structurePresheafInCommRingCat (↑S : Type u)).stalk p) : Type u))
          ((stalkIso (↑R : Type u) (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) :
                (a : Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal)) →
                  (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk
                        (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
                    Type u))
              ((algebraMap (↑R : Type u) (Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal)) :
                    (a : (↑R : Type u)) → Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal))
                  x :
                Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom f) p.asIdeal)) :
            (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u))
                  (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
              Type u))) :
      Localization.AtPrime p.asIdeal)
    ((algebraMap (↑S : Type u) (Localization.AtPrime p.asIdeal) : (a : (↑S : Type u)) → Localization.AtPrime p.asIdeal)
        ((CommRingCat.Hom.hom f : (a : (↑R : Type u)) → (↑S : Type u)) x) :
      Localization.AtPrime p.asIdeal)
have simp : Eq (α := (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u))
  ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p) :
        (a :
            (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
              Type u)) →
          (↑((structurePresheafInCommRingCat (↑S : Type u)).stalk p) : Type u))
      ((algebraMap (↑R : Type u)
              (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u))
                    (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
                Type u) :
            (a : (↑R : Type u)) →
              (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
                Type u))
          x :
        (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u))
              (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)) :
          Type u)) :
    (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u))
  ((algebraMap (↑S : Type u) (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u) :
        (a : (↑S : Type u)) → (↑((structurePresheafInCommRingCat (↑S : Type u)).stalk p) : Type u))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u)) → (↑S : Type u)) x : (↑S : Type u)) :
    (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑S : Type u)) p) : Type u))
Tactic: simp only [AlgEquiv.commutes, RingEquiv.symm_apply_eq, AlgEquiv.coe_ringEquiv]