awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Height
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

Tactic:
refine iSup_le fun I => ?_

Premises used: iSup_le
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
pos : ∀ (h : I = ⊤), (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
neg : ∀ (h : ¬I = ⊤), (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R
⊢ (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
by_cases h : I = ⊤
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
h : I = ⊤
⊢ (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
simp [h, ringKrullDim_nonneg_of_nontrivial]

Premises used: ringKrullDim_nonneg_of_nontrivial
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
h : ¬I = ⊤
⊢ (↑(⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
simp [h, height_le_ringKrullDim_of_ne_top]

Premises used: Ideal.height_le_ringKrullDim_of_ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ ringKrullDim R ≤ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞)

Tactic:
iSup_le fun p => WithBot.coe_le_coe.mpr (le_trans (b := p.last.asIdeal.height) ?_ ?_)

Premises used: Iff.mpr, Order.krullDim, WithBot.coe_le_coe, iSup_le, ringKrullDim, le_trans
-- Module: Mathlib.RingTheory.Ideal.Height
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
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
⊢ ringKrullDim R ≤ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞)

Tactic:
refine iSup_le fun p => WithBot.coe_le_coe.mpr (le_trans (b := p.last.asIdeal.height) ?_ ?_)

Premises used: iSup_le
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
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
⊢ (↑(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:
rw [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 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
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})) :
        ℕ∞))
a₁ :
  ⨆ (_ :
      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})) :
        ℕ∞) ≤
    (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.primeHeight
⊢ (↑(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:
apply le_trans (b := ⨆ (_ : p.last ≤ p.last), ↑p.length)

Premises used: le_trans
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ 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:
le_iSup (fun _ => (↑p.length : ℕ∞)) le_rfl

Premises used: le_rfl, le_iSup, RelSeries.length, Nat.cast
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ 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:
exact le_iSup (fun _ => (↑p.length : ℕ∞)) le_rfl

Premises used: le_rfl, le_iSup, RelSeries.length, Nat.cast
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
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 ≤
        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})) :
        ℕ∞) ≤
    (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:
le_iSup (fun p' => (⨆ _, p'.length : ℕ∞)) p

Premises used: _private.0.Ideal.primeHeight, Set.Mem, iSup, le_iSup, Order.height
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
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 ≤
        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})) :
        ℕ∞) ≤
    (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:
exact le_iSup (fun p' => (⨆ _, p'.length : ℕ∞)) p

Premises used: iSup, le_iSup
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
a :
  (RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          p).asIdeal.height ≤
    ⨆ (_ :
      (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal ≠
        ⊤),
      (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal.height
a₁ :
  LE.le (α := ℕ∞)
    (⨆ (_ :
      (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal ≠
        ⊤),
      (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)
⊢ (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:
apply le_trans (b := ⨆ (_ : (p.last).asIdeal ≠ ⊤), p.last.asIdeal.height)

Premises used: le_trans
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
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 ≤
    ⨆ (_ :
      (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal ≠
        ⊤),
      (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:
le_iSup_of_le p.last.isPrime.ne_top' le_rfl

Premises used: le_rfl, le_iSup_of_le, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
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 ≤
    ⨆ (_ :
      (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal ≠
        ⊤),
      (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:
exact le_iSup_of_le p.last.isPrime.ne_top' le_rfl

Premises used: le_rfl, le_iSup_of_le, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ LE.le (α := ℕ∞)
    (⨆ (_ :
      (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal ≠
        ⊤),
      (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:
le_iSup (fun I => ⨆ _, I.height) p.last.asIdeal

Premises used: RelSeries.last, iSup, le_iSup, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ LE.le (α := ℕ∞)
    (⨆ (_ :
      (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal ≠
        ⊤),
      (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:
exact le_iSup (fun I => ⨆ _, I.height) p.last.asIdeal

Premises used: RelSeries.last, iSup, le_iSup, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
rw : Eq (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
⊢ (↑(⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) : WithBot ℕ∞) = ringKrullDim R

Tactic:
rw [← sup_height_eq_ringKrullDim, WithBot.coe_inj]

Premises used: Ideal.sup_height_eq_ringKrullDim, WithBot.coe_inj
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
a : LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
a₁ : LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height)
⊢ Eq (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)

Tactic:
iSup_mono fun I => iSup_mono' fun hI => ⟨hI.ne_top, le_refl _⟩

Premises used: le_refl, iSup_mono', Exists.intro, Ideal.IsPrime.ne_top, Ideal.height, iSup_mono
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)

Tactic:
exact iSup_mono fun I => iSup_mono' fun hI => ⟨hI.ne_top, le_refl _⟩

Premises used: iSup_mono', Exists.intro, iSup_mono
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height)

Tactic:
iSup_mono' fun I => ?_

Premises used: iSup_mono'
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
a : ∀ (I : Ideal R), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
⊢ LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) (⨆ (I : Ideal R), ⨆ (_ : I.IsPrime), I.height)

Tactic:
refine iSup_mono' fun I => ?_

Premises used: iSup_mono'
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
pos : ∀ (I_top : I = ⊤), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
neg : ∀ (I_top : ¬I = ⊤), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)

Tactic:
by_cases I_top : I = ⊤
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : I = ⊤
⊢ LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : IsPrime.{u_1} (α := R) ⊥), height.{u_1} (R := R) ⊥)

Tactic:
simp [I_top]
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : I = ⊤
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)

Tactic:
exact ⟨⊥, by simp [I_top]⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
neg :
  ∀ (P : Ideal R) (hP : P ∈ I.minimalPrimes),
    ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)

Tactic:
obtain ⟨P, hP⟩ := Set.nonempty_coe_sort.mp (nonempty_minimalPrimes I_top)

Premises used: Set.nonempty_coe_sort, Ideal.nonempty_minimalPrimes, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)

Tactic:
⟨P, iSup_pos (α := ℕ∞) I_top ▸ le_iSup_of_le (hP.left.left) ?_⟩

Premises used: Eq.rec, iSup_pos, And.left, le_iSup_of_le, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
neg : I.height ≤ P.height
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsPrime), i'.height)

Tactic:
refine ⟨P, iSup_pos (α := ℕ∞) I_top ▸ le_iSup_of_le (hP.left.left) ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : ¬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
inst_1 : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
this : P.IsPrime
⊢ I.height ≤ P.height

Tactic:
iInf_le_of_le P (iInf_le_of_le hP (ge_of_eq (Ideal.height_eq_primeHeight P)))

Premises used: ge_of_eq, iInf_le_of_le, Ideal.height, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
I_top : ¬I = ⊤
P : Ideal R
hP : P ∈ I.minimalPrimes
this : P.IsPrime
⊢ I.height ≤ P.height

Tactic:
exact iInf_le_of_le P (iInf_le_of_le hP (ge_of_eq (Ideal.height_eq_primeHeight P)))

Premises used: iInf_le_of_le
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ (↑(⨆ (I : Ideal R), ⨆ (x : I.IsPrime), I.primeHeight) : WithBot ℕ∞) = ringKrullDim R

Tactic:
simp [← Ideal.height_eq_primeHeight, Ideal.sup_isPrime_height_eq_ringKrullDim]

Premises used: Ideal.sup_isPrime_height_eq_ringKrullDim, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
rw : Eq (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
⊢ (↑(⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) : WithBot ℕ∞) = ringKrullDim R

Tactic:
rw [← Ideal.sup_height_eq_ringKrullDim, WithBot.coe_inj]

Premises used: Ideal.sup_height_eq_ringKrullDim, WithBot.coe_inj
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
a : LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)
a₁ : LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height)
⊢ Eq (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)

Tactic:
iSup_mono fun I => iSup_mono' fun hI => ⟨hI.isPrime.ne_top , le_rfl⟩

Premises used: le_rfl, iSup_mono', Ideal.IsMaximal.isPrime, Exists.intro, Ideal.IsPrime.ne_top, iSup_mono
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height)

Tactic:
exact iSup_mono fun I => iSup_mono' fun hI => ⟨hI.isPrime.ne_top , le_rfl⟩

Premises used: iSup_mono', Exists.intro, iSup_mono
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height)

Tactic:
iSup_mono' fun I => ?_

Premises used: iSup_mono'
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
a : ∀ (I : Ideal R), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)
⊢ LE.le (α := ℕ∞) (⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) (⨆ (I : Ideal R), ⨆ (_ : I.IsMaximal), I.height)

Tactic:
refine iSup_mono' fun I => ?_

Premises used: iSup_mono'
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
I : Ideal R
a :
  ∃ (i' : Ideal R),
    LE.le (α := ℕ∞) (⨆ (_ : Ne.{u_1 + 1} (α := Ideal R) ⊤ ⊤), height.{u_1} (R := R) ⊤) (⨆ (_ : i'.IsMaximal), i'.height)
a₁ : ∀ (I_top : I ≠ ⊤), ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)
⊢ ∃ (i' : Ideal R), LE.le (α := ℕ∞) (⨆ (_ : I ≠ ⊤), I.height) (⨆ (_ : i'.IsMaximal), i'.height)

Tactic:
obtain rfl | I_top := eq_or_ne I ⊤

Premises used: eq_or_ne, Top.top, rfl