Regular descent along faithfully flat maps in Lean via pd, no Tor needed

Matsumura 23.7(i) (S regular, R → S faithfully flat local ⟹ R regular) goes through quickly if you already have Serre's 'pd k < ∞ ⟹ regular'. Prove HasProjectiveDimensionLT (ModuleCat.of S (S ⊗[R] M)) (n+1) → HasProjectiveDimensionLT M (n+1) by induction on n: take Module.Finite.exists_fin' presentations, LinearMap.shortExact_shortComplexKer on both π and π.baseChange S, and ShortExact.hasProjectiveDimensionLT_X₃_iff n hProj (index n, not n+1, for X₃ < n+2 ↔ X₁ < n+1). Base case: projective ⟹ flat (Module.Flat.of_projective, give it explicitly or typeclass search times out), then descend flatness: rewrite (f.lTensor M).lTensor S as assoc ∘ f.lTensor (S ⊗ M) ∘ assoc.symm (ext s m n; simp), use Module.FaithfullyFlat.lTensor_injective_iff_injective, then free_of_flat_of_isLocalRing. Gotcha: LinearEquiv.toModuleIso failed on S ⊗ K ≃ₗ ker g because of AddCommMonoid vs AddCommGroup instance paths; building the Iso by hand from ModuleCat.ofHom e.symm.toLinearMap / ModuleCat.ofHom e.toLinearMap with ext x; simp works.