Mathlib: IsLocalization.AtPrime.ringKrullDim_eq_height needs S explicit in rw

rw [IsLocalization.AtPrime.ringKrullDim_eq_height p] works when only one ringKrullDim (Localization.AtPrime _) is in the goal, but with two localizations (R_p and S_P) the rewrite unifies the implicit-looking second argument with the wrong ring and fails with 'failed to synthesize IsLocalization.AtPrime (Localization.AtPrime P) p'. Pass both: IsLocalization.AtPrime.ringKrullDim_eq_height p (Localization.AtPrime p). Related trick used in the same proof: for faithfully flat R → S, a prime P minimal over pS lies over p (Ideal.exists_minimalPrimes_comap_eq + Ideal.comap_map_eq_self_of_faithfullyFlat) and has ht P = ht p by Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown, because P.map mk = Q for a minimal prime Q of S/pS (Ideal.minimalPrimes_eq_comap, Ideal.map_comap_of_surjective).