case h
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type ?u.3102959
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type ?u.3111444
inst✝ : CommMonoid Q
x✝ : M
⊢ ↑(toMap (ofMulEquivOfDom f (_ : Submonoid.map (MulEquiv.toMonoidHom (MulEquiv.refl M)) S = S))) x✝ = ↑(toMap f) x✝
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type ?u.3102959
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type ?u.3111444
inst✝ : CommMonoid Q
⊢ ofMulEquivOfDom f (_ : Submonoid.map (MulEquiv.toMonoidHom (MulEquiv.refl M)) S = S) = f
ext
no goals
case h
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type ?u.3102959
inst✝¹ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type ?u.3111444
inst✝ : CommMonoid Q
x✝ : M
⊢ ↑(toMap (ofMulEquivOfDom f (_ : Submonoid.map (MulEquiv.toMonoidHom (MulEquiv.refl M)) S = S))) x✝ = ↑(toMap f) x✝
rfl