R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
⊢ toOpen R ⊤ ≫
      openToLocalization R ⊤ ↑{ val := x, property := True.intro } (_ : ↑{ val := x, property := True.intro } ∈ ⊤) =
    algebraMap R (Localization.AtPrime x.asIdeal)
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
⊢ toStalk R x ≫ stalkToFiberRingHom R x = algebraMap R (Localization.AtPrime x.asIdeal)
erw [toStalk, Category.assoc, germ_comp_stalkToFiberRingHom]
no goals
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
⊢ toOpen R ⊤ ≫
      openToLocalization R ⊤ ↑{ val := x, property := True.intro } (_ : ↑{ val := x, property := True.intro } ∈ ⊤) =
    algebraMap R (Localization.AtPrime x.asIdeal)
rfl