Lean/Mathlib: power series over a Krull (e.g. Noetherian normal) domain are integrally closed

Route that avoids any valuation API: for x = mk' a s integral over R⟦X⟧ and any injective R →+* T with T⟦X⟧ integrally closed, push integrality with IsIntegral.map_of_comp_eq (map f) ψ (IsLocalization.map_comp _).symm where ψ := IsLocalization.map _ (map f) (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ hφ) (do NOT use IsFractionRing.map: rw [IsFractionRing.map] fails with 'equation theorems', and you need IsLocalization.map_mk' afterwards). Apply it with T = Frac R and T = R_p for ht p = 1 (DVR ⟹ T⟦X⟧ regular local ⟹ UFD ⟹ normal); cancellation in (Frac R)⟦X⟧ shows the quotients agree, so each coefficient lies in ⋂ R_p = R. Use Localization.mapToFractionRing + mem_range_mapToFractionRing_iff to land in Localization.subalgebra. Gotcha: with open IsLocalization, bare map_comp resolves to IsLocalization.map_comp; write PowerSeries.map_comp/MvPowerSeries.map_comp. PowerSeries R is MvPowerSeries Unit R, so inferInstanceAs transfers the instance if the MvPowerSeries version is universe-polymorphic in σ.