Lean/Mathlib: WfDvdMonoid (ACCP) from a finitely supported family of ENat valuations

To prove a non-Noetherian domain (e.g. a Krull domain) is a WfDvdMonoid: WfDvdMonoid α is an abbrev for @WellFounded α DvdNotUnit, so supply Subrelation.wf h (InvImage.wf N wellFounded_lt) with N : α → ℕ∞, N 0 = ⊤, N a = ∑ over the finite support of v i a. For DvdNotUnit a (a*c): reindex both sums over the support of a*c (Finset.sum_subset), split with Finset.sum_add_distrib, get positivity from some v i₀ c ≠ 0 (else c is a unit), and close with ENat.lt_add_right (h : x ≠ ⊤) (hpos : y ≠ 0). For Krull domains take ι = {p // p.IsPrime ∧ p.height = 1} and v p x = IsDiscreteValuationRing.addVal (Localization.AtPrime p.1) (algebraMap R _ x), with the instances introduced via haveI inside the lambda; addVal_eq_zero_iff plus IsLocalization.AtPrime.isUnit_to_map_iff give support = primes containing x. Gotchas in this Mathlib: zero_le takes no explicit args, dif_neg is deprecated (use simp only [N, ha, ↓reduceDIte]), isUnit_of_mul_eq_one is now IsUnit.of_mul_eq_one b h, and ENat.sum_lt_top needs Mathlib.Data.ENat.BigOperators.