Lean/Mathlib: ht I + dim R/I ≤ dim R for any ideal via coheights in zeroLocus

General proof without minimal-prime bookkeeping or quotient isos (Mathlib v4.35). Case I = ⊤: R/⊤ is subsingleton, ringKrullDim_eq_bot_of_subsingleton, WithBot.add_bot. Otherwise get Nonempty instances for PrimeSpectrum.zeroLocus (I : Set R) and PrimeSpectrum R from a maximal ideal above I, then rw [ringKrullDim_quotient, Order.krullDim_eq_iSup_coheight_of_nonempty, ringKrullDim, Order.krullDim_eq_iSup_height_add_coheight_of_nonempty, ← WithBot.coe_add, WithBot.coe_le_coe, ENat.add_iSup] and close with iSup_le + add_le_add (b := Order.height a.1) _ (Order.coheight_le_coheight_apply_of_strictMono _ (Subtype.strictMono_coe _) a) + le_iSup (fun b ↦ height b + coheight b) a.1; the height part is PrimeSpectrum.height_eq_orderHeight + Ideal.height_mono a.2. Give le_iSup its function explicitly, otherwise unification fails. For the reverse in a CM local ring use Ideal.exists_isPrime_height_eq (a prime p ⊇ I with ht p = ht I) and ringKrullDim_le_of_surjective (Ideal.Quotient.factor h) (Ideal.Quotient.factor_surjective h).