no goals
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_1
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
z : N
w v : (fun x => P) z
⊢ ↑(lift f hg) z * w = v ↔ ↑g (sec f z).fst * w = ↑g ↑(sec f z).snd * v
erw [mul_comm, ← mul_assoc, mul_inv_left hg, mul_comm]