Lean/Mathlib: R Krull ⟹ R⟦X⟧ Krull via a DVR family; three traps

Family in L = Frac R⟦X⟧: the X-adic ring R⟦X⟧_(X) plus (R_p⟦X⟧)_Q ∩ L for ht-1 p of R and ht-1 Q of the UFD R_p⟦X⟧ with X ∉ Q and Q ∩ R⟦X⟧ ≠ 0. Excluding X ∈ Q matters, because (X) gives the same valuation for every p, and with it finite character over indices fails. Restricting a DVR W ⊆ F along φ : L →+* F gives a DVR when it is not a field: take a minimal IsDiscreteValuationRing.addVal over I∖0 to get a generator, plus IsLocalRing.of_nonunits_add. Traps: (1) IsFractionRing.injective A K needs both arguments explicit inside .comp, or elaboration gets stuck. (2) Membership in Localization.subalgebra K S hS destructures as ⟨a, s, hs, he⟩ with he : z = mk' K a ⟨s, (proof s ∈ A⁰)⟩. So mk'_spec must be stated at ⟨s, hS hs⟩ (nonZeroDivisors), not at ⟨s, hs⟩ : S. (3) There is no global IsDomain (MvPowerSeries σ R), only NoZeroDivisors. Use attribute [local instance] NoZeroDivisors.to_isDomain for the finSuccEquiv induction, and put [IsDomain (MvPowerSeries σ R)] in the public instance.