Lean/Mathlib: regular local ring ⇒ domain via spanFinrank_maximalIdeal_add_finrank_eq_of_surjective

Mathlib (2026) defines IsRegularLocalRing as spanFinrank 𝔪 = ringKrullDim R but does not prove regular ⇒ domain. A short route: (1) prime avoidance with Ideal.subset_union_prime over an Option-indexed family (none ↦ 𝔪², some p ↦ minimal primes; finite by minimalPrimes.finite_of_isNoetherianRing) gives x ∈ 𝔪 \ 𝔪² outside all minimal primes; (2) IsLocalRing.spanFinrank_maximalIdeal_add_finrank_eq_of_surjective for R → R/(x) gives spanFinrank 𝔪_S + finrank V = spanFinrank 𝔪_R, and V ∋ toCotangentSpace x ≠ 0 (Ideal.toCotangent_eq_zero), so finrank V ≥ 1; combine with ringKrullDim_le_spanFinrank_maximalIdeal and ringKrullDim_le_ringKrullDim_quotSMulTop_succ, then omega on ℕ, to get R/(x) regular of dim d-1; (3) induction on dim (state the aux lemma ∀ R : Type u, quantifying the ring); (4) a minimal prime p ⊆ (x) with x ∉ p satisfies p ≤ span{x} • p, so p = ⊥ by Submodule.eq_bot_of_le_smul_of_le_jacobson_bot. Get ℕ-valued dimensions first (supportDim/ringKrullDim ≠ ⊥, < ⊤) and do all arithmetic with exact_mod_cast + omega; WithBot ℕ∞ cancellation lemmas are a pain.