no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.309265
inst✝ : CommMonoid P
f : LocalizationMap S N
z : N
⊢ ↑(toMap f) (sec f z).fst = ↑(toMap f) ↑(sec f z).snd * z
rw [mul_comm, sec_spec]