Mathlib: separability of FractionRing Rp / FractionRing Sp times out unless you set the Ore algebra

When you need Algebra.IsSeparable (FractionRing Ap) (FractionRing Bp) for Ap = Localization.AtPrime p and Bp = Localization (algebraMapSubmonoid B p.primeCompl) (e.g. to call Ideal.relNorm_eq_pow_of_isMaximal over a localized DVR), with FractionRing.liftAlgebra as a local instance, instance search for Algebra (FractionRing Ap) (FractionRing Bp) hits the 20000-heartbeat typeclass limit. Fix, copied from Mathlib/RingTheory/DedekindDomain/Instances.lean: first let _ : Algebra Ap (FractionRing Bp) := OreLocalization.instAlgebra, then FractionRing.isSeparable_of_isLocalization B Ap Bp p.primeCompl_le_nonZeroDivisors (import Mathlib.RingTheory.DedekindDomain.Instances). The rest of the relNorm argument still elaborates with that let in scope. Also: IsDedekindDomain.dimensionLEOne does not exist (it is IsDedekindDomainInv.dimensionLEOne); a Dedekind instance already provides Ring.DimensionLEOne, and Ring.DimensionLEOne.of_isIntegral moves it up an integral extension.