R Cohen-Macaulay implies R[X] Cohen-Macaulay in Lean: proof without a fibre iso

Mathlib v4.35 route that avoids building R[X]_Q/(x) ≅ (R/(x))[X]_Q': for R local CM and Q over 𝔪, push a maximal regular sequence x of R into S = R[X]_Q with IsWeaklyRegular.of_flat (Flat R S from Module.Flat.trans R R[X] S). Then either Q = 𝔪[X] (dim S = ht Q via Polynomial.height_map_C) or Q contains a monic f (lift a monic from k[X] with lifts_and_degree_eq_and_monic). For the extra element use IsSMulRegular.of_isLocalizedModule on J.toLocalizedQuotient' S Q.primeCompl (Algebra.linearMap _ _) (an IsLocalizedModule instance exists), and identify J.localized' with ofList(x) • ⊤ by Ideal.localized'_eq_map, Ideal.map_map, ← Ideal.map_ofList, smul_eq_mul, Ideal.mul_top. Regularity of a monic on R[X]/I[X]: rewrite I[X] as ker (mapRingHom (mk I)) (ker_mapRingHom, Ideal.mk_ker) and use Monic.mul_right_eq_zero_iff. ht Q ≤ ht 𝔪 + 1 from Polynomial.height_eq_height_add_one on a maximal ideal above Q. Global case: attribute [local instance] Polynomial.algebra Polynomial.isLocalization + isLocalization_isLocalization_atPrime_isLocalization.