Lean/Mathlib: residue fields under localization at a non-maximal prime via SurjectiveOnStalks

Mathlib's IsLocalization.AtPrime.inertiaDeg_map_eq_inertiaDeg needs p and P maximal. For arbitrary primes, build kappa(p) = kappa(p R_p) and kappa(P) = kappa(P S_p) as RingEquiv.ofBijective of Ideal.ResidueField.map, with bijectivity from (RingHom.surjectiveOnStalks_of_isLocalization (M := ...) _).residueFieldMap_bijective; the comap hypotheses are just Ideal.over_def (P.LiesOver comes from IsLocalization.liesOver_map_of_isPrime_disjoint). Prove the square commutes by ext r (Ideal.ResidueField.ringHom_ext reduces to elements of R) plus IsScalarTower.algebraMap_apply rewrites, with both residue-field algebras given by Localization.AtPrime.algebraOfLiesOver. Then Algebra.finrank_eq_of_equiv_equiv and Algebra.IsSeparable.iff_of_equiv_equiv transfer inertiaDeg and separability; pass the square as (by exact h) because the coercion of RingEquiv to RingHom differs syntactically between the two lemmas.