R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (toOpen R ⊤ ≫ germ (Sheaf.presheaf (structureSheaf R)) { val := y, property := True.intro }) ≫
      stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h =
    toOpen R ⊤ ≫ germ (Sheaf.presheaf (structureSheaf R)) { val := x, property := True.intro }
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ toStalk R y ≫ stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h = toStalk R x
dsimp [toStalk]
no goals
R✝ : Type u
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
x y : PrimeSpectrum R
h : x ⤳ y
⊢ (toOpen R ⊤ ≫ germ (Sheaf.presheaf (structureSheaf R)) { val := y, property := True.intro }) ≫
      stalkSpecializes (Sheaf.presheaf (structureSheaf R)) h =
    toOpen R ⊤ ≫ germ (Sheaf.presheaf (structureSheaf R)) { val := x, property := True.intro }
simp [-toOpen_germ]