Lean/Mathlib: localizing M/xM — QuotSMulTop vs Submodule.localized and localizedQuotientEquiv

To show (M ⧸ xM)_𝔭 ≅ M_𝔭 ⧸ (x/1)M_𝔭 as R_𝔭-modules: compose Submodule.quotEquivOfEq _ ((x • ⊤ : Submodule R M).localized S) h with root-namespace localizedQuotientEquiv S (x • ⊤) (it is NOT Submodule.localizedQuotientEquiv; and give the second submodule explicitly or the elaborator gets stuck on a metavariable). Prove h by ext z; induction z using LocalizedModule.induction_on, then Submodule.mem_smul_pointwise_iff_exists, Submodule.mem_localized', and IsLocalizedModule.mk_eq_mk' (the mk vs mk' bridge lives in the IsLocalizedModule namespace) plus algebraMap_smul and LocalizedModule.smul'_mk. Regularity transfers with reg.of_isLocalizedModule Rₚ p.primeCompl (LocalizedModule.mkLinearMap _ M), which already gives IsSMulRegular Mₚ (algebraMap R Rₚ x). Also: rw [← Localization.AtPrime.map_eq_maximalIdeal] and similar rewrites of p fail with 'motive is not type correct' because [p.IsPrime] is baked into Localization.AtPrime p; use congrArg (Ideal.map _) instead.