case intro
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
h : ↑(toMap f) x = ↑(toMap f) y
c : { x // x ∈ S }
hc : ↑c * x = ↑c * y
⊢ ↑g x = ↑g y
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
h : ↑(toMap f) x = ↑(toMap f) y
⊢ ↑g x = ↑g y
obtain ⟨c, hc⟩ := f.eq_iff_exists.1 h
case intro
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
h : ↑(toMap f) x = ↑(toMap f) y
c : { x // x ∈ S }
hc : ↑c * x = ↑c * y
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) c)⁻¹ * ↑(MonoidHom.restrict g S) c * ↑g x = ↑g y
case intro
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
h : ↑(toMap f) x = ↑(toMap f) y
c : { x // x ∈ S }
hc : ↑c * x = ↑c * y
⊢ ↑g x = ↑g y
rw [← one_mul (g x), ← IsUnit.liftRight_inv_mul (g.restrict S) hg c]
case intro
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
h : ↑(toMap f) x = ↑(toMap f) y
c : { x // x ∈ S }
hc : ↑c * x = ↑c * y
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) c)⁻¹ * ↑g ↑c * ↑g x = ↑g y
case intro
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
h : ↑(toMap f) x = ↑(toMap f) y
c : { x // x ∈ S }
hc : ↑c * x = ↑c * y
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) c)⁻¹ * ↑(MonoidHom.restrict g S) c * ↑g x = ↑g y
show _ * g c * _ = _
no goals
case intro
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
h : ↑(toMap f) x = ↑(toMap f) y
c : { x // x ∈ S }
hc : ↑c * x = ↑c * y
⊢ ↑(↑(IsUnit.liftRight (MonoidHom.restrict g S) hg) c)⁻¹ * ↑g ↑c * ↑g x = ↑g y
rw [mul_assoc, ← g.map_mul, hc, mul_comm, mul_inv_left hg, g.map_mul]