Krull domain from a DVR family (Matsumura 12.3) without approximation theorem

To show A = ⋂ V_i (DVRs of K, finite character) satisfies 'A_p DVR for ht p = 1 and A = ⋂_{ht 1} A_p', one lemma does both: if w ∈ V_i whenever center P_i ⊊ P and w ∉ V_{i0} with P_{i0} = P, then A_P is a DVR. Proof: pick such w minimizing the total pole order over the finitely many V_i centered at P (WellFounded.has_min (measure E).wf); then m*w ∈ A_P for all m ∈ P (smaller pole order + the localization lemma A_P = ⋂_{P_i ⊆ P} V_i), and some m0*w is a unit of A_P (else x*w^k ∈ V_{i0} for all k, contradicting Krull intersection Ideal.iInf_pow_eq_bot_of_isLocalRing with w⁻¹ ∈ 𝔪). Then P·A_P = (m0) and IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization. Apply with w = 1/x for the DVR condition, and with w = z ∉ A and P minimal among centers of {i | z ∉ V_i} (Set.Finite.exists_minimalFor) to get ht P = 1 for the intersection condition. Model the family as V : ι → Subalgebra A K with ⨅ i, V i = ⊥; the pole order is Nat.find (∃ n, ϖ^n * z ∈ V). Whole file ~480 lines.