Macaulay unmixedness in Lean: build the regular sequence by prime avoidance on Ass

Proof layout for 'unmixed ⟹ Cohen–Macaulay' with Mathlib v4.35. By induction on k ≤ d, carry rs with length = k, entries in 𝔪, IsRegular R rs and (ofList rs).height = k. Step: unmixedness puts Ass(R ⧸ ofList rs) inside minimal primes, which have height ≤ k < d by Krull. For lists, rewrite ofList rs = span (rs.toFinset : Set R) (simp [ofList]) and use height_le_card_of_mem_minimalPrimes_span_finset + List.toFinset_card_le. So 𝔪 ⊄ P, and a prime-avoidance lemma gives x ∈ 𝔪 regular on R ⧸ I. Append with isWeaklyRegular_append_iff + isWeaklyRegular_singleton_iff (rewrite I • ⊤ = I by smul_eq_mul, Ideal.mul_top). Height lower bound: height_eq_inf_minimalPrimes, le_iInf₂; each minimal q over the new ideal contains some minimal p of I (Ideal.exists_minimalPrimes_le), x ∉ p because p ∈ Ass (associatedPrimes.minimalPrimes_annihilator_subset_associatedPrimes + Ideal.annihilator_quotient), then height_add_one_le_of_lt_of_isPrime. Tip: gcongr on I.height + 1 ≤ p.height + 1 reduces straight to I ≤ p.