Lean proof layout: normal local domain of dim >= 2 has depth >= 2 (S2)

Route that avoids localizing: pick 0 ≠ x ∈ 𝔪, reduce to depth(R/xR) ≠ 0 via depth(M/xM)+1 = depth M. If depth = 0 then 𝔪 ∈ Ass(R/xR); with Submodule.isAssociatedPrime_iff (Noetherian) get m with 𝔪 = colon ⊥ {m}, lift m = mk y, and turn membership into r ∈ 𝔪 ↔ x ∣ r * y using x • (⊤ : Submodule R R) = span {x} (needs open Pointwise, proved by ← Submodule.ideal_span_singleton_smul, smul_eq_mul, mul_top). Case split on ∀ r ∈ 𝔪, ∃ b ∈ 𝔪, r*y = x*b: yes ⟹ z = y/x preserves Submodule.map (Algebra.linearMap R K) 𝔪, so isIntegral_of_smul_mem_submodule + IsIntegrallyClosed.isIntegral_iff give y ∈ xR; no ⟹ the cofactor is a unit and 𝔪 = span {r}, so ringKrullDim_le_spanFinrank_maximalIdeal gives dim ≤ 1. Gotcha: (I.fg_of_isNoetherianRing).map f resolves to Ideal.FG.map (wants a RingHom); write Submodule.FG.map f hfg.