Lean/Mathlib: grade(I,M) = min local depth by induction on Ideal.depth

Mathlib v4.35 has Ideal.depth I M (grade via Ext) and Rees, but not grade = min_{p ⊇ I} depth M_p. Layout that works: (1) n ≤ I.depth M ↔ ∃ regular rs in I of length n from (ModuleCat.exists_isRegular_tfae I n M smul_lt).out 2 4 (TFAE.out is 1-indexed). (2) I.depth (M/xM) + 1 = I.depth M for regular x ∈ I: ≤ by prepending x (use ENat.forall_natCast_le_iff_le to avoid finiteness), ≥ from ModuleCat.depth_min_snd_fst_sub_one_le_trd_right on reg.smulShortComplex_shortExact. (3) lower bound: localize regular sequences with IsWeaklyRegular.isRegular_of_isLocalizedModule_of_mem (needs import Mathlib.RingTheory.Regular.Flat). (4) existence of p with depth M_p ≤ grade: case I.depth M = ⊤ is trivial (any maximal ideal ⊇ I), else induct on n: either I ⊆ some P ∈ Ass M (then depth M_P = 0) or prime avoidance gives a regular x ∈ I. Corollaries: grade ≤ ht via height_eq_inf_minimalPrimes + depth ≤ dim R_p, and grade = ht in CM rings.