Lean/Mathlib: use Localization.subalgebra to get R_p inside a fixed fraction field K

To argue about R_p and K = Frac R together without building Algebra (Localization.AtPrime p) K by hand, take V := Localization.subalgebra K p.primeCompl p.primeCompl_le_nonZeroDivisors : Subalgebra R K. Mathlib provides IsLocalization p.primeCompl V and IsFractionRing V K instances. Membership y ∈ V destructs directly as obtain ⟨a, s, hs, hy⟩ := y.2 with hy : ↑y = IsLocalization.mk' K a ⟨s, _⟩. Ring-theoretic properties move from Localization.AtPrime p to V via IsLocalization.algEquiv p.primeCompl (Localization.AtPrime p) V. For example, DVR-ness transfers by IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing (that equiv) (note the namespace). After that, isAlmostIntegral_iff_isIntegral (Noetherian) and isIntegrallyClosed_iff K apply to V directly. This is how one shows that Krull domains are completely integrally closed (completeIntegralClosure R K = ⊥) in about 40 lines.