no goals
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
f : R
s : { x_1 // x_1 ∈ Ideal.primeCompl x.asIdeal }
⊢ ↑(toStalk R x) f =
    ↑(toStalk R x) ↑s *
      ↑(germ (Sheaf.presheaf (structureSheaf R)) { val := x, property := (_ : ↑s ∈ Ideal.primeCompl x.asIdeal) })
        (const R f (↑s) (PrimeSpectrum.basicOpen ↑s)
          (_ : ∀ (x_1 : ↑(PrimeSpectrum.Top R)), x_1 ∈ PrimeSpectrum.basicOpen ↑s → x_1 ∈ PrimeSpectrum.basicOpen ↑s))
erw [← germ_toOpen R (PrimeSpectrum.basicOpen s) ⟨x, s.2⟩,
  ← germ_toOpen R (PrimeSpectrum.basicOpen s) ⟨x, s.2⟩, ← RingHom.map_mul, toOpen_eq_const,
  toOpen_eq_const, const_mul_cancel']