case h
M : Type u_4
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)
T : Submonoid P
Q : Type u_3
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
x✝ : M
⊢ ↑(toMap (ofMulEquivOfLocalizations f (MulEquiv.trans k j))) x✝ =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom j) (toMap (ofMulEquivOfLocalizations f k))) x✝
M : Type u_4
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)
T : Submonoid P
Q : Type u_3
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
⊢ toMap (ofMulEquivOfLocalizations f (MulEquiv.trans k j)) =
    MonoidHom.comp (MulEquiv.toMonoidHom j) (toMap (ofMulEquivOfLocalizations f k))
ext
no goals
case h
M : Type u_4
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)
T : Submonoid P
Q : Type u_3
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
x✝ : M
⊢ ↑(toMap (ofMulEquivOfLocalizations f (MulEquiv.trans k j))) x✝ =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom j) (toMap (ofMulEquivOfLocalizations f k))) x✝
rfl