awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
succ : span {x} ≤ I
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
have succ₁ : Submodule.spanRank (J ⊔ span {x}) ≤ (↑(r + 1) : Cardinal.{u_1})
Tactic: refine ⟨J ⊔ Ideal.span {x}, sup_le h₁ ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
succ : span {x} ≤ I
succ₁ : Submodule.spanRank (J ⊔ span {x}) ≤ (↑(r + 1) : Cardinal.{u_1})
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
have succ₂ : (↑(r + 1) : ℕ∞) ≤ (J ⊔ span {x}).height
Tactic: refine ⟨J ⊔ Ideal.span {x}, sup_le h₁ ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
⊢ span {x} ≤ I
have succ : {x} ⊆ (↑I : Set R)
Tactic: rwa [Ideal.span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
⊢ Submodule.spanRank (J ⊔ span {x}) ≤ (↑(r + 1) : Cardinal.{u_1})
have succ : Submodule.spanRank J + Submodule.spanRank (R := R) (span {x}) ≤ (↑(r + 1) : Cardinal.{u_1})
Tactic: apply Submodule.spanRank_sup_le_sum_spanRank.trans
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
⊢ Submodule.spanRank J + Submodule.spanRank (R := R) (span {x}) ≤ (↑(r + 1) : Cardinal.{u_1})
have succ : Submodule.spanRank J + Submodule.spanRank (R := R) (span {x}) ≤ HAdd.hAdd (α := Cardinal.{u_1}) (↑r : Cardinal.{u_1}) 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
⊢ (↑(r + 1) : ℕ∞) ≤ (J ⊔ span {x}).height
have succ : ∀ (p : Ideal R) (hp : p ∈ (J ⊔ span {x}).minimalPrimes), (↑(r + 1) : ℕ∞) ≤ p.primeHeight
Tactic: refine le_iInf₂ (fun p hp ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
⊢ (↑(r + 1) : ℕ∞) ≤ p.primeHeight
have this : p.IsPrime
Tactic: have := hp.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
⊢ (↑(r + 1) : ℕ∞) ≤ p.primeHeight
have succ : (↑(r + 1) : ℕ∞) ≤ p.height
Tactic: rw [← p.height_eq_primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
⊢ (↑(r + 1) : ℕ∞) ≤ p.height
have pos : ∀ (h : p.height = ⊤), (↑(r + 1) : ℕ∞) ≤ p.height
Tactic: by_cases h : p.height = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
pos : ∀ (h : p.height = ⊤), (↑(r + 1) : ℕ∞) ≤ p.height
⊢ (↑(r + 1) : ℕ∞) ≤ p.height
have neg : ∀ (h : ¬p.height = ⊤), (↑(r + 1) : ℕ∞) ≤ p.height
Tactic: by_cases h : p.height = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
h : ¬p.height = ⊤
⊢ (↑(r + 1) : ℕ∞) ≤ p.height
have this₁ : p.FiniteHeight
Tactic: have : p.FiniteHeight := ⟨Or.inr h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h : ¬p.height = ⊤
this : p.FiniteHeight
⊢ (↑(r + 1) : ℕ∞) ≤ p.height
have this₁ : J.height ≤ p.height
Tactic: have := Ideal.height_mono (le_sup_left.trans hp.le)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h : ¬p.height = ⊤
this_2 : p.FiniteHeight
this : J.height ≤ p.height
⊢ (↑(r + 1) : ℕ∞) ≤ p.height
have neg : (↑r : ℕ∞) ≠ p.height
Tactic: suffices h : (r : ℕ∞) ≠ p.height by
        exact Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h : ¬p.height = ⊤
this_2 : p.FiniteHeight
this : J.height ≤ p.height
e : (↑r : ℕ∞) = p.height
⊢ False
have neg : p ∈ S
Tactic: apply hx₂ p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h : ¬p.height = ⊤
this_2 : p.FiniteHeight
this : J.height ≤ p.height
e : (↑r : ℕ∞) = p.height
neg : p ∈ S
⊢ False
have neg₁ : x ∈ (↑p : Set R)
Tactic: apply hx₂ p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
hr : (↑r : ℕ∞) ≤ I.height
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
have zero : ∀ (hr : (↑0 : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑0 : Cardinal.{u_1}) ∧ (↑0 : ℕ∞) ≤ J.height
Tactic: induction r with
  | zero => simp
  | succ r ih =>
    obtain ⟨J, h₁, h₂, h₃⟩ := ih ((WithTop.coe_le_coe.mpr r.le_succ).trans hr)
    let S := { K | K ∈ J.minimalPrimes ∧ Ideal.height K = r }
    have hS : Set.Finite S := Set.Finite.subset J.finite_minimalPrimes_of_isNoetherianRing
      (fun _ h => h.1)
    have : ¬(I : Set R) ⊆ ⋃ K ∈ hS.toFinset, (K : Set R) := by
      refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_
      · rintro K hK - -
        rw [Set.Finite.mem_toFinset] at hK
        exact hK.1.isPrime
      · push Not
        intro K hK e
        have := hr.trans (Ideal.height_mono e)
        rw [Set.Finite.mem_toFinset] at hK
        rw [hK.2, ← not_lt] at this
        norm_cast at this
        exact this r.lt_succ_self
    simp_rw [Set.not_subset, Set.mem_iUnion, not_exists, Set.Finite.mem_toFinset] at this
    obtain ⟨x, hx₁, hx₂⟩ := this
    refine ⟨J ⊔ Ideal.span {x}, sup_le h₁ ?_, ?_, ?_⟩
    · rwa [Ideal.span_le, Set.singleton_subset_iff]
    · apply Submodule.spanRank_sup_le_sum_spanRank.trans
      push_cast
      exact add_le_add h₂ ((Submodule.spanRank_span_le_card _).trans (by simp))
    · refine le_iInf₂ (fun p hp ↦ ?_)
      have := hp.isPrime
      rw [← p.height_eq_primeHeight]
      by_cases h : p.height = ⊤
      · exact le_of_le_of_eq le_top h.symm
      have : p.FiniteHeight := ⟨Or.inr h⟩
      have := Ideal.height_mono (le_sup_left.trans hp.le)
      suffices h : (r : ℕ∞) ≠ p.height by
        exact Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)
      intro e
      apply hx₂ p
      · refine ⟨mem_minimalPrimes_of_height_eq (le_sup_left.trans hp.le) (e.symm.trans_le h₃),
          e.symm⟩
      · apply hp.le <| Ideal.mem_sup_right <| mem_span_singleton_self x
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
hr : (↑r : ℕ∞) ≤ I.height
zero : ∀ (hr : (↑0 : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑0 : Cardinal.{u_1}) ∧ (↑0 : ℕ∞) ≤ J.height
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
have succ : ∀ (r : ℕ)
  (ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height)
  (hr : (↑(r + 1) : ℕ∞) ≤ I.height),
  ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
Tactic: induction r with
  | zero => simp
  | succ r ih =>
    obtain ⟨J, h₁, h₂, h₃⟩ := ih ((WithTop.coe_le_coe.mpr r.le_succ).trans hr)
    let S := { K | K ∈ J.minimalPrimes ∧ Ideal.height K = r }
    have hS : Set.Finite S := Set.Finite.subset J.finite_minimalPrimes_of_isNoetherianRing
      (fun _ h => h.1)
    have : ¬(I : Set R) ⊆ ⋃ K ∈ hS.toFinset, (K : Set R) := by
      refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_
      · rintro K hK - -
        rw [Set.Finite.mem_toFinset] at hK
        exact hK.1.isPrime
      · push Not
        intro K hK e
        have := hr.trans (Ideal.height_mono e)
        rw [Set.Finite.mem_toFinset] at hK
        rw [hK.2, ← not_lt] at this
        norm_cast at this
        exact this r.lt_succ_self
    simp_rw [Set.not_subset, Set.mem_iUnion, not_exists, Set.Finite.mem_toFinset] at this
    obtain ⟨x, hx₁, hx₂⟩ := this
    refine ⟨J ⊔ Ideal.span {x}, sup_le h₁ ?_, ?_, ?_⟩
    · rwa [Ideal.span_le, Set.singleton_subset_iff]
    · apply Submodule.spanRank_sup_le_sum_spanRank.trans
      push_cast
      exact add_le_add h₂ ((Submodule.spanRank_span_le_card _).trans (by simp))
    · refine le_iInf₂ (fun p hp ↦ ?_)
      have := hp.isPrime
      rw [← p.height_eq_primeHeight]
      by_cases h : p.height = ⊤
      · exact le_of_le_of_eq le_top h.symm
      have : p.FiniteHeight := ⟨Or.inr h⟩
      have := Ideal.height_mono (le_sup_left.trans hp.le)
      suffices h : (r : ℕ∞) ≠ p.height by
        exact Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)
      intro e
      apply hx₂ p
      · refine ⟨mem_minimalPrimes_of_height_eq (le_sup_left.trans hp.le) (e.symm.trans_le h₃),
          e.symm⟩
      · apply hp.le <| Ideal.mem_sup_right <| mem_span_singleton_self x
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) = ringKrullDim R
have a : (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
a : (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
⊢ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) = ringKrullDim R
have a₁ : ringKrullDim R ≤ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
have a : ⨆ (i : Ideal R), (↑(⨆ (_ : i ≠ ⊤), i.height) : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: rw [WithBot.coe_iSup ⟨⊤, fun _ _ => le_top⟩]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ ⨆ (i : Ideal R), (↑(⨆ (_ : i ≠ ⊤), i.height) : WithBot ℕ∞) ≤ ringKrullDim R
have a : ∀ (I : Ideal R), (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: refine iSup_le fun I => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
⊢ (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
have pos : ∀ (h : I = ⊤), (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: by_cases h : I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
pos : ∀ (h : I = ⊤), (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
⊢ (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
have neg : ∀ (h : ¬I = ⊤), (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: by_cases h : I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ ringKrullDim R ≤ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞)
have a : ∀ (p : LTSeries (PrimeSpectrum R)),
  (↑(p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.height
Tactic: refine iSup_le fun p => WithBot.coe_le_coe.mpr (le_trans (b := p.last.asIdeal.height) ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
a :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    (↑(p.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal.height
⊢ ringKrullDim R ≤ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞)
have a₁ : ∀ (p : LTSeries (PrimeSpectrum R)),
  (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.height ≤
    ⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height
Tactic: refine iSup_le fun p => WithBot.coe_le_coe.mpr (le_trans (b := p.last.asIdeal.height) ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ (↑(p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.height
have a : (↑(p.length (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞) ≤
  (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        p).asIdeal.primeHeight
Tactic: rw [height_eq_primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ (↑(p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.primeHeight
have a : LE.le (α := ℕ∞)
  (↑(p.length (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})) :
    ℕ∞)
  (⨆ (_ :
    RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        p ≤
      RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        p),
    (↑(p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞))
Tactic: apply le_trans (b := ⨆ (_ : p.last ≤ p.last), ↑p.length)