no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.658823
inst✝ : CommMonoid P
f : LocalizationMap S N
x y : M
c : { x // x ∈ S }
h : ↑(toMap f) (x * ↑c) = ↑(toMap f) (y * ↑c)
⊢ ↑(toMap f) (↑(?m.689095 h) * x) = ↑(toMap f) (↑(?m.689095 h) * y)
rw [mul_comm _ x, mul_comm _ y, h]