case mk
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
val✝ : ↑(PrimeSpectrum.Top R)
property✝ : val✝ ∈ U
⊢ ↑(stalkToFiberRingHom R ↑{ val := val✝, property := property✝ })
      (↑(germ (Sheaf.presheaf (structureSheaf R)) { val := val✝, property := property✝ }) s) =
    ↑s { val := val✝, property := property✝ }
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
x : { x // x ∈ U }
s : ↑((structureSheaf R).val.obj U.op)
⊢ ↑(stalkToFiberRingHom R ↑x) (↑(germ (Sheaf.presheaf (structureSheaf R)) x) s) = ↑s x
cases x
no goals
case mk
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj U.op)
val✝ : ↑(PrimeSpectrum.Top R)
property✝ : val✝ ∈ U
⊢ ↑(stalkToFiberRingHom R ↑{ val := val✝, property := property✝ })
      (↑(germ (Sheaf.presheaf (structureSheaf R)) { val := val✝, property := property✝ }) s) =
    ↑s { val := val✝, property := property✝ }
exact stalkToFiberRingHom_germ' R U _ _ _