M : Type u_6
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_4
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_5
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_1
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_2
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
x : N
⊢ ↑(map k hl j) (↑(map f hy k) x) = ↑(MonoidHom.comp (map k hl j) (map f hy k)) x
M : Type u_6
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_4
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_5
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_1
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_2
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
x : N
⊢ ↑(map k hl j) (↑(map f hy k) x) = ↑(map f (_ : ∀ (x : { x // x ∈ S }), ↑(MonoidHom.comp l g) ↑x ∈ U) j) x
rw [← @map_comp_map M _ S N _ P _ f g T hy Q _ k A _ U R _ j l hl]
no goals
M : Type u_6
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_4
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : LocalizationMap S N
g : M →* P
hg : ∀ (y : { x // x ∈ S }), IsUnit (↑g ↑y)
T : Submonoid P
hy : ∀ (y : { x // x ∈ S }), ↑g ↑y ∈ T
Q : Type u_5
inst✝² : CommMonoid Q
k : LocalizationMap T Q
A : Type u_1
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_2
inst✝ : CommMonoid R
j : LocalizationMap U R
l : P →* A
hl : ∀ (w : { x // x ∈ T }), ↑l ↑w ∈ U
x : N
⊢ ↑(map k hl j) (↑(map f hy k) x) = ↑(MonoidHom.comp (map k hl j) (map f hy k)) x
simp only [MonoidHom.coe_comp, comp_apply]