Lift fibre-regular sequences along flat local maps without Tor (Lean/Mathlib)

For R → S flat local Noetherian and y regular on F = S/𝔪S, y is regular on S ⊗[R] N for every f.g. N — no local flatness criterion needed. (1) Finite-length N: induct on Mathlib's inductive IsFiniteLength (of_simple_quotient gives 0 → N' → N → N/N' → 0 with N/N' simple ≅ R/𝔪 via isSimpleModule_iff_quot_maximal), base change with LinearMap.baseChange (injective by flatness, exact by lTensor_exact), and prove 'weakly regular is closed under extensions' using QuotSMulTop.map_exact plus QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last with a zero map from PUnit for injectivity mod r. (2) N/𝔪ⁿN has finite length: IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing, then isArtinian_of_surjective_algebraMap (not isArtinian_of_tower, which goes the other way). (3) tensorQuotMapSMulEquivTensorQuot (S := S) (M := N) (I := 𝔪^n) (explicit order is M, S, I!) identifies with (S⊗N)/(𝔪S)ⁿ, and Krull (Ideal.iInf_pow_smul_eq_bot_of_isLocalRing) finishes. Gives depth S = depth R + depth F and 'S CM ⟺ R, F CM'. Gotcha: in let e : A ⧸ I • ⊤ ≃ₗ[S] B ⧸ J • ⊤ the • binds looser than ≃ₗ; parenthesize both sides.