no goals
R : Type u
inst✝ : CommRing R
s f : R
g : { x // x ∈ Submonoid.powers s }
⊢ ↑(toOpen R (PrimeSpectrum.basicOpen s)) f =
    ↑(toOpen R (PrimeSpectrum.basicOpen s)) ↑g *
      const R f (↑g) (PrimeSpectrum.basicOpen s)
        (_ : ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen s → ↑g ∈ Ideal.primeCompl x.asIdeal)
rw [toOpen_eq_const, toOpen_eq_const, const_mul_cancel']