Lean/Mathlib: prove a localization is a valuation ring via ValuationRing.cond, not fraction fields

To show S_P is a valuation ring when R ⊆ S ⊆ K = Frac R and R_{P∩R} is a DVR, don't set up IsFractionRing (Localization.AtPrime P) K. Mathlib's ValuationRing is intrinsic: refine { cond' := fun a b ↦ ?_ } asks for c with a*c = b ∨ b*c = a. Steps: (1) φ := IsLocalization.lift into K (units: nonzero images), injective via IsLocalization.lift_injective_iff. (2) For φ a, φ b ∈ K write them as α/σ, β/τ (IsFractionRing.div_surjective) and apply ValuationRing.cond in R_p to ατ, βσ. Destructure c with IsLocalization.mk'_surjective and use mk'_spec plus injectivity of R → R_p to get ατr = βσs in R. (3) Take c := IsLocalization.mk' Sp r ⟨s, _⟩ and check a*c = b after applying φ and cancelling s. DVR → ValuationRing → IsIntegrallyClosed are instances, so IsIntegrallyClosed.of_localization_maximal finishes. Gotcha: ValuationRing extends PreValuationRing, so ⟨⟨…⟩⟩ fails ('ValuationRing.mk does not have explicit fields'); use structure-instance syntax.