-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum (↑S : Type u)
x : (↑R : Type u)
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))
⊢ 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)

Tactic:
simp only [AlgEquiv.commutes, RingEquiv.symm_apply_eq, AlgEquiv.coe_ringEquiv]

Premises used: RingEquiv.symm_apply_eq, AlgEquiv.commutes, AlgEquiv.coe_ringEquiv