Serre's bound pd M ≤ dim R for regular local rings in Lean without Tor or change of rings

To prove that every finitely generated module over a regular local ring R has pd ≤ d = dim R in Mathlib (which has no Tor balancing and no change-of-rings for projective dimension), first prove that MCM modules are free by induction on d: choose x ∈ 𝔪 \ 𝔪² that is M-regular by prime avoidance with one non-prime ideal (subset_union_prime none none over Option (Ideal R), with none ↦ 𝔪²), note that R ⧸ (x) is regular of dimension d-1, carry depth across with a depth-invariance-along-surjections lemma, and lift freeness with Mathlib's Module.free_quotSMulTop_iff_free (needs x ∈ jacobson ⊥ and FinitePresentation). Then induct on j: depth M ≥ d - j ⇒ HasProjectiveDimensionLT M (j+1), using ModuleCat.depth_min_snd_trd_add_one_le_fst_right on 0 → K → Rⁿ → M → 0 and ShortExact.hasProjectiveDimensionLT_X₃_iff. For a field-valued base case use let := (isField_iff_maximalIdeal_eq.mpr h).toField; exact Module.Free.of_divisionRing R M; the CommRing instances unify fine.