no goals
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : LocalizedModule S M
m m' : M
s s' : { x // x ∈ S }
⊢ mk m s + mk m' s' = mk m' s' + mk m s
rw [mk_add_mk, mk_add_mk, add_comm, mul_comm]