awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this_1 : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
disj : Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
⊢ P.height = p.height + 1
have eq : under R[X] (B := Rₚ[X]) (Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P) = P
Tactic: have eq := under_map_of_isPrime_disjoint _ Rₚ[X] ‹P.IsMaximal›.isPrime disj
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this_1 : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
this : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
disj : Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
eq : under R[X] (B := Rₚ[X]) (Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P) = P
⊢ P.height = p.height + 1
have this₁ : IsMaximal (α := R[X]) (under R[X] P')
Tactic: have : (P'.under R[X]).IsMaximal := eq.symm ▸ ‹P.IsMaximal›
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this_1 : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
this_2 : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
disj : Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
eq : under R[X] (B := Rₚ[X]) (Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P) = P
this : IsMaximal (α := R[X]) (under R[X] P')
⊢ P.height = p.height + 1
have this₁ : P'.IsMaximal
Tactic: have : P'.IsMaximal := .of_isLocalization_of_disjoint (p.primeCompl.map C)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this_1 : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
this_2 : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
disj : Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
eq : under R[X] (B := Rₚ[X]) (Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P) = P
this_3 : IsMaximal (α := R[X]) (under R[X] P')
this : P'.IsMaximal
⊢ P.height = p.height + 1
have this₁ : P'.LiesOver p'
Tactic: have : P'.LiesOver p' := liesOver_of_isPrime_of_disjoint p.primeCompl _ _ disj
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this_1 : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
this_2 : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
disj : Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
eq : under R[X] (B := Rₚ[X]) (Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P) = P
this_3 : IsMaximal (α := R[X]) (under R[X] P')
this_4 : P'.IsMaximal
this : P'.LiesOver p'
⊢ p.height = p'.height
have h : Disjoint (↑p.primeCompl : Set R) (↑p : Set R)
Tactic: rw [height_map_of_disjoint p.primeCompl]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this_1 : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
this_2 : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
disj : Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
eq : under R[X] (B := Rₚ[X]) (Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P) = P
this_3 : IsMaximal (α := R[X]) (under R[X] P')
this_4 : P'.IsMaximal
this : P'.LiesOver p'
⊢ P.height = p.height + 1
have eq1 : p.height = p'.height
Tactic: have eq1 : p.height = p'.height := by
    rw [height_map_of_disjoint p.primeCompl]
    exact Disjoint.symm <| Set.disjoint_left.mpr fun _ a b ↦ b a
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this_1 : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
this_2 : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
disj : Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
eq : under R[X] (B := Rₚ[X]) (Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P) = P
this_3 : IsMaximal (α := R[X]) (under R[X] P')
this_4 : P'.IsMaximal
this : P'.LiesOver p'
eq1 : p.height = p'.height
⊢ P.height = P'.height
have rw : P.height = P.height
Tactic: rw [height_map_of_disjoint (Submonoid.map C <| p.primeCompl) _ disj]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this_1 : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
this_2 : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
disj : Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
eq : under R[X] (B := Rₚ[X]) (Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P) = P
this_3 : IsMaximal (α := R[X]) (under R[X] P')
this_4 : P'.IsMaximal
this : P'.LiesOver p'
eq1 : p.height = p'.height
⊢ P.height = p.height + 1
have eq2 : P.height = P'.height
Tactic: have eq2 : P.height = P'.height := by
    rw [height_map_of_disjoint (Submonoid.map C <| p.primeCompl) _ disj]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst_2 : P.IsMaximal
inst_3 : P.LiesOver p
this_1 : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) p
this_2 : p'.IsMaximal
P' : Ideal Rₚ[X] := Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P
disj : Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])
eq : under R[X] (B := Rₚ[X]) (Ideal.map (F := R[X] →+* Rₚ[X]) (algebraMap R[X] Rₚ[X]) P) = P
this_3 : IsMaximal (α := R[X]) (under R[X] P')
this_4 : P'.IsMaximal
this : P'.LiesOver p'
eq1 : p.height = p'.height
eq2 : P.height = P'.height
⊢ P.height = p.height + 1
have rw : P'.height = p'.height + 1
Tactic: rw [eq1, eq2]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ ringKrullDim.{u_1} R[X] = ringKrullDim R + 1
have refine_1 : ringKrullDim.{u_1} R[X] ≤ ringKrullDim R + 1
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
refine_1 : ringKrullDim.{u_1} R[X] ≤ ringKrullDim R + 1
⊢ ringKrullDim.{u_1} R[X] = ringKrullDim R + 1
have refine_2 : ringKrullDim R + 1 ≤ ringKrullDim.{u_1} R[X]
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ ringKrullDim.{u_1} R[X] ≤ ringKrullDim R + 1
have a : Nontrivial.{u_1} R[X]
Tactic: nontriviality R[X]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
h : Nontrivial.{u_1} R[X]
⊢ ringKrullDim.{u_1} R[X] ≤ ringKrullDim R + 1
have refine : ∀ (M : Ideal R[X]) (hM : M.IsMaximal), (↑M.height : WithBot ℕ∞) ≤ ringKrullDim R + 1
Tactic: refine (ringKrullDim_le_iff_isMaximal_height_le (ringKrullDim R + 1)).mpr fun M hM ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
h : Nontrivial.{u_1} R[X]
M : Ideal R[X]
hM : M.IsMaximal
⊢ (↑M.height : WithBot ℕ∞) ≤ ringKrullDim R + 1
have rw : (↑(height (under R M)) : WithBot ℕ∞) + 1 ≤ ringKrullDim R + 1
Tactic: rw [height_eq_height_add_one (M.under R) M, WithBot.coe_add, WithBot.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
h : Nontrivial.{u_1} R[X]
M : Ideal R[X]
hM : M.IsMaximal
⊢ (↑(height (under R M)) : WithBot ℕ∞) + 1 ≤ ringKrullDim R + 1
have bc : (↑(height (under R M)) : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
α β : Type u_2
e : α ≃ β
H : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞)
⊢ ringKrullDim (MvPolynomial β R) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
have h : ringKrullDim (MvPolynomial α R) = ringKrullDim (MvPolynomial β R)
Tactic: convert! ← H using 1
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
α β : Type u_2
e : α ≃ β
H : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞)
h : ringKrullDim (MvPolynomial α R) = ringKrullDim (MvPolynomial β R)
⊢ ringKrullDim (MvPolynomial β R) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
have h₁ : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
Tactic: convert! ← H using 1
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
α β : Type u_2
e : α ≃ β
H : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞)
⊢ ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
have h : ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
Tactic: rw [Nat.card_congr e]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
α : Type u_2
inst_3 : Fintype α
IH : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞)
⊢ ringKrullDim (MvPolynomial.{u_2, u_1} (Option α) R) = ringKrullDim R + (↑(Nat.card.{u_2} (Option α)) : WithBot ℕ∞)
have h_option : ∀ (IH : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞)),
  ringKrullDim (MvPolynomial.{u_2, u_1} (Option α) R) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
Tactic: simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
α : Type u_2
inst_3 : Fintype α
IH : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞)
⊢ ringKrullDim (MvPolynomial.{u_2, u_1} (Option α) R) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
have h_option : ringKrullDim (Polynomial (MvPolynomial α R)) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
Tactic: rw [ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv,
      Polynomial.ringKrullDim_of_isNoetherianRing, IH]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
α : Type u_2
inst_3 : Fintype α
IH : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞)
h_option : ringKrullDim (Polynomial (MvPolynomial α R)) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
⊢ ringKrullDim (MvPolynomial.{u_2, u_1} (Option α) R) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
have h_option₁ : ringKrullDim (MvPolynomial α R) + 1 = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
Tactic: rw [ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv,
      Polynomial.ringKrullDim_of_isNoetherianRing, IH]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
α : Type u_2
inst_3 : Fintype α
IH : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞)
h_option : ringKrullDim (Polynomial (MvPolynomial α R)) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
h_option₁ : ringKrullDim (MvPolynomial α R) + 1 = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
⊢ ringKrullDim (MvPolynomial.{u_2, u_1} (Option α) R) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
have h_option₂ : ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1 = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
Tactic: rw [ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv,
      Polynomial.ringKrullDim_of_isNoetherianRing, IH]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
⊢ ringKrullDim (MvPolynomial ι R) = ringKrullDim R + (↑(Nat.card ι) : WithBot ℕ∞)
have of_equiv : ∀ {α β : Type u_2} (e : α ≃ β) (H : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞)),
  ringKrullDim (MvPolynomial β R) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
Tactic: induction ι using Finite.induction_empty_option with
  | of_equiv e H =>
    convert! ← H using 1
    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
    · rw [Nat.card_congr e]
  | h_empty => simp
  | h_option IH =>
    simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
    rw [ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv,
      Polynomial.ringKrullDim_of_isNoetherianRing, IH]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
of_equiv :
  ∀ {α β : Type u_2} (e : α ≃ β) (H : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞)),
    ringKrullDim (MvPolynomial β R) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
⊢ ringKrullDim (MvPolynomial ι R) = ringKrullDim R + (↑(Nat.card ι) : WithBot ℕ∞)
have h_empty : ringKrullDim (MvPolynomial PEmpty.{u_2 + 1} R) = ringKrullDim R + (↑(Nat.card PEmpty.{u_2 + 1}) : WithBot ℕ∞)
Tactic: induction ι using Finite.induction_empty_option with
  | of_equiv e H =>
    convert! ← H using 1
    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
    · rw [Nat.card_congr e]
  | h_empty => simp
  | h_option IH =>
    simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
    rw [ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv,
      Polynomial.ringKrullDim_of_isNoetherianRing, IH]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Polynomial (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
of_equiv :
  ∀ {α β : Type u_2} (e : α ≃ β) (H : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞)),
    ringKrullDim (MvPolynomial β R) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
h_empty : ringKrullDim (MvPolynomial PEmpty.{u_2 + 1} R) = ringKrullDim R + (↑(Nat.card PEmpty.{u_2 + 1}) : WithBot ℕ∞)
⊢ ringKrullDim (MvPolynomial ι R) = ringKrullDim R + (↑(Nat.card ι) : WithBot ℕ∞)
have h_option : ∀ {α : Type u_2} [Fintype α] (IH : ringKrullDim (MvPolynomial α R) = ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞)),
  ringKrullDim (MvPolynomial.{u_2, u_1} (Option α) R) = ringKrullDim R + (↑(Nat.card.{u_2} (Option α)) : WithBot ℕ∞)
Tactic: induction ι using Finite.induction_empty_option with
  | of_equiv e H =>
    convert! ← H using 1
    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
    · rw [Nat.card_congr e]
  | h_empty => simp
  | h_option IH =>
    simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
    rw [ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv,
      Polynomial.ringKrullDim_of_isNoetherianRing, IH]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
q : LTSeries (↑(support R M) : Type u_1)
⊢ ∃ (p : LTSeries (↑(support R M) : Type u_1)),
    q.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ≤
        p.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ∧
      (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal.IsMaximal
have obtain : ∀ (m : Ideal R) (hmm : m.IsMaximal)
  (hm :
    (↑(RelSeries.last (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b})
              q) :
          PrimeSpectrum R).asIdeal ≤
      m),
  ∃ (p : LTSeries (↑(support R M) : Type u_1)),
    q.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ≤
        p.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ∧
      (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal.IsMaximal
Tactic: obtain ⟨m, hmm, hm⟩ := exists_le_maximal _ q.last.1.2.1
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
q : LTSeries (↑(support R M) : Type u_1)
m : Ideal R
hmm : m.IsMaximal
hm :
  (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            q) :
        PrimeSpectrum R).asIdeal ≤
    m
⊢ ∃ (p : LTSeries (↑(support R M) : Type u_1)),
    q.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ≤
        p.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ∧
      (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal.IsMaximal
have inl : ∀
  (hlt :
    (↑(RelSeries.last (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b})
              q) :
          PrimeSpectrum R).asIdeal <
      m),
  ∃ (p : LTSeries (↑(support R M) : Type u_1)),
    q.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ≤
        p.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ∧
      (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal.IsMaximal
Tactic: obtain hlt | rfl := lt_or_eq_of_le hm