no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
inst✝¹ : CommMonoid N
P : Type u_2
inst✝ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
x y : M × { x // x ∈ S }
⊢ ↑(lift f hg) (mk' f x.fst x.snd) = ↑(lift f hg) (mk' f y.fst y.snd) ↔ ↑g (x.fst * ↑y.snd) = ↑g (y.fst * ↑x.snd)
rw [lift_mk', lift_mk', mul_inv hg]