awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Height
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 ℕ)
rw₂ rw₃ : Eq (α := ℕ∞) (↑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

Tactic:
rw [len, WithTop.some_eq_coe, ENat.some_eq_coe]

Premises used: ENat.some_eq_coe, WithTop.some_eq_coe
-- Module: Mathlib.RingTheory.Ideal.Height
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})) :
          ℕ∞) =
        some n

Tactic:
exact ⟨l, last, by rw [len, WithTop.some_eq_coe, ENat.some_eq_coe]⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I ≤ J
simp :
  Order.height { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ≤
    Order.height { asIdeal := J, isPrime := inst_2 : PrimeSpectrum R }
⊢ I.height ≤ J.height

Tactic:
simp only [Ideal.height_eq_primeHeight, Ideal.primeHeight]

Premises used: _private.0.Ideal.primeHeight, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I ≤ J
a : { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ≤ { asIdeal := J, isPrime := inst_2 }
⊢ Order.height { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ≤
    Order.height { asIdeal := J, isPrime := inst_2 : PrimeSpectrum R }

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I ≤ J
⊢ { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ≤ { asIdeal := J, isPrime := inst_2 }

Tactic:
h

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I ≤ J
⊢ { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ≤ { asIdeal := J, isPrime := inst_2 }

Tactic:
exact h
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I ≤ J
⊢ I.primeHeight ≤ J.primeHeight

Tactic:
simpa [Ideal.height_eq_primeHeight] using Ideal.height_mono_of_isPrime h

Premises used: _private.0.Ideal.height_mono_of_isPrime, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I < J
simp :
  Order.height { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } + 1 ≤
    Order.height { asIdeal := J, isPrime := inst_2 : PrimeSpectrum R }
⊢ I.height + 1 ≤ J.height

Tactic:
simp only [Ideal.height_eq_primeHeight, Ideal.primeHeight]

Premises used: _private.0.Ideal.primeHeight, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
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 } + 1 ≤
    Order.height { asIdeal := J, isPrime := inst_2 : PrimeSpectrum R }

Tactic:
Order.height_add_one_le h

Premises used: Order.height_add_one_le
-- Module: Mathlib.RingTheory.Ideal.Height
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 } + 1 ≤
    Order.height { asIdeal := J, isPrime := inst_2 : PrimeSpectrum R }

Tactic:
exact Order.height_add_one_le h

Premises used: Order.height_add_one_le
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.IsPrime
inst_2 : J.IsPrime
h : I < J
⊢ I.primeHeight + 1 ≤ J.primeHeight

Tactic:
simpa [Ideal.height_eq_primeHeight] using Ideal.height_add_one_le_of_lt_of_isPrime h

Premises used: Ideal.height_add_one_le_of_lt_of_isPrime, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
⊢ height.{u_1} (R := R) ⊤ = ⊤

Tactic:
simp [height, minimalPrimes_top]

Premises used: Ideal.minimalPrimes_top, Ideal.height
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
h : I ≤ J
simp : LE.le (α := ℕ∞) (⨅ J ∈ I.minimalPrimes, J.height) (⨅ J_1 ∈ J.minimalPrimes, J_1.height)
⊢ I.height ≤ J.height

Tactic:
simp only [I.height_eq_inf_minimalPrimes, J.height_eq_inf_minimalPrimes]

Premises used: Ideal.height_eq_inf_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.Height
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)

Tactic:
le_iInf₂ (fun p hp ↦ ?_)

Premises used: le_iInf₂
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
h : I ≤ J
refine : ∀ (p : Ideal R) (hp : p ∈ J.minimalPrimes), ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
⊢ LE.le (α := ℕ∞) (⨅ J ∈ I.minimalPrimes, J.height) (⨅ J_1 ∈ J.minimalPrimes, J_1.height)

Tactic:
refine le_iInf₂ (fun p hp ↦ ?_)

Premises used: le_iInf₂
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
⊢ p.IsPrime

Tactic:
have := hp.isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
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
obtain : ∀ (q : Ideal R) (hq : q ∈ I.minimalPrimes) (e : q ≤ p), ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height

Tactic:
obtain ⟨q, hq, e⟩ := Ideal.exists_minimalPrimes_le (h.trans hp.le)

Premises used: Ideal.IsMinimalPrime.le, Ideal.exists_minimalPrimes_le, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Height
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
⊢ q.IsPrime

Tactic:
have := hq.isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this_1 : p.IsPrime
q : Ideal R
hq : q ∈ I.minimalPrimes
e : q ≤ p
this : q.IsPrime
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height

Tactic:
(iInf₂_le q hq).trans (Ideal.height_mono_of_isPrime e)

Premises used: iInf₂_le, _private.0.Ideal.height_mono_of_isPrime, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this_1 : p.IsPrime
q : Ideal R
hq : q ∈ I.minimalPrimes
e : q ≤ p
this : q.IsPrime
⊢ ⨅ J ∈ I.minimalPrimes, J.height ≤ p.height

Tactic:
exact (iInf₂_le q hq).trans (Ideal.height_mono_of_isPrime e)

Premises used: iInf₂_le, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Height
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
neg : ∀ (hJ : ¬J = ⊤), I.height < J.height
⊢ I.height < J.height

Tactic:
by_cases hJ : J = ⊤
-- Module: Mathlib.RingTheory.Ideal.Height
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 = ⊤
pos : I.height < ⊤
⊢ I.height < J.height

Tactic:
grw [hJ, height_top]

Premises used: Ideal.height_top
-- Module: Mathlib.RingTheory.Ideal.Height
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 < ⊤

Tactic:
I.height_lt_top IsPrime.ne_top'

Premises used: Ideal.height_lt_top, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.Height
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 < ⊤

Tactic:
exact I.height_lt_top IsPrime.ne_top'

Premises used: Ideal.height_lt_top, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.Height
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 = ⊤
neg : I.height + 1 ≤ ⨅ J_1 ∈ J.minimalPrimes, J_1.height
⊢ I.height < J.height

Tactic:
rw [← ENat.add_one_le_iff (I.height_ne_top IsPrime.ne_top'), J.height_eq_inf_minimalPrimes]

Premises used: ENat.add_one_le_iff, Ideal.IsPrime.ne_top', Ideal.height_ne_top, Ideal.height_eq_inf_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.Height
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

Tactic:
le_iInf₂ (fun K hK ↦ ?_)

Premises used: le_iInf₂
-- Module: Mathlib.RingTheory.Ideal.Height
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 = ⊤
neg : ∀ (K : Ideal R) (hK : K ∈ J.minimalPrimes), I.height + 1 ≤ K.height
⊢ I.height + 1 ≤ ⨅ J_1 ∈ J.minimalPrimes, J_1.height

Tactic:
refine le_iInf₂ (fun K hK ↦ ?_)

Premises used: le_iInf₂
-- Module: Mathlib.RingTheory.Ideal.Height
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
⊢ K.IsPrime

Tactic:
have := hK.isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
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 < K

Tactic:
have : I < K := lt_of_lt_of_le h hK.le
-- Module: Mathlib.RingTheory.Ideal.Height
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_1 : K.IsPrime
this : I < K
⊢ I.height + 1 ≤ K.height

Tactic:
Ideal.height_add_one_le_of_lt_of_isPrime this

Premises used: Ideal.height_add_one_le_of_lt_of_isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
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_1 : K.IsPrime
this : I < K
⊢ I.height + 1 ≤ K.height

Tactic:
exact Ideal.height_add_one_le_of_lt_of_isPrime this

Premises used: Ideal.height_add_one_le_of_lt_of_isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
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.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)
-- Module: Mathlib.RingTheory.Ideal.Height
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
this : I.FiniteHeight
⊢ I.height < J.height

Tactic:
Ideal.height_strict_mono_of_isPrime h

Premises used: Ideal.height_strict_mono_of_isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
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
this : I.FiniteHeight
⊢ I.height < J.height

Tactic:
exact Ideal.height_strict_mono_of_isPrime h

Premises used: Ideal.height_strict_mono_of_isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
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.primeHeight < J.primeHeight

Tactic:
simpa [← Ideal.height_eq_primeHeight] using Ideal.height_strict_mono_of_isPrime_of_isPrime h

Premises used: Ideal.height_strict_mono_of_isPrime_of_isPrime, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
rw : (↑(Order.height { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R }) : WithBot ℕ∞) ≤ ringKrullDim R
⊢ (↑I.height : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
rw [Ideal.height_eq_primeHeight, Ideal.primeHeight]

Premises used: _private.0.Ideal.primeHeight, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ (↑(Order.height { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R }) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
Order.height_le_krullDim _

Premises used: Order.height_le_krullDim, ringKrullDim
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ (↑(Order.height { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R }) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
exact Order.height_le_krullDim _

Premises used: Order.height_le_krullDim
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : I.FiniteHeight
J : Ideal R
h : I ≤ J
h_height : J.height ≤ I.height
⊢ I = J

Tactic:
eq_of_le_of_not_lt h fun hlt => not_le.mpr (Ideal.height_strict_mono_of_isPrime hlt) h_height

Premises used: not_le, Ideal.height_strict_mono_of_isPrime, Iff.mpr, eq_of_le_of_not_lt
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ (↑I.primeHeight : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
Order.height_le_krullDim _

Premises used: _private.0.Ideal.primeHeight, Order.height_le_krullDim, ringKrullDim
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≠ ⊤
⊢ Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)

Tactic:
Ideal.nonempty_minimalPrimes h

Premises used: Ideal.nonempty_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≠ ⊤
obtain : ∀ (P : Ideal R) (hP : P ∈ I.minimalPrimes), (↑I.height : WithBot ℕ∞) ≤ ringKrullDim R
⊢ (↑I.height : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
obtain ⟨P, hP⟩ : Nonempty (I.minimalPrimes) := Ideal.nonempty_minimalPrimes h

Premises used: Ideal.minimalPrimes, Ideal.nonempty_minimalPrimes, Set.Elem, Nonempty
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
rw : (↑(⨅ J ∈ I.minimalPrimes, J.height) : WithBot ℕ∞) ≤ ringKrullDim R
⊢ (↑I.height : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
rw [I.height_eq_inf_minimalPrimes]

Premises used: Ideal.height_eq_inf_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ P.IsPrime

Tactic:
have := hP.isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
this : P.IsPrime
⊢ (↑(⨅ J ∈ I.minimalPrimes, J.height) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
(WithBot.coe_le_coe.mpr (iInf₂_le _ hP)).trans P.height_le_ringKrullDim_of_isPrime

Premises used: Ideal.height_le_ringKrullDim_of_isPrime, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≠ ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
this : P.IsPrime
⊢ (↑(⨅ J ∈ I.minimalPrimes, J.height) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
refine (WithBot.coe_le_coe.mpr (iInf₂_le _ hP)).trans P.height_le_ringKrullDim_of_isPrime

Premises used: Ideal.height_le_ringKrullDim_of_isPrime, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
l : LTSeries (PrimeSpectrum R) := LTSeries.longestOf (PrimeSpectrum R)
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
⊢ ∃ (p : Ideal R), p.IsMaximal ∧ (↑p.height : WithBot ℕ∞) = ringKrullDim R

Tactic:
obtain ⟨m, hm, hle⟩ := l.last.asIdeal.exists_le_maximal IsPrime.ne_top'

Premises used: RelSeries.last, Ideal.exists_le_maximal, Ideal.IsPrime.ne_top', PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Ideal.Height
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

Tactic:
⟨m, hm, le_antisymm (height_le_ringKrullDim_of_ne_top IsPrime.ne_top') ?_⟩

Premises used: le_antisymm, And.intro, Exists.intro, Ideal.IsPrime.ne_top', Ideal.height_le_ringKrullDim_of_ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
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
refine : ringKrullDim R ≤ (↑m.height : WithBot ℕ∞)
⊢ ∃ (p : Ideal R), p.IsMaximal ∧ (↑p.height : WithBot ℕ∞) = ringKrullDim R

Tactic:
refine ⟨m, hm, le_antisymm (height_le_ringKrullDim_of_ne_top IsPrime.ne_top') ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Height
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 ℕ∞)
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 ℕ∞)
⊢ ringKrullDim R ≤ (↑m.height : WithBot ℕ∞)

Tactic:
trans (l.last.asIdeal.height : WithBot ℕ∞)

Premises used: WithBot.some, RelSeries.last, Ideal.height, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Ideal.Height
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
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 ℕ∞)
⊢ 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:
rw [Ideal.height_eq_primeHeight]

Premises used: _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
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.primeHeight :
      WithBot ℕ∞)

Tactic:
LTSeries.height_last_longestOf.symm.le

Premises used: _private.0.Ideal.primeHeight, RelSeries.last, Eq.le, ringKrullDim, LTSeries.height_last_longestOf, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Height
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.primeHeight :
      WithBot ℕ∞)

Tactic:
exact LTSeries.height_last_longestOf.symm.le

Premises used: Eq.le, LTSeries.height_last_longestOf, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Height
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
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
⊢ (↑(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:
norm_cast