R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : { x // x ∈ U }
f : R
⊢ ↑(germ (Sheaf.presheaf (structureSheaf R)) x) (↑(toOpen R U) f) =
    ↑(toOpen R U ≫ germ (Sheaf.presheaf (structureSheaf R)) x) f
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : { x // x ∈ U }
f : R
⊢ ↑(germ (Sheaf.presheaf (structureSheaf R)) x) (↑(toOpen R U) f) = ↑(toStalk R ↑x) f
rw [← toOpen_germ]
no goals
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : { x // x ∈ U }
f : R
⊢ ↑(germ (Sheaf.presheaf (structureSheaf R)) x) (↑(toOpen R U) f) =
    ↑(toOpen R U ≫ germ (Sheaf.presheaf (structureSheaf R)) x) f
rfl