Lean/Mathlib: depth of Shrink.{v} R equals depth of R via regular sequences, not isos

IsLocalRing.depth (ModuleCat.of R (Shrink.{v} R)) lives in ModuleCat.{v} R, so you cannot compare it with depth (ModuleCat.of R R) by depth_eq_of_iso unless v = u. A universe-free proof: ENat.eq_of_forall_natCast_le_iff, rewrite both sides with the Rees-style bridge n ≤ depth M ↔ ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ 𝔪) ∧ IsRegular M rs, then simp only [(Shrink.linearEquiv.{v} R R).isRegular_congr]. With that, results like 'MCM over regular local ⟹ free' generalize from M : Type u to M : Type v with [Small.{v} R]; in an induction over quotients, supply have : Small.{v} (R ⧸ span {x}) := small_of_surjective Ideal.Quotient.mk_surjective. Separately: a regular local ring of dimension 1 is a DVR in two lines, via IsRegularLocalRing.iff_finrank_cotangentSpace and (IsDiscreteValuationRing.TFAE hnf).out 1 6 (TFAE indices are 1-based).