M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
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)
j k : N →* P
h : ∀ (a : M), ↑(MonoidHom.comp j (toMap f)) a = ↑(MonoidHom.comp k (toMap f)) a
⊢ lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp j (toMap f)) ↑y)) =
    lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp k (toMap f)) ↑y))
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
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)
j k : N →* P
h : ∀ (a : M), ↑(MonoidHom.comp j (toMap f)) a = ↑(MonoidHom.comp k (toMap f)) a
⊢ j = k
rw [← f.lift_of_comp j, ← f.lift_of_comp k]
case e_g.h
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
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)
j k : N →* P
h : ∀ (a : M), ↑(MonoidHom.comp j (toMap f)) a = ↑(MonoidHom.comp k (toMap f)) a
x : M
⊢ ↑(MonoidHom.comp j (toMap f)) x = ↑(MonoidHom.comp k (toMap f)) x
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
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)
j k : N →* P
h : ∀ (a : M), ↑(MonoidHom.comp j (toMap f)) a = ↑(MonoidHom.comp k (toMap f)) a
⊢ lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp j (toMap f)) ↑y)) =
    lift f (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(MonoidHom.comp k (toMap f)) ↑y))
congr 1 with x
no goals
case e_g.h
M : Type u_3
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
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)
j k : N →* P
h : ∀ (a : M), ↑(MonoidHom.comp j (toMap f)) a = ↑(MonoidHom.comp k (toMap f)) a
x : M
⊢ ↑(MonoidHom.comp j (toMap f)) x = ↑(MonoidHom.comp k (toMap f)) x
exact h x