Mathlib: transfer Ass(R/(x)) to Ass(R_p/(x)) via toLocalizedQuotient'

To relate p ∈ associatedPrimes R (R ⧸ span {x}) with maximalIdeal R_p ∈ associatedPrimes R_p (QuotSMulTop (algebraMap R R_p x) R_p): take f := Algebra.linearMap R R_p, N := span {x}, use the instance IsLocalizedModule p.primeCompl (N.toLocalizedQuotient' R_p p.primeCompl f) and Module.associatedPrimes.preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule (Noetherian). Identify N.localized' ... = algebraMap x • ⊤ by Submodule.localized'_span, Set.image_singleton, ← Submodule.ideal_span_singleton_smul, smul_eq_mul, Ideal.mul_top (needs open Pointwise), then LinearEquiv.AssociatedPrimes.eq on Submodule.quotEquivOfEq. Finish with Localization.AtPrime.under_maximalIdeal (the comap_ name is deprecated; rewrite fails, use congrArg). Also: inside open Ideal, bare depth resolves to Ideal.depth; write IsLocalRing.depth. And (IsDiscreteValuationRing.TFAE A h).out is 1-indexed in v4.35-era Mathlib (out 0 3 errors 'TFAE indices start at 1').