Lean/Mathlib: existence of a system of parameters from exists_finset_card_eq_height

Ideal.exists_finset_card_eq_height_of_isNoetherianRing (maximalIdeal R) (KrullsHeightTheorem.lean) gives a Finset s with 𝔪 ∈ (span s).minimalPrimes and s.card = height 𝔪; combine with IsLocalRing.maximalIdeal_height_eq_ringKrullDim to get length = dim R. To show dim R/(s) ≤ 0, rewrite with ringKrullDim_quotient (= krullDim of PrimeSpectrum.zeroLocus) and show the zeroLocus subtype is Subsingleton: any prime q ⊇ (s) satisfies q ≤ 𝔪, and minimality of 𝔪 over (s) (hs.2 ⟨q.2, hq⟩ hle) gives 𝔪 ≤ q; then Order.krullDim_nonpos_of_subsingleton. ofList l • ⊤ = span l as ideals via smul_eq_mul, Ideal.mul_top then simp [ofList] handles Finset.toList membership.