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