R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h ≫ (stalkIso R x).hom =
    (stalkIso R y).hom ≫
      let_fun this := PrimeSpectrum.localizationMapOfSpecializes h;
      this
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h ≫ stalkToFiberRingHom R x =
    stalkToFiberRingHom R y ≫
      let_fun this := PrimeSpectrum.localizationMapOfSpecializes h;
      this
change _ ≫ (StructureSheaf.stalkIso R x).hom = (StructureSheaf.stalkIso R y).hom ≫ _
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (stalkIso R y).inv ≫ stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h =
    (let_fun this := PrimeSpectrum.localizationMapOfSpecializes h;
      this) ≫
      (stalkIso R x).inv
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h ≫ (stalkIso R x).hom =
    (stalkIso R y).hom ≫
      let_fun this := PrimeSpectrum.localizationMapOfSpecializes h;
      this
rw [← Iso.eq_comp_inv, Category.assoc, ← Iso.inv_comp_eq]
no goals
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (stalkIso R y).inv ≫ stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h =
    (let_fun this := PrimeSpectrum.localizationMapOfSpecializes h;
      this) ≫
      (stalkIso R x).inv
exact localizationToStalk_stalkSpecializes h