no goals
M : Type u_2
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_1
inst✝ : CommMonoid Q
k : LocalizationMap T Q
z : N
⊢ ↑(toMap k) (↑g ↑(sec f z).snd) * ↑(map f hy k) z = ↑(toMap k) (↑g (sec f z).fst)
rw [mul_comm, f.map_mul_right]