-- Mathlib/AlgebraicGeometry/Spec.lean
theorem Spec_map_localization_isIso (R : CommRingCat.{u}) (M : Submonoid R)
    (x : PrimeSpectrum (Localization M)) :
    IsIso
      ((Spec.toPresheafedSpace.map
        (CommRingCat.ofHom (algebraMap R (Localization M))).op).stalkMap x)

Proof state:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom

Tactic:
infer_instance

Result:
no goals

Proof state:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) x)

Tactic:
rw [← localRingHom_comp_stalkIso]

Result:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    ((stalkIso (↑(CommRingCat.of ↑R))
          ((PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))) x)).hom ≫
      CommRingCat.ofHom
          (Localization.localRingHom
            ((PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))))
                x).asIdeal
            x.asIdeal (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) ⋯) ≫
        (stalkIso (↑(CommRingCat.of (Localization M))) x).inv)

Proof state:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (CommRingCat.ofHom
      (Localization.localRingHom
        ((PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))) x).asIdeal
        x.asIdeal (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) ⋯))

Tactic:
show
  IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M
    x.asIdeal).toRingEquiv.toCommRingCatIso.hom

Result:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom

Proof state:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (PresheafedSpace.Hom.stalkMap (Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op)
      x)

Tactic:
dsimp only [Spec.toPresheafedSpace_map, Quiver.Hom.unop_op]

Result:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) x)

Proof state:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    ((stalkIso (↑(CommRingCat.of ↑R))
          ((PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))) x)).hom ≫
      CommRingCat.ofHom
          (Localization.localRingHom
            ((PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))))
                x).asIdeal
            x.asIdeal (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) ⋯) ≫
        (stalkIso (↑(CommRingCat.of (Localization M))) x).inv)

Tactic:
refine IsIso.comp_isIso' inferInstance (IsIso.comp_isIso' ?_ inferInstance)

Result:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (CommRingCat.ofHom
      (Localization.localRingHom
        ((PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))) x).asIdeal
        x.asIdeal (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) ⋯))