Regular quotients of regular local rings, with the dimension count

If R and R/I are regular local rings, there is a regular system of parameters x₁, …, xₙ of R an initial segment x₁, …, x_c of which generates I, and dim R/I + c = dim R ([TSPA, Tag 00NR] with [TSPA, Tag 00NQ]). Both halves are proved elsewhere (Hironaka/Algebra/Local/QuotientParameters.lean: IsRegularLocalRing.exists_span_eq_maximalIdeal_and_eq_span_image_lt; Hironaka/Algebra/Local/RegularSystem.lean: isRegularLocalRing_quotient_span_image_lt_and_ringKrullDim) and are bundled here in the form used for the Jacobian criterion of analytic spaces (Hironaka/AnalyticSpace/Jacobian.lean).

theorem IsLocalRing.exists_regularSystemOfParameters_of_quotient_and_ringKrullDim {R : Type u} [CommRing R] [IsRegularLocalRing R] (I : Ideal R) [IsRegularLocalRing (R ⧸ I)] : ∃ (n : ℕ) (c : ℕ) (x : Fin n → R), c ≤ n ∧ ↑n = ringKrullDim R ∧ maximalIdeal R = Ideal.span (Set.range x) ∧ I = Ideal.span (x '' {j : Fin n | ↑j < c}) ∧ ringKrullDim (R ⧸ I) + ↑c = ringKrullDim R

If R and R/I are regular local rings, there is a regular system of parameters x of R an initial segment of length c of which generates I, and dim R/I + c = dim R ([TSPA, Tag 00NR] and [TSPA, Tag 00NQ]).