no goals
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.700135
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
s : { x // x ∈ M }
⊢ mk' S x s = 0 ↔ ∃ m, ↑m * x = 0
rw [← (map_units S s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff M]