awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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
⊢ Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])

Tactic:
Set.disjoint_left.mpr fun a ⟨b, hb⟩ ha ↦ hb.1 ?_

Premises used: Iff.mpr, False, _private.0.Polynomial.height_eq_height_add_one.match_1, Set.disjoint_left, And.left
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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
refine :
  ∀ a ∈ (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]),
    ∀ (ha : a ∈ (↑P : Set R[X])) (b : R) (hb : b ∈ (↑p.primeCompl : Set R) ∧ (C : (a : R) → R[X]) b = a),
      b ∈ (↑p : Set R)
⊢ Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])

Tactic:
refine Set.disjoint_left.mpr fun a ⟨b, hb⟩ ha ↦ hb.1 ?_
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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
a : R[X]
h : a ∈ (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X])
ha : a ∈ (↑P : Set R[X])
b : R
hb : b ∈ (↑p.primeCompl : Set R) ∧ (C : (a : R) → R[X]) b = a
rwa : b ∈ p
rwa₁ : Membership.mem (γ := Ideal R) (under R P) b
rwa₂ : Membership.mem (α := R[X]) P ((algebraMap R R[X] : (a : R) → R[X]) b : R[X])
rwa₃ : Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) b : R[X])
rwa₄ rwa₅ rwa₆ rwa₇ : a ∈ P
⊢ b ∈ (↑p : Set R)

Tactic:
rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]

Premises used: And.right, SetLike.mem_coe, Ideal.LiesOver.over, Ideal.mem_comap, Polynomial.algebraMap_eq
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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
⊢ Disjoint (↑(Submonoid.map (F := R →+* R[X]) C p.primeCompl) : Set R[X]) (↑P : Set R[X])

Tactic:
have disj : Disjoint (p.primeCompl.map C : Set R[X]) P := by
    refine Set.disjoint_left.mpr fun a ⟨b, hb⟩ ha ↦ hb.1 ?_
    rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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])
⊢ 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
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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
⊢ IsMaximal (α := R[X]) (under R[X] P')

Tactic:
have : (P'.under R[X]).IsMaximal := eq.symm ▸ ‹P.IsMaximal›
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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'.IsMaximal

Tactic:
have : P'.IsMaximal := .of_isLocalization_of_disjoint (p.primeCompl.map C)
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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'.LiesOver p'

Tactic:
have : P'.LiesOver p' := liesOver_of_isPrime_of_disjoint p.primeCompl _ _ disj
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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'
h : Disjoint (↑p.primeCompl : Set R) (↑p : Set R)
⊢ p.height = p'.height

Tactic:
rw [height_map_of_disjoint p.primeCompl]

Premises used: IsLocalization.height_map_of_disjoint, Ideal.primeCompl
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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'
⊢ Disjoint (↑p.primeCompl : Set R) (↑p : Set R)

Tactic:
Disjoint.symm <| Set.disjoint_left.mpr fun _ a b ↦ b a

Premises used: Iff.mpr, Set.disjoint_left, Disjoint.symm
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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'
⊢ Disjoint (↑p.primeCompl : Set R) (↑p : Set R)

Tactic:
exact Disjoint.symm <| Set.disjoint_left.mpr fun _ a b ↦ b a

Premises used: Disjoint.symm
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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

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
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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
rw rw₁ : P.height = P.height
⊢ P.height = P'.height

Tactic:
rw [height_map_of_disjoint (Submonoid.map C <| p.primeCompl) _ disj]

Premises used: Polynomial.C, IsLocalization.height_map_of_disjoint, Submonoid.map, Ideal.primeCompl
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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

Tactic:
have eq2 : P.height = P'.height := by
    rw [height_map_of_disjoint (Submonoid.map C <| p.primeCompl) _ disj]
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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
rw : P'.height = p'.height + 1
⊢ P.height = p.height + 1

Tactic:
rw [eq1, eq2]
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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

Tactic:
apply height_eq_height_add_one_of_isMaximal p' P'

Premises used: _private.0.Polynomial.height_eq_height_add_one_of_isMaximal
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ ringKrullDim.{u_1} R[X] = ringKrullDim R + 1

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
refine_1 : ringKrullDim.{u_1} R[X] ≤ ringKrullDim R + 1
refine_2 : ringKrullDim R + 1 ≤ ringKrullDim.{u_1} R[X]
⊢ ringKrullDim.{u_1} R[X] = ringKrullDim R + 1

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ Nontrivial.{u_1} R[X]

Tactic:
nontriviality R[X]
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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

Tactic:
(ringKrullDim_le_iff_isMaximal_height_le (ringKrullDim R + 1)).mpr fun M hM ↦ ?_

Premises used: Iff.mpr, ringKrullDim_le_iff_isMaximal_height_le, HAdd.hAdd, ringKrullDim, OfNat.ofNat
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
h : Nontrivial.{u_1} R[X]
refine : ∀ (M : Ideal R[X]) (hM : M.IsMaximal), (↑M.height : WithBot ℕ∞) ≤ ringKrullDim R + 1
⊢ ringKrullDim.{u_1} R[X] ≤ ringKrullDim R + 1

Tactic:
refine (ringKrullDim_le_iff_isMaximal_height_le (ringKrullDim R + 1)).mpr fun M hM ↦ ?_

Premises used: Iff.mpr, ringKrullDim_le_iff_isMaximal_height_le, HAdd.hAdd, ringKrullDim, OfNat.ofNat
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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
rw : (↑(height (under R M)) : WithBot ℕ∞) + 1 ≤ ringKrullDim R + 1
⊢ (↑M.height : WithBot ℕ∞) ≤ ringKrullDim R + 1

Tactic:
rw [height_eq_height_add_one (M.under R) M, WithBot.coe_add, WithBot.coe_one]

Premises used: Polynomial.height_eq_height_add_one, WithBot.coe_one, WithBot.coe_add, Ideal.under
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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
bc : (↑(height (under R M)) : WithBot ℕ∞) ≤ ringKrullDim R
⊢ (↑(height (under R M)) : WithBot ℕ∞) + 1 ≤ ringKrullDim R + 1

Tactic:
gcongr
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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 ℕ∞) ≤ ringKrullDim R

Tactic:
Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

Premises used: Ideal.IsPrime.ne_top', Ideal.height_le_ringKrullDim_of_ne_top
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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 ℕ∞) ≤ ringKrullDim R

Tactic:
exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

Premises used: Ideal.IsPrime.ne_top', Ideal.height_le_ringKrullDim_of_ne_top
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ ringKrullDim R + 1 ≤ ringKrullDim.{u_1} R[X]

Tactic:
ringKrullDim_succ_le_ringKrullDim_polynomial

Premises used: ringKrullDim_succ_le_ringKrullDim_polynomial
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ ringKrullDim R + 1 ≤ ringKrullDim.{u_1} R[X]

Tactic:
exact ringKrullDim_succ_le_ringKrullDim_polynomial

Premises used: ringKrullDim_succ_le_ringKrullDim_polynomial
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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 ℕ∞)

Tactic:
H
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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)
h₁ : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
⊢ ringKrullDim (MvPolynomial β R) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)

Tactic:
convert! ← H using 1
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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 (MvPolynomial β R)

Tactic:
ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv

Premises used: ringKrullDim_eq_of_ringEquiv, AlgEquiv.toRingEquiv, MvPolynomial.renameEquiv
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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 (MvPolynomial β R)

Tactic:
exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv

Premises used: ringKrullDim_eq_of_ringEquiv, AlgEquiv.toRingEquiv, MvPolynomial.renameEquiv
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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 h₁ : ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
⊢ ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)

Tactic:
rw [Nat.card_congr e]

Premises used: Nat.card_congr
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
ι : Type u_2
inst_2 : Finite ι
⊢ ringKrullDim (MvPolynomial PEmpty.{u_2 + 1} R) = ringKrullDim R + (↑(Nat.card PEmpty.{u_2 + 1}) : WithBot ℕ∞)

Tactic:
simp
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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 ℕ∞)
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
⊢ ringKrullDim (MvPolynomial.{u_2, u_1} (Option α) R) = ringKrullDim R + (↑(Nat.card.{u_2} (Option α)) : WithBot ℕ∞)

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢

Premises used: add_assoc, Fintype.card_option, Nat.cast_add, Nat.cast_one, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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
h_option₂ h_option₃ :
  ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1 = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1
⊢ ringKrullDim (MvPolynomial.{u_2, u_1} (Option α) R) = ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1

Tactic:
rw [ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv,
      Polynomial.ringKrullDim_of_isNoetherianRing, IH]

Premises used: ringKrullDim_eq_of_ringEquiv, AlgEquiv.toRingEquiv, MvPolynomial.optionEquivLeft, Polynomial.ringKrullDim_of_isNoetherianRing
-- Module: Mathlib.RingTheory.KrullDimension.Polynomial
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 ℕ∞)
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 ℕ∞)
⊢ 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]

Premises used: Finite.induction_empty_option, add_assoc, ringKrullDim_eq_of_ringEquiv, Fintype.card_option, Nat.cast_add, AlgEquiv.toRingEquiv, MvPolynomial.optionEquivLeft, Polynomial.ringKrullDim_of_isNoetherianRing, Nat.cast_one, Nat.card_eq_fintype_card