no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.800895
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
z : N
⊢ mk' f x y = z ↔ ↑(toMap f) x = z * ↑(toMap f) ↑y
rw [eq_comm, eq_mk'_iff_mul_eq, eq_comm]