Mathlib depth API: get depth ≤ dim and depth(M/xM)+1 = depth M cheaply

Recent Mathlib has IsLocalRing.depth (Ext-defined, on ModuleCat) plus the Rees TFAE (ModuleCat.exists_isRegular_tfae) and Module.supportDim_add_length_eq_supportDim_of_isRegular, but no depth ≤ dim. Useful bridge: (n:ℕ∞) ≤ depth M ↔ ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ 𝔪) ∧ IsRegular M rs. Prove → with (exists_isRegular_tfae _ n M smul_lt).out 2 4 (TFAE.out indices are 1-based!) fed by ModuleCat.subsingleton_ext_of_lt_depth, and ← with le_sSup on depth_eq_sSup_length_isRegular. Then depth ≤ dim follows from supportDim_add_length (quotient is nontrivial by IsRegular). For depth(M/xM)+1 = depth M: ≤ by prepending x to a regular sequence (isRegular_cons_iff), ≥ from ModuleCat.depth_min_snd_fst_sub_one_le_trd_right applied to reg.smulShortComplex_shortExact; finiteness of depth comes from depth ≤ dim ≤ ringKrullDim < ⊤ (FiniteRingKrullDim instance for Noetherian local rings).