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
I : Ideal R
⊢ I.height = ⨅ J ∈ I.minimalPrimes, J.height
have apply : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes), p.primeHeight = p.height
Tactic: apply iInf_congr (fun p ↦ iInf_congr fun hp ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ p.primeHeight = p.height
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
I : Ideal R
⊢ I.FiniteHeight ↔ I = ⊤ ∨ I.height < ⊤
have rw : I = ⊤ ∨ I.height ≠ ⊤ ↔ I = ⊤ ∨ I.height < ⊤
Tactic: rw [Ideal.finiteHeight_iff, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
rw : I = ⊤ ∨ I.height ≠ ⊤ ↔ I = ⊤ ∨ I.height < ⊤
⊢ I.FiniteHeight ↔ I = ⊤ ∨ I.height < ⊤
have rw₁ : I = ⊤ ∨ I.height ≠ ⊤ ↔ I = ⊤ ∨ I.height ≠ ⊤
Tactic: rw [Ideal.finiteHeight_iff, lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.FiniteHeight
inst_2 : I.IsPrime
⊢ I.primeHeight ≠ ⊤
have rw : I.height ≠ ⊤
Tactic: rw [← I.height_eq_primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.FiniteHeight
inst_2 : I.IsPrime
⊢ I.primeHeight < ⊤
have rw : I.height < ⊤
Tactic: rw [← I.height_eq_primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
inst_1 : p.IsPrime
inst_2 : p.FiniteHeight
⊢ ∃ (l : LTSeries (PrimeSpectrum R)),
    RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          l =
        { asIdeal := p, isPrime := ⋯ } ∧
      (↑(l.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) =
        p.height
have obtain : ∀ (n : ℕ) (hn : p.height = some n),
  ∃ (l : LTSeries (PrimeSpectrum R)),
    RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          l =
        { asIdeal := p, isPrime := sorry } ∧
      (↑(l.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) =
        p.height
Tactic: obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp (p.height_ne_top (IsPrime.ne_top ‹_›))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
inst_1 : p.IsPrime
inst_2 : p.FiniteHeight
n : ℕ
hn : p.height = some n
⊢ ∃ (l : LTSeries (PrimeSpectrum R)),
    RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          l =
        { asIdeal := p, isPrime := ⋯ } ∧
      (↑(l.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) =
        p.height
have rw : ∀ (hn : Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } = some n),
  ∃ (l : LTSeries (PrimeSpectrum R)),
    RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          l =
        { asIdeal := p, isPrime := sorry } ∧
      (↑(l.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) =
        Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R }
Tactic: rw [Ideal.height_eq_primeHeight, Ideal.primeHeight] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
inst_1 : p.IsPrime
inst_2 : p.FiniteHeight
n : ℕ
hn : Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } = some n
⊢ ∃ (l : LTSeries (PrimeSpectrum R)),
    RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          l =
        { asIdeal := p, isPrime := ⋯ } ∧
      (↑(l.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) =
        Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R }
have obtain : ∀ (l : LTSeries (PrimeSpectrum R))
  (last :
    RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        l =
      { asIdeal := p, isPrime := inst_1 })
  (len :
    l.length (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b}) =
      n),
  ∃ (l : LTSeries (PrimeSpectrum R)),
    RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          l =
        { asIdeal := p, isPrime := sorry } ∧
      (↑(l.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) =
        Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R }
Tactic: obtain ⟨l, last, len⟩ := Order.exists_series_of_height_eq_coe (⟨p, ‹_›⟩ : PrimeSpectrum R) hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
inst_1 : p.IsPrime
inst_2 : p.FiniteHeight
n : ℕ
hn : Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } = some n
l : LTSeries (PrimeSpectrum R)
last :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      l =
    { asIdeal := p, isPrime := inst_1 }
len :
  l.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b}) =
    n
⊢ ∃ (l : LTSeries (PrimeSpectrum R)),
    RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          l =
        { asIdeal := p, isPrime := ⋯ } ∧
      (↑(l.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) =
        Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R }
have rw : ∃ (l : LTSeries (PrimeSpectrum R)),
  RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        l =
      { asIdeal := p, isPrime := sorry } ∧
    (↑(l.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) =
      some n
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
inst_1 : p.IsPrime
inst_2 : p.FiniteHeight
n : ℕ
hn : Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } = some n
l : LTSeries (PrimeSpectrum R)
last :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      l =
    { asIdeal := p, isPrime := inst_1 }
len :
  l.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b}) =
    n
⊢ (↑(l.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    some n
have rw : (↑n : ℕ∞) = some n
Tactic: rw [len, WithTop.some_eq_coe, ENat.some_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
inst_1 : p.IsPrime
inst_2 : p.FiniteHeight
n : ℕ
hn : Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } = some n
l : LTSeries (PrimeSpectrum R)
last :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      l =
    { asIdeal := p, isPrime := inst_1 }
len :
  l.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b}) =
    n
rw : (↑n : ℕ∞) = some n
⊢ (↑(l.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    some n
have rw₁ : (↑n : ℕ∞) = (↑n : WithTop ℕ)
Tactic: rw [len, WithTop.some_eq_coe, ENat.some_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
inst_1 : p.IsPrime
inst_2 : p.FiniteHeight
n : ℕ
hn : Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } = some n
l : LTSeries (PrimeSpectrum R)
last :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      l =
    { asIdeal := p, isPrime := inst_1 }
len :
  l.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b}) =
    n
rw : (↑n : ℕ∞) = some n
rw₁ : (↑n : ℕ∞) = (↑n : WithTop ℕ)
⊢ (↑(l.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    some n
have rw₂ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : WithTop ℕ)
Tactic: rw [len, WithTop.some_eq_coe, ENat.some_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I ≤ J
⊢ I.height ≤ J.height
have simp : Order.height { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ≤
  Order.height { asIdeal := J, isPrime := inst_2 : PrimeSpectrum R }
Tactic: simp only [Ideal.height_eq_primeHeight, Ideal.primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I ≤ J
⊢ Order.height { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ≤
    Order.height { asIdeal := J, isPrime := inst_2 : PrimeSpectrum R }
have a : { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ≤ { asIdeal := J, isPrime := inst_2 }
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I < J
⊢ I.height + 1 ≤ J.height
have simp : Order.height { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } + 1 ≤
  Order.height { asIdeal := J, isPrime := inst_2 : PrimeSpectrum R }
Tactic: simp only [Ideal.height_eq_primeHeight, Ideal.primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
h : I ≤ J
⊢ I.height ≤ J.height
have simp : LE.le (α := ℕ∞) (⨅ J ∈ I.minimalPrimes, J.height) (⨅ J_1 ∈ J.minimalPrimes, J_1.height)
Tactic: simp only [I.height_eq_inf_minimalPrimes, J.height_eq_inf_minimalPrimes]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
h : I ≤ J
⊢ LE.le (α := ℕ∞) (⨅ J ∈ I.minimalPrimes, J.height) (⨅ J_1 ∈ J.minimalPrimes, J_1.height)
have refine : ∀ (p : Ideal R) (hp : p ∈ J.minimalPrimes), ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
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
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
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
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this : p.IsPrime
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
have obtain : ∀ (q : Ideal R) (hq : q ∈ I.minimalPrimes) (e : q ≤ p), ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
Tactic: obtain ⟨q, hq, e⟩ := Ideal.exists_minimalPrimes_le (h.trans hp.le)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this : p.IsPrime
q : Ideal R
hq : q ∈ I.minimalPrimes
e : q ≤ p
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
have this₁ : q.IsPrime
Tactic: have := hq.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
h : I < J
inst_2 : I.FiniteHeight
⊢ I.height < J.height
have pos : ∀ (hJ : J = ⊤), I.height < J.height
Tactic: by_cases hJ : J = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
h : I < J
inst_2 : I.FiniteHeight
pos : ∀ (hJ : J = ⊤), I.height < J.height
⊢ I.height < J.height
have neg : ∀ (hJ : ¬J = ⊤), I.height < J.height
Tactic: by_cases hJ : J = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
h : I < J
inst_2 : I.FiniteHeight
hJ : J = ⊤
⊢ I.height < J.height
have pos : I.height < ⊤
Tactic: grw [hJ, height_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
h : I < J
inst_2 : I.FiniteHeight
hJ : ¬J = ⊤
⊢ I.height < J.height
have neg : I.height + 1 ≤ ⨅ J_1 ∈ J.minimalPrimes, J_1.height
Tactic: rw [← ENat.add_one_le_iff (I.height_ne_top IsPrime.ne_top'), J.height_eq_inf_minimalPrimes]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
h : I < J
inst_2 : I.FiniteHeight
hJ : ¬J = ⊤
⊢ I.height + 1 ≤ ⨅ J_1 ∈ J.minimalPrimes, J_1.height
have neg : ∀ (K : Ideal R) (hK : K ∈ J.minimalPrimes), I.height + 1 ≤ K.height
Tactic: refine le_iInf₂ (fun K hK ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
h : I < J
inst_2 : I.FiniteHeight
hJ : ¬J = ⊤
K : Ideal R
hK : K ∈ J.minimalPrimes
⊢ I.height + 1 ≤ K.height
have this : K.IsPrime
Tactic: have := hK.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
h : I < J
inst_2 : I.FiniteHeight
hJ : ¬J = ⊤
K : Ideal R
hK : K ∈ J.minimalPrimes
this : K.IsPrime
⊢ I.height + 1 ≤ K.height
have this₁ : I < K
Tactic: have : I < K := lt_of_lt_of_le h hK.le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I < J
inst_3 : J.FiniteHeight
⊢ I.height < J.height
have this : I.FiniteHeight
Tactic: have : I.FiniteHeight := I.finiteHeight_iff.mpr
    (Or.inr (lt_of_le_of_lt (Ideal.height_mono h.le) (J.height_lt_top IsPrime.ne_top')).ne)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ (↑I.height : WithBot ℕ∞) ≤ ringKrullDim R
have rw : (↑(Order.height { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R }) : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: rw [Ideal.height_eq_primeHeight, Ideal.primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≠ ⊤
⊢ (↑I.height : WithBot ℕ∞) ≤ ringKrullDim R
have obtain : ∀ (P : Ideal R) (hP : P ∈ I.minimalPrimes), (↑I.height : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: obtain ⟨P, hP⟩ : Nonempty (I.minimalPrimes) := Ideal.nonempty_minimalPrimes h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ (↑I.height : WithBot ℕ∞) ≤ ringKrullDim R
have rw : (↑(⨅ J ∈ I.minimalPrimes, J.height) : WithBot ℕ∞) ≤ ringKrullDim R
Tactic: rw [I.height_eq_inf_minimalPrimes]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ (↑(⨅ J ∈ I.minimalPrimes, J.height) : WithBot ℕ∞) ≤ ringKrullDim R
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 : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := LTSeries.longestOf (PrimeSpectrum R)
⊢ ∃ (p : Ideal R), p.IsMaximal ∧ (↑p.height : WithBot ℕ∞) = ringKrullDim R
have obtain : ∀ (m : Ideal R) (hm : m.IsMaximal)
  (hle :
    (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          l).asIdeal ≤
      m),
  ∃ (p : Ideal R), p.IsMaximal ∧ (↑p.height : WithBot ℕ∞) = ringKrullDim R
Tactic: obtain ⟨m, hm, hle⟩ := l.last.asIdeal.exists_le_maximal IsPrime.ne_top'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := LTSeries.longestOf (PrimeSpectrum R)
m : Ideal R
hm : m.IsMaximal
hle :
  (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        l).asIdeal ≤
    m
⊢ ∃ (p : Ideal R), p.IsMaximal ∧ (↑p.height : WithBot ℕ∞) = ringKrullDim R
have refine : ringKrullDim R ≤ (↑m.height : WithBot ℕ∞)
Tactic: refine ⟨m, hm, le_antisymm (height_le_ringKrullDim_of_ne_top IsPrime.ne_top') ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := LTSeries.longestOf (PrimeSpectrum R)
m : Ideal R
hm : m.IsMaximal
hle :
  (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        l).asIdeal ≤
    m
⊢ ringKrullDim R ≤ (↑m.height : WithBot ℕ∞)
have trans : ringKrullDim R ≤
  (↑(RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            l).asIdeal.height :
    WithBot ℕ∞)
Tactic: trans (l.last.asIdeal.height : WithBot ℕ∞)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := LTSeries.longestOf (PrimeSpectrum R)
m : Ideal R
hm : m.IsMaximal
hle :
  (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        l).asIdeal ≤
    m
trans :
  ringKrullDim R ≤
    (↑(RelSeries.last (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              l).asIdeal.height :
      WithBot ℕ∞)
⊢ ringKrullDim R ≤ (↑m.height : WithBot ℕ∞)
have trans₁ : (↑(RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            l).asIdeal.height :
    WithBot ℕ∞) ≤
  (↑m.height : WithBot ℕ∞)
Tactic: trans (l.last.asIdeal.height : WithBot ℕ∞)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := LTSeries.longestOf (PrimeSpectrum R)
m : Ideal R
hm : m.IsMaximal
hle :
  (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        l).asIdeal ≤
    m
⊢ ringKrullDim R ≤
    (↑(RelSeries.last (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              l).asIdeal.height :
      WithBot ℕ∞)
have rw : ringKrullDim R ≤
  (↑(RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            l).asIdeal.primeHeight :
    WithBot ℕ∞)
Tactic: rw [Ideal.height_eq_primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := LTSeries.longestOf (PrimeSpectrum R)
m : Ideal R
hm : m.IsMaximal
hle :
  (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        l).asIdeal ≤
    m
⊢ (↑(RelSeries.last (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              l).asIdeal.height :
      WithBot ℕ∞) ≤
    (↑m.height : WithBot ℕ∞)
have norm_cast : (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        l).asIdeal.height ≤
  m.height
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I_1 I : Ideal R
inst_1 : FiniteRingKrullDim R
⊢ I.FiniteHeight
have rw : ¬I = ⊤ → (↑I.height : WithBot ℕ∞) < (↑⊤ : WithBot ℕ∞)
Tactic: rw [finiteHeight_iff, or_iff_not_imp_left, ← lt_top_iff_ne_top, ← WithBot.coe_lt_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
e : I ≤ J
inst_1 : J.IsPrime
inst_2 : J.FiniteHeight
e' : J.height ≤ I.height
⊢ J ∈ I.minimalPrimes
have obtain : ∀ (p : Ideal R) (h₁ : p ∈ I.minimalPrimes) (h₂ : p ≤ J), J ∈ I.minimalPrimes
Tactic: obtain ⟨p, h₁, h₂⟩ := Ideal.exists_minimalPrimes_le e
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
e : I ≤ J
inst_1 : J.IsPrime
inst_2 : J.FiniteHeight
e' : J.height ≤ I.height
p : Ideal R
h₁ : p ∈ I.minimalPrimes
h₂ : p ≤ J
⊢ J ∈ I.minimalPrimes
have h : J = p
Tactic: convert! h₁