no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.946305
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ mk' f (x * ↑y) y = ↑(toMap f) x
rw [← mul_mk'_one_eq_mk', f.toMap.map_mul, mul_assoc, mul_mk'_one_eq_mk', mk'_self', mul_one]