no goals
R : Type u_1
inst✝⁷ : CommRing R
S : Submonoid R
M : Type u_2
M' : Type ?u.925325
M'' : Type ?u.925328
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
s : { x // x ∈ S }
m : M
⊢ LocalizedModule.mk m s = mk' (LocalizedModule.mkLinearMap S M) m s
rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
  LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_apply]