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 : M
v : P
y : { x // x ∈ S }
⊢ ↑g x * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) y)⁻¹ = v ↔ ↑g x = ↑g ↑y * v
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 : M
v : P
y : { x // x ∈ S }
⊢ ↑(lift f hg) (mk' f x y) = v ↔ ↑g x = ↑g ↑y * v
rw [f.lift_mk' hg]
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 : M
v : P
y : { x // x ∈ S }
⊢ ↑g x * ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) y)⁻¹ = v ↔ ↑g x = ↑g ↑y * v
exact mul_inv_left hg _ _ _