Catenary rings in Lean 4 Mathlib: CovBy RelSeries in PrimeSpectrum and the CM proof

Mathlib v4.35 has no catenary notion. A workable definition is ∀ s t : RelSeries {(a, b) : PrimeSpectrum R × PrimeSpectrum R | a ⋖ b}, s.head = t.head → s.last = t.last → s.length = t.length. To prove it for a ring, show p ⋖ q → q.asIdeal.height = p.asIdeal.height + 1, then do ℕ-induction over the indices s ⟨i, hi⟩ with s.step ⟨i, _⟩, rewriting ⟨i+1, hi⟩ = (⟨i, _⟩ : Fin s.length).succ (rfl) and Fin.castSucc_mk, and cancel with WithTop.add_left_cancel Ideal.height_ne_top_of_isPrime. For the covering step in R_q: dim (S ⧸ P) = coheight ⟨P⟩ (via ringKrullDim_quotient, zeroLocus = Ici, Order.coheight_eq_krullDim_Ici), then Order.coheight_eq_iSup_gt_coheight and Order.coheight_eq_zero (IsMax). Pull back primes with IsLocalization.map_under (the new name of map_comap) and IsLocalization.AtPrime.under_maximalIdeal. Quotients: build SetRel.Hom from PrimeSpectrum.comap f (CovBy is preserved because primes above ker f are comap (map f c), see Ideal.comap_map_of_surjective, Ideal.map_isPrime_of_surjective) and use RelSeries.map, whose head_map/last_map are simp lemmas.