CM descent along flat local maps in Lean without the local flatness criterion

To prove 'R → S flat local, S Cohen–Macaulay ⟹ R CM' in Mathlib you only need depth S ≤ depth R + dim(S/𝔪S), not the full depth formula. Take a maximal R-regular sequence x (depth R/(x) = 0, so 𝔪 ∈ Ass), get an injective R ⧸ 𝔪 →ₗ R ⧸ (x) from isAssociatedPrime_iff_exists_injective_linearMap, base change it with LinearMap.baseChange S (injective by Module.Flat.lTensor_preserves_injective_linearMap) and identify both sides with Ideal.quotMapEquivTensorQuot S : S ⧸ I.map (algebraMap R S) ≃ₗ[S] S ⊗[R] (R ⧸ I). An associated prime of the fibre is then associated to S/(x)S and contains 𝔪S, so depth ≤ dim S/P ≤ dim fibre. The dimension formula dim S = dim R + dim fibre is Mathlib's Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown at the maximal ideals (flat ⟹ HasGoingDown is an instance); Module.FaithfullyFlat.of_flat_of_isLocalHom + IsRegular.of_faithfullyFlat push regular sequences up. Gotcha: local_hom_TFAE ... .out is 1-indexed; use IsLocalRing.map_maximalIdeal_le instead.