Auslander–Buchsbaum in Lean/Mathlib: induction on pd, Mathlib depth lemma, one Ext trick

Mathlib (v4.35-era) already has everything except one step: ModuleCat.depth_min_snd_trd_add_one_le_fst_right / depth_min_snd_fst_sub_one_le_trd_right (depth lemma for 0→K→F→M→0), ShortComplex.ShortExact.projectiveDimension_X₃_eq_succ_of_not_projective (pd K = pd M - 1), LinearMap.shortExact_shortComplexKer, and Module.free_of_flat_of_isLocalRing. Induct on n = pd M with a minimal presentation (kernel ⊆ 𝔪•Rⁿ; build it from Module.finBasis k (k ⊗ M) lifted via TensorProduct.mk_surjective and span_eq_top_of_tmul_eq_basis). The only case the depth lemma does not settle is pd M = 1 (K free, depth K = depth R); there show K→F induces 0 on Ext(k,-): with K projective and image in 𝔪•F, lift through (Fin s → F) → F, (x_j) ↦ Σ m_j x_j (m generators of 𝔪) via Module.projective_lifting_property, so f = Σ m_j • ψ_j and use Ext.mk₀_sum, Ext.comp_sum, Ext.mk₀_smul, Ext.comp_smul; then Ext.covariant_sequence_exact₁ gives a nonzero Ext^{d-1}(k,M). For depth of free F use IsWeaklyRegular.isWeaklyRegular_rTensor + TensorProduct.lid (≥) and a retract argument on Ext (≤). Finish arithmetic by pulling every ℕ∞ to ℕ, rw [min_le_iff], norm_cast, omega (Nat.cast_min fails for ℕ∞: no IsStrictOrderedRing).