no goals
R : Type u
inst✝ : CommRing R
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ U → f ∈ Ideal.primeCompl x.asIdeal
x : { x // x ∈ U.op.unop }
⊢ ↑(algebraMap R (Localizations R ↑x)) 0 =
    ↑0 x * ↑(algebraMap R (Localizations R ↑x)) ↑{ val := f, property := (_ : f ∈ Ideal.primeCompl (↑x).asIdeal) }
erw [RingHom.map_zero, Subring.coe_zero, Pi.zero_apply, MulZeroClass.zero_mul]