no goals
R : Type u_2
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_1
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.248906
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
z : S
⊢ ↑(algebraMap R S) (sec M z).fst = ↑(algebraMap R S) ↑(sec M z).snd * z
rw [mul_comm, sec_spec]