no goals
R : Type u
inst✝ : CommRing R
f : R
⊢ ↑(toOpen R (PrimeSpectrum.basicOpen f)) f *
      const R 1 f (PrimeSpectrum.basicOpen f)
        (_ : ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ PrimeSpectrum.basicOpen f → x ∈ PrimeSpectrum.basicOpen f) =
    1
rw [toOpen_eq_const, const_mul_rev]