no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_3
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)
x : M
y : { x // x ∈ S }
⊢ ↑(toMap f) ((sec f (mk' f x y)).fst * ↑y) = ↑(toMap f) (x * ↑(sec f (mk' f x y)).snd)
simp_rw [f.toMap.map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]