Lean/Mathlib: R_p regular for regular local R via pd and IsLocalizedModule (no Tor)

Once you have 'R regular local ⇒ every f.g. module has finite pd' and 'pd k < ∞ ⇒ regular', localization is short: ModuleCat.projectiveDimension_le_projectiveDimension_of_isLocalizedModule P.primeCompl (ModuleCat.of R (R ⧸ P)) bounds pd of the localized module, and you identify (R/P)_P with R_P ⧸ 𝔪 as follows: Submodule.toLocalizedQuotient' Rp P.primeCompl (Algebra.linearMap R Rp) P is an instance of IsLocalizedModule, so IsLocalizedModule.iso gives an R-linear equiv LocalizedModule P.primeCompl (R ⧸ P) ≃ Rp ⧸ P.localized' ...; make it Rp-linear with LinearEquiv.extendScalarsOfIsLocalization, then use Submodule.localized'_eq_span + IsLocalization.AtPrime.map_eq_maximalIdeal and Submodule.quotEquivOfEq. Wrap with Shrink.linearEquiv on both ends to get an iso in ModuleCat and finish with projectiveDimension_eq_of_iso. The change-of-rings step pd_{R/x}(N/xN) ≤ pd_R N (x regular on R and N) can be done by hand: induct with a syzygy, use QuotSMulTop.map_exact/map_surjective for right exactness, and prove injectivity of K/xK → F/xF from x-regularity of N via Submodule.mem_smul_pointwise_iff_exists; build R/x-linear maps with LinearMap.extendScalarsOfSurjective.