awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (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:
height_mono hle

Premises used: Ideal.height_mono
-- 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
⊢ (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:
exact height_mono hle

Premises used: Ideal.height_mono
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I_1 I : Ideal R
inst_1 : FiniteRingKrullDim R
rw : ¬I = ⊤ → (↑I.height : WithBot ℕ∞) < (↑⊤ : WithBot ℕ∞)
⊢ I.FiniteHeight

Tactic:
rw [finiteHeight_iff, or_iff_not_imp_left, ← lt_top_iff_ne_top, ← WithBot.coe_lt_coe]

Premises used: Ideal.finiteHeight_iff, lt_top_iff_ne_top, WithBot.coe_lt_coe, Classical.or_iff_not_imp_left
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I_1 I : Ideal R
inst_1 : FiniteRingKrullDim R
⊢ ¬I = ⊤ → (↑I.height : WithBot ℕ∞) < (↑⊤ : WithBot ℕ∞)

Tactic:
fun h ↦ lt_of_le_of_lt (Ideal.height_le_ringKrullDim_of_ne_top h) ringKrullDim_lt_top

Premises used: lt_of_le_of_lt, ringKrullDim_lt_top, Ideal.height_le_ringKrullDim_of_ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I_1 I : Ideal R
inst_1 : FiniteRingKrullDim R
⊢ ¬I = ⊤ → (↑I.height : WithBot ℕ∞) < (↑⊤ : WithBot ℕ∞)

Tactic:
exact fun h ↦ lt_of_le_of_lt (Ideal.height_le_ringKrullDim_of_ne_top h) ringKrullDim_lt_top

Premises used: lt_of_le_of_lt, ringKrullDim_lt_top, Ideal.height_le_ringKrullDim_of_ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
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
obtain : ∀ (p : Ideal R) (h₁ : p ∈ I.minimalPrimes) (h₂ : p ≤ J), J ∈ I.minimalPrimes
⊢ J ∈ I.minimalPrimes

Tactic:
obtain ⟨p, h₁, h₂⟩ := Ideal.exists_minimalPrimes_le e

Premises used: Ideal.exists_minimalPrimes_le
-- Module: Mathlib.RingTheory.Ideal.Height
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
⊢ p ∈ I.minimalPrimes

Tactic:
h₁
-- Module: Mathlib.RingTheory.Ideal.Height
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
h : J = p
⊢ J ∈ I.minimalPrimes

Tactic:
convert! h₁
-- Module: Mathlib.RingTheory.Ideal.Height
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 = p

Tactic:
(eq_of_le_of_not_lt h₂ fun h₃ ↦ ?_).symm

Premises used: Eq.symm, eq_of_le_of_not_lt
-- Module: Mathlib.RingTheory.Ideal.Height
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
h : ∀ (h₃ : p < J), False
⊢ J = p

Tactic:
refine (eq_of_le_of_not_lt h₂ fun h₃ ↦ ?_).symm

Premises used: Eq.symm, eq_of_le_of_not_lt
-- Module: Mathlib.RingTheory.Ideal.Height
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
h₃ : p < J
⊢ p.IsPrime

Tactic:
have := h₁.isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
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
h₃ : p < J
this : p.IsPrime
⊢ p.FiniteHeight

Tactic:
have := finiteHeight_of_le h₂ IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.Height
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
h₃ : p < J
this_1 : p.IsPrime
this : p.FiniteHeight
⊢ False

Tactic:
lt_irrefl _ ((height_strict_mono_of_isPrime h₃).trans_le
    (e'.trans <| height_mono h₁.le))

Premises used: Ideal.height_strict_mono_of_isPrime, lt_irrefl, Ideal.IsMinimalPrime.le, Ideal.height_mono, LT.lt.trans_le, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Height
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
h₃ : p < J
this_1 : p.IsPrime
this : p.FiniteHeight
⊢ False

Tactic:
exact lt_irrefl _ ((height_strict_mono_of_isPrime h₃).trans_le
    (e'.trans <| height_mono h₁.le))

Premises used: Ideal.height_strict_mono_of_isPrime, lt_irrefl, Ideal.IsMinimalPrime.le, Ideal.height_mono, LT.lt.trans_le, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
rw :
  IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ↔
    Membership.mem (γ := Set (Ideal R)) {x : Ideal R | Minimal IsPrime x} I
⊢ I.height = 0 ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I

Tactic:
rw [Ideal.height_eq_primeHeight, Ideal.primeHeight, Order.height_eq_zero,
    minimalPrimes_eq_minimals]

Premises used: _private.0.Ideal.primeHeight, minimalPrimes_eq_minimals, Order.height_eq_zero, _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
⊢ IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ↔
    Membership.mem (γ := Set (Ideal R)) {x : Ideal R | Minimal IsPrime x} I

Tactic:
⟨fun h ↦ ⟨‹_›, ?_⟩, fun ⟨hI, hI'⟩ b hb ↦ hI' b.isPrime hb⟩

Premises used: PrimeSpectrum.mk, PrimeSpectrum.isPrime, LE.le, And.intro, Iff.intro, _private.0.Ideal.height_eq_zero_iff.match_1
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
refine : ∀ (h : IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R }) ⦃y : Ideal R⦄, y.IsPrime → y ≤ I → I ≤ y
⊢ IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R } ↔
    Membership.mem (γ := Set (Ideal R)) {x : Ideal R | Minimal IsPrime x} I

Tactic:
refine ⟨fun h ↦ ⟨‹_›, ?_⟩, fun ⟨hI, hI'⟩ b hb ↦ hI' b.isPrime hb⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
h : IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R }
by_contra! : ∀ (P : Ideal R) (hP₁ : P.IsPrime) (hP₂ : P ≤ I) (hP₃ : ¬I ≤ P), False
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → y ≤ I → I ≤ y

Tactic:
by_contra! ⟨P, ⟨hP₁, ⟨hP₂, hP₃⟩⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
h : IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R }
P : Ideal R
hP₁ : P.IsPrime
hP₂ : P ≤ I
hP₃ : ¬I ≤ P
⊢ False

Tactic:
hP₃ (h (b := ⟨P, hP₁⟩) hP₂)
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
h : IsMin { asIdeal := I, isPrime := inst_1 : PrimeSpectrum R }
P : Ideal R
hP₁ : P.IsPrime
hP₂ : P ≤ I
hP₃ : ¬I ≤ P
⊢ False

Tactic:
exact hP₃ (h (b := ⟨P, hP₁⟩) hP₂)
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
rw : I.height = 0 ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
rw₁ rw₂ :
  Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I
⊢ I.primeHeight = 0 ↔ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) I

Tactic:
rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_zero_iff]

Premises used: Ideal.height_eq_zero_iff, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
rw :
  LE.le (α := ℕ∞) 1
    (⨅ (J : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) J), J.height)
⊢ 1 ≤ height (R := R) (span {x})

Tactic:
rw [Ideal.height_eq_inf_minimalPrimes]

Premises used: Ideal.height_eq_inf_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ LE.le (α := ℕ∞) 1
    (⨅ (J : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) J), J.height)

Tactic:
le_iInf₂ fun q hq => ?_

Premises used: le_iInf₂
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
refine : ∀ (q : Ideal R) (hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) q), 1 ≤ q.height
⊢ LE.le (α := ℕ∞) 1
    (⨅ (J : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) J), J.height)

Tactic:
refine le_iInf₂ fun q hq => ?_

Premises used: le_iInf₂
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
q : Ideal R
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) q
⊢ q.IsPrime

Tactic:
have : q.IsPrime := hq.isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
q : Ideal R
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) q
this : q.IsPrime
rw : q ∉ minimalPrimes R
⊢ 1 ≤ q.height

Tactic:
rw [ENat.one_le_iff_ne_zero, Ne, height_eq_zero_iff]

Premises used: Ideal.height_eq_zero_iff, Ne, ENat.one_le_iff_ne_zero
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
q : Ideal R
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) q
this : q.IsPrime
hmin : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) q
⊢ False

Tactic:
absurd hx <| notMem_nonZeroDivisors_of_mem_mem_minimalPrimes
    (hq.1.2 <| Ideal.mem_span_singleton.mpr <| dvd_refl x) hmin

Premises used: Iff.mpr, notMem_nonZeroDivisors_of_mem_mem_minimalPrimes, absurd, And.right, And.left, Ideal.mem_span_singleton, dvd_refl
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
q : Ideal R
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) q
this : q.IsPrime
hmin : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) q
⊢ False

Tactic:
exact absurd hx <| notMem_nonZeroDivisors_of_mem_mem_minimalPrimes
    (hq.1.2 <| Ideal.mem_span_singleton.mpr <| dvd_refl x) hmin

Premises used: Iff.mpr, notMem_nonZeroDivisors_of_mem_mem_minimalPrimes, absurd, And.right, And.left, Ideal.mem_span_singleton, dvd_refl
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
obtain :
  ∀ (p : Ideal R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p), height.{u_1} (R := R) ⊥ = 0
⊢ height.{u_1} (R := R) ⊥ = 0

Tactic:
obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes (R := R) (I := ⊥) top_ne_bot.symm

Premises used: top_ne_bot, Ideal.nonempty_minimalPrimes, Ne.symm
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
rw : Eq (α := ℕ∞) (⨅ (J : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) J), J.height) 0
⊢ height.{u_1} (R := R) ⊥ = 0

Tactic:
rw [Ideal.height_eq_inf_minimalPrimes]

Premises used: Ideal.height_eq_inf_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
simp : ∃ (i : Ideal R) (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) i), i.height = 0
⊢ Eq (α := ℕ∞) (⨅ (J : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) J), J.height) 0

Tactic:
simp only [ENat.iInf_eq_zero]

Premises used: ENat.iInf_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
⊢ ∃ (i : Ideal R) (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) i), i.height = 0

Tactic:
⟨p, hp, haveI := hp.isPrime; height_eq_zero_iff.mpr hp⟩

Premises used: Iff.mpr, Ideal.height_eq_zero_iff, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
⊢ ∃ (i : Ideal R) (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) i), i.height = 0

Tactic:
refine ⟨p, hp, haveI := hp.isPrime; height_eq_zero_iff.mpr hp⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : Subsingleton R
rw : height.{u_1} (R := R) ⊤ = ⊤
rw₁ rw₂ : Eq (α := ℕ∞) ⊤ ⊤
⊢ I.height = ⊤

Tactic:
rw [Subsingleton.elim I ⊤, Ideal.height_top]

Premises used: Ideal.height_top, Subsingleton.elim, Top.top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
⊢ I ≠ ⊤

Tactic:
have h : I ≠ ⊤ := Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
obtain : ∀ (M : Ideal R) (hM : M.IsMaximal) (hM' : I ≤ M), I.IsMaximal
⊢ I.IsMaximal

Tactic:
obtain ⟨M, hM, hM'⟩ := Ideal.exists_le_maximal I h

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
inl : ∀ (hM' : I < M), I.IsMaximal
inr : ∀ (hM' : I = M), I.IsMaximal
⊢ I.IsMaximal

Tactic:
rcases lt_or_eq_of_le hM' with (hM' | hM')

Premises used: lt_or_eq_of_le
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'_1 : I ≤ M
hM' : I < M
⊢ I.height < M.height

Tactic:
have h1 := Ideal.height_strict_mono_of_isPrime hM'
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'_1 : I ≤ M
hM' : I < M
h1 : I.height < M.height
⊢ (↑M.height : WithBot ℕ∞) ≤ (↑I.height : WithBot ℕ∞)

Tactic:
have h2 := e ▸ M.height_le_ringKrullDim_of_ne_top hM.ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'_1 : I ≤ M
hM' : I < M
h1 : I.height < M.height
h2 : (↑M.height : WithBot ℕ∞) ≤ (↑I.height : WithBot ℕ∞)
⊢ I.IsMaximal

Tactic:
simp [← not_lt, h1] at h2

Premises used: not_lt
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'_1 : I ≤ M
hM' : I = M
⊢ I.IsMaximal

Tactic:
hM' ▸ hM

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.height : WithBot ℕ∞) = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'_1 : I ≤ M
hM' : I = M
⊢ I.IsMaximal

Tactic:
exact hM' ▸ hM
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
inst_2 : FiniteRingKrullDim R
e : (↑I.primeHeight : WithBot ℕ∞) = ringKrullDim R
⊢ (↑I.height : WithBot ℕ∞) = ringKrullDim R

Tactic:
simpa [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 : IsLocalRing R
rw :
  (↑(Order.height (α := PrimeSpectrum R) { asIdeal := maximalIdeal R, isPrime := ⋯ : PrimeSpectrum R }) : WithBot ℕ∞) =
    ringKrullDim R
⊢ (↑(height (maximalIdeal R)) : 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
inst_1 : IsLocalRing R
⊢ (↑(Order.height (α := PrimeSpectrum R) { asIdeal := maximalIdeal R, isPrime := ⋯ : PrimeSpectrum R }) : WithBot ℕ∞) =
    ringKrullDim R

Tactic:
Order.height_top_eq_krullDim

Premises used: Order.height_top_eq_krullDim, IsLocalRing.closedPoint, ringKrullDim
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
⊢ (↑(Order.height (α := PrimeSpectrum R) { asIdeal := maximalIdeal R, isPrime := ⋯ : PrimeSpectrum R }) : WithBot ℕ∞) =
    ringKrullDim R

Tactic:
exact Order.height_top_eq_krullDim

Premises used: Order.height_top_eq_krullDim
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
⊢ (↑(primeHeight (maximalIdeal R)) : WithBot ℕ∞) = ringKrullDim R

Tactic:
simp [← 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
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : I.IsPrime
mp : (↑I.height : WithBot ℕ∞) = ringKrullDim R → I = IsLocalRing.maximalIdeal R
mpr : I = IsLocalRing.maximalIdeal R → (↑I.height : WithBot ℕ∞) = ringKrullDim R
⊢ (↑I.height : WithBot ℕ∞) = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : I.IsPrime
h : (↑I.height : WithBot ℕ∞) = ringKrullDim R
⊢ I = IsLocalRing.maximalIdeal R

Tactic:
IsLocalRing.eq_maximalIdeal (Ideal.isMaximal_of_height_eq_ringKrullDim h)

Premises used: IsLocalRing.eq_maximalIdeal, Ideal.isMaximal_of_height_eq_ringKrullDim
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : I.IsPrime
h : (↑I.height : WithBot ℕ∞) = ringKrullDim R
⊢ I = IsLocalRing.maximalIdeal R

Tactic:
exact IsLocalRing.eq_maximalIdeal (Ideal.isMaximal_of_height_eq_ringKrullDim h)

Premises used: IsLocalRing.eq_maximalIdeal, Ideal.isMaximal_of_height_eq_ringKrullDim
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
inst_2 : IsLocalRing R
inst_3 : IsPrime (IsLocalRing.maximalIdeal R)
⊢ (↑(height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) = ringKrullDim R

Tactic:
IsLocalRing.maximalIdeal_height_eq_ringKrullDim

Premises used: IsLocalRing.maximalIdeal_height_eq_ringKrullDim
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
inst_2 : IsLocalRing R
inst_3 : IsPrime (IsLocalRing.maximalIdeal R)
⊢ (↑(height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) = ringKrullDim R

Tactic:
exact IsLocalRing.maximalIdeal_height_eq_ringKrullDim

Premises used: IsLocalRing.maximalIdeal_height_eq_ringKrullDim
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : FiniteRingKrullDim R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : I.IsPrime
rw : (↑I.height : WithBot ℕ∞) = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R
rw₁ rw₂ : I = IsLocalRing.maximalIdeal R ↔ I = IsLocalRing.maximalIdeal R
⊢ (↑I.primeHeight : WithBot ℕ∞) = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R

Tactic:
rw [← Ideal.height_eq_primeHeight, Ideal.height_eq_ringKrullDim_iff]

Premises used: Ideal.height_eq_ringKrullDim_iff, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : Ideal R
n : ℕ
inst_1 : p.IsPrime
rw :
  (∀ (a : Ideal R) (b : a.IsPrime),
      (Equiv.symm
                (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                  fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
              (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
            (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b) <
          { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } →
        Order.height (α := PrimeSpectrum R)
            ((Equiv.symm
                    (RelIso.toEquiv (r := fun (x1 x2 : PrimeSpectrum R) ↦ x1 ≤ x2) (s :=
                      fun (x1 x2 : { I : Ideal R // I.IsPrime }) ↦ x1 ≤ x2) (PrimeSpectrum.equivSubtype R)) :
                  (a : { I : Ideal R // I.IsPrime }) → PrimeSpectrum R)
                (Subtype.mk (p := fun (a : Ideal R) ↦ a.IsPrime) a b) :
              PrimeSpectrum R) <
          (↑n : ℕ∞)) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)
⊢ p.height ≤ (↑n : ℕ∞) ↔ ∀ (q : Ideal R), q.IsPrime → q < p → q.height < (↑n : ℕ∞)

Tactic:
rw [height_eq_primeHeight, primeHeight, Order.height_le_coe_iff,
    (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall]

Premises used: _private.0.Ideal.primeHeight, Equiv.forall_congr_left, PrimeSpectrum.equivSubtype, Subtype.forall, Order.height_le_coe_iff, RelIso.toEquiv, _private.0.Ideal.height_eq_primeHeight