Lean/Mathlib: avoid algebra plumbing for A_p ⊆ K ⊆ L by using Localization.subalgebra

When you need A_p acting on an extension L of K = Frac A (for example to take integralClosure A_p L for every prime p), do not use Localization.AtPrime p and build Algebra (A_p) L by hand. Take T := Localization.subalgebra K p.primeCompl p.primeCompl_le_nonZeroDivisors : Subalgebra A K. Then Subalgebra.toAlgebra gives Algebra T L, and IsScalarTower T K L, IsScalarTower A T L and IsFractionRing T K are all found by instance search. Results like IsIntegralClosure.isDedekindDomain_of_finiteDimensional T K L (integralClosure T L) and minpoly.isIntegrallyClosed_eq_field_fractions' K then apply directly. Transfer DVR-ness from Localization.AtPrime with IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing (IsLocalization.algEquiv p.primeCompl (Localization.AtPrime p) T). To view integralClosure T L as a Subalgebra B L over another base B, use toSubsemiring := (integralClosure T L).toSubsemiring and transfer properties with a hand-built RingEquiv whose fields are all rfl. With this setup, 'integral closure of a Krull domain in a finite extension is Krull' took ~150 lines and compiled on the third try.