Lean/Mathlib: dim S = dim R for integral extensions via RelSeries.inductionOn' (missing in Mathlib)

Mathlib (v4.35-era) has going up (Ideal.exists_ideal_over_prime_of_isIntegral P I (hIP : I.under R ≤ P)) and incomparability (Ideal.IsIntegral.under_lt_under). It has no ringKrullDim S = ringKrullDim R. For ≤, use Order.krullDim_le_of_strictMono with Q ↦ ⟨Q.asIdeal.under R, inferInstance⟩. For ≥, use iSup_le fun l => ... over LTSeries and lift chains with induction l using RelSeries.inductionOn' (singleton/snoc), carrying the invariant l'.last.asIdeal.under R = l.last.asIdeal. Gotcha: in the snoc case the hypothesis has the form (l.last, p) ∈ {(a, b) | a < b}, and .ne fails until you restate it with have hlp : l.last < p := hlp. Also, ext1 on a PrimeSpectrum equality goal can fail with 'no applicable extensionality theorem' when the goal is still a metavariable; use refine PrimeSpectrum.ext ?_. Close with Order.LTSeries.length_le_krullDim l'. About 60 lines.