awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
⊢ under R Q ≤ p

Tactic:
have hQp' : Q.under _ ≤ p := by
    intro x hxQ
    by_contra hxp
    exact Set.subset_compl_iff_disjoint_right.mpr hQp hxQ ⟨x, hxp, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
hQp' : under R Q ≤ p
obtain :
  ∀ (Q' : Ideal S) (hQ'Q : Q' ≥ Q) (hQ' : Q'.IsPrime) (hQ'p : comap (F := R →+* S) (algebraMap R S) Q' = p), False
⊢ False

Tactic:
obtain ⟨Q', hQ'Q, hQ', hQ'p⟩ := Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime _ _ hQp'

Premises used: Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (F := R →+* S) (algebraMap R S) Q' = p
⊢ Q' = q

Tactic:
hq.le ⟨hQ', ⟨hQ'p.symm⟩⟩

Premises used: Set.Mem, setOf, Eq.le, Ideal.LiesOver.mk, And.intro, Set.singleton, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (F := R →+* S) (algebraMap R S) Q' = p
⊢ Q'.IsPrime

Tactic:
obtain rfl : Q' = q := hq.le ⟨hQ', ⟨hQ'p.symm⟩⟩

Premises used: Eq.le, Ideal.LiesOver.mk, And.intro, Eq.symm, rfl
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst_1 : CommRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_6 : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (F := R →+* S) (algebraMap R S) Q' = p
inst : Q'.IsPrime
⊢ Eq (α := Set (Ideal S)) (p.primesOver S) {Q'}

Tactic:
obtain rfl : Q' = q := hq.le ⟨hQ', ⟨hQ'p.symm⟩⟩

Premises used: Eq.le, Ideal.LiesOver.mk, And.intro, Eq.symm, rfl
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst_1 : CommRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_6 : Algebra.IsIntegral R S
x : S
hx : x ∉ q
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (F := R →+* S) (algebraMap R S) Q' = p
inst : Q'.IsPrime
hq₁ : Eq (α := Set (Ideal S)) (p.primesOver S) {Q'}
⊢ x ∉ Q'

Tactic:
obtain rfl : Q' = q := hq.le ⟨hQ', ⟨hQ'p.symm⟩⟩

Premises used: Eq.le, Ideal.LiesOver.mk, And.intro, Eq.symm, rfl
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
inst_4 : Algebra.IsIntegral R S
x : S
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (F := R →+* S) (algebraMap R S) Q' = p
inst_5 : Q'.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {Q'}
hx : x ∉ Q'
⊢ False

Tactic:
hx (hQ'Q (hxQ (Ideal.mem_span_singleton_self _)))

Premises used: Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
inst_4 : Algebra.IsIntegral R S
x : S
this : ∀ (r : R) (_ : r ∉ p) (c : S), c * x ≠ (algebraMap R S : (a : R) → S) r
Q : Ideal S
hQ : Q.IsPrime
hxQ : span {x} ≤ Q
hQp : Disjoint (↑Q : Set S) (↑(Algebra.algebraMapSubmonoid S p.primeCompl) : Set S)
hQp' : under R Q ≤ p
Q' : Ideal S
hQ'Q : Q' ≥ Q
hQ' : Q'.IsPrime
hQ'p : comap (F := R →+* S) (algebraMap R S) Q' = p
inst_5 : Q'.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {Q'}
hx : x ∉ Q'
⊢ False

Tactic:
exact hx (hQ'Q (hxQ (Ideal.mem_span_singleton_self _)))

Premises used: Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst_4 : P.LiesOver p
inst_5 : P.IsMaximal
⊢ IsMaximal (Ideal.under A P)

Tactic:
isMaximal_comap_of_isIntegral_of_isMaximal P

Premises used: Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst_4 : P.LiesOver p
hpm : p.IsMaximal
inst_5 : P.IsPrime
⊢ IsMaximal (Ideal.under A P)

Tactic:
rw [P.over_def p] at hpm

Premises used: Ideal.over_def
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst_4 : P.LiesOver p
hpm : p.IsMaximal
inst_5 : P.IsPrime
hpm₁ : IsMaximal (Ideal.under A P)
⊢ P.IsPrime

Tactic:
rw [P.over_def p] at hpm

Premises used: Ideal.over_def
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst_4 : P.LiesOver p
hpm : IsMaximal (Ideal.under A P)
inst_5 : P.IsPrime
⊢ P.IsMaximal

Tactic:
isMaximal_of_isIntegral_of_isMaximal_comap P hpm

Premises used: Ideal.isMaximal_of_isIntegral_of_isMaximal_comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst_4 : P.LiesOver p
hpm : IsMaximal (Ideal.under A P)
inst_5 : P.IsPrime
⊢ P.IsMaximal

Tactic:
exact isMaximal_of_isIntegral_of_isMaximal_comap P hpm

Premises used: Ideal.isMaximal_of_isIntegral_of_isMaximal_comap
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst_4 : P.LiesOver p
inst_5 : P.IsMaximal
rw : IsMaximal (Ideal.under A P)
⊢ p.IsMaximal

Tactic:
rw [P.over_def p]

Premises used: Ideal.over_def
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst_4 : P.LiesOver p
inst_5 : P.IsMaximal
⊢ IsMaximal (Ideal.under A P)

Tactic:
exact isMaximal_comap_of_isIntegral_of_isMaximal P

Premises used: Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
inst_4 : Nontrivial A
inst_5 : IsDomain B
h : LiesOver.{u_1, u_2} (A := A) P ⊥
⊢ P = ⊥

Tactic:
eq_bot_of_comap_eq_bot <| ((liesOver_iff _ _).mp h).symm

Premises used: Ideal.eq_bot_of_comap_eq_bot, Ideal.liesOver_iff, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
inst_4 : Nontrivial A
inst_5 : IsDomain B
hP : P ≠ ⊥
⊢ Ne (α := Ideal A) (under A P) ⊥

Tactic:
fun h ↦ hP <| eq_bot_of_comap_eq_bot h

Premises used: Ideal.eq_bot_of_comap_eq_bot, Not
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
P : Ideal B
p : Ideal A
inst_4 : P.LiesOver p
⊢ Algebra.IsIntegral.{u_1, u_2} (A ⧸ p) (B ⧸ P)

Tactic:
Algebra.IsIntegral.tower_top A

Premises used: Algebra.IsIntegral.tower_top
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
p : Ideal A
inst_1 : p.IsMaximal
B : Type u_2
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Algebra.IsIntegral A B
Q : (↑(p.primesOver B) : Type u_2)
⊢ (↑Q : Ideal B).IsMaximal

Tactic:
Ideal.IsMaximal.of_liesOver_isMaximal Q.1 p

Premises used: Ideal.IsMaximal.of_liesOver_isMaximal, Subtype.val
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
p : Ideal A
inst_1 : p.IsMaximal
B : Type u_2
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Algebra.IsIntegral A B
P : Ideal B
hP : Membership.mem (γ := Set (Ideal B)) (p.primesOver B) P
⊢ P.IsMaximal

Tactic:
primesOver.isMaximal ⟨P, hP⟩

Premises used: Subtype.mk, Ideal.primesOver.isMaximal
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
inst_4 : Module.IsTorsionFree A B
inst_5 : IsDomain A
inst_6 : IsDomain B
h :
  ∀ (p : Ideal B),
    Membership.mem (γ := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) p ↔
      Membership.mem (γ := Set (Ideal B)) {⊥} p
⊢ Eq (α := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) {⊥}

Tactic:
ext p
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
inst_4 : Module.IsTorsionFree A B
inst_5 : IsDomain A
inst_6 : IsDomain B
p : Ideal B
⊢ Membership.mem (γ := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) p ↔ Membership.mem (γ := Set (Ideal B)) {⊥} p

Tactic:
⟨fun ⟨_, ⟨h⟩⟩ ↦ p.eq_bot_of_comap_eq_bot h.symm, ?_⟩

Premises used: _private.0.Ideal.primesOver_bot.match_1, Ideal.eq_bot_of_comap_eq_bot, Membership.mem, Bot.bot, Iff.intro, Singleton.singleton, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
inst_4 : Module.IsTorsionFree A B
inst_5 : IsDomain A
inst_6 : IsDomain B
p : Ideal B
h :
  Membership.mem (γ := Set (Ideal B)) {⊥} p → Membership.mem (γ := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) p
⊢ Membership.mem (γ := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) p ↔ Membership.mem (γ := Set (Ideal B)) {⊥} p

Tactic:
refine ⟨fun ⟨_, ⟨h⟩⟩ ↦ p.eq_bot_of_comap_eq_bot h.symm, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
inst_4 : Module.IsTorsionFree A B
inst_5 : IsDomain A
inst_6 : IsDomain B
⊢ Membership.mem (γ := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) ⊥

Tactic:
⟨Ideal.isPrime_bot, Ideal.bot_liesOver_bot A B⟩

Premises used: Ideal.primesOver, Set.Mem, setOf, Ideal.isPrime_bot, And.intro, Ideal.bot_liesOver_bot
-- Module: Mathlib.RingTheory.Ideal.GoingUp
Goal:
A : Type u_1
inst : CommRing A
B : Type u_2
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Algebra.IsIntegral A B
inst_4 : Module.IsTorsionFree A B
inst_5 : IsDomain A
inst_6 : IsDomain B
⊢ Membership.mem (γ := Set (Ideal B)) (primesOver.{u_1, u_2} (A := A) ⊥ B) ⊥

Tactic:
exact ⟨Ideal.isPrime_bot, Ideal.bot_liesOver_bot A B⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
⊢ I.height = I.primeHeight

Tactic:
simp [height, primeHeight, Ideal.minimalPrimes_eq_subsingleton_self]

Premises used: _private.0.Ideal.primeHeight, Ideal.minimalPrimes_eq_subsingleton_self, Ideal.height
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
p : PrimeSpectrum R
⊢ p.asIdeal.height = Order.height p

Tactic:
p.asIdeal.height_eq_primeHeight

Premises used: _private.0.Ideal.primeHeight, PrimeSpectrum.asIdeal, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
apply : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes), p.primeHeight = p.height
⊢ I.height = ⨅ J ∈ I.minimalPrimes, J.height

Tactic:
apply iInf_congr (fun p ↦ iInf_congr fun hp ↦ ?_)

Premises used: iInf_congr
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
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 p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
⊢ p.primeHeight = p.height

Tactic:
(Ideal.height_eq_primeHeight _).symm

Premises used: Eq.symm, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
⊢ p.primeHeight = p.height

Tactic:
exact (Ideal.height_eq_primeHeight _).symm

Premises used: Eq.symm, _private.0.Ideal.height_eq_primeHeight
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
rw : I = ⊤ ∨ I.height ≠ ⊤ ↔ I = ⊤ ∨ I.height < ⊤
rw₁ rw₂ : I = ⊤ ∨ I.height ≠ ⊤ ↔ I = ⊤ ∨ I.height ≠ ⊤
⊢ I.FiniteHeight ↔ I = ⊤ ∨ I.height < ⊤

Tactic:
rw [Ideal.finiteHeight_iff, lt_top_iff_ne_top]

Premises used: Ideal.finiteHeight_iff, lt_top_iff_ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hI : I ≠ ⊤
inst_1 : I.FiniteHeight
⊢ I.height ≠ ⊤

Tactic:
(‹I.FiniteHeight›.eq_top_or_height_ne_top).resolve_left hI

Premises used: Ideal.FiniteHeight.eq_top_or_height_ne_top, Or.resolve_left
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
hI : I ≠ ⊤
inst_1 : I.FiniteHeight
⊢ I.height < ⊤

Tactic:
(Ideal.height_ne_top hI).lt_top

Premises used: Ne.lt_top, Ideal.height_ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.FiniteHeight
inst_2 : I.IsPrime
⊢ I.height ≠ ⊤

Tactic:
Ideal.height_ne_top ‹I.IsPrime›.ne_top

Premises used: Ideal.height_ne_top, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.FiniteHeight
inst_2 : I.IsPrime
rw : I.height ≠ ⊤
⊢ I.primeHeight ≠ ⊤

Tactic:
rw [← I.height_eq_primeHeight]

Premises used: _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.FiniteHeight
inst_2 : I.IsPrime
⊢ I.height ≠ ⊤

Tactic:
exact Ideal.height_ne_top ‹I.IsPrime›.ne_top

Premises used: Ideal.height_ne_top, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.FiniteHeight
inst_2 : I.IsPrime
⊢ I.height < ⊤

Tactic:
Ideal.height_lt_top ‹I.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 : Ideal R
inst_1 : I.FiniteHeight
inst_2 : I.IsPrime
rw : I.height < ⊤
⊢ I.primeHeight < ⊤

Tactic:
rw [← I.height_eq_primeHeight]

Premises used: _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.FiniteHeight
inst_2 : I.IsPrime
⊢ I.height < ⊤

Tactic:
exact Ideal.height_lt_top ‹I.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
p : Ideal R
inst_1 : p.IsPrime
inst_2 : p.FiniteHeight
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 := ⋯ } ∧
        (↑(l.length (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) =
          p.height
⊢ ∃ (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

Tactic:
obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp (p.height_ne_top (IsPrime.ne_top ‹_›))

Premises used: Option.ne_none_iff_exists', Iff.mp, Ideal.height_ne_top, Ideal.IsPrime.ne_top
-- 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 : p.height = some n
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 := ⋯ } ∧
        (↑(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 }
⊢ ∃ (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

Tactic:
rw [Ideal.height_eq_primeHeight, Ideal.primeHeight] at hn ⊢

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
p : Ideal R
inst_1 : p.IsPrime
inst_2 : p.FiniteHeight
n : ℕ
hn : Order.height { asIdeal := p, isPrime := inst_1 : PrimeSpectrum R } = some n
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 := ⋯ } ∧
        (↑(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 }
⊢ ∃ (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 }

Tactic:
obtain ⟨l, last, len⟩ := Order.exists_series_of_height_eq_coe (⟨p, ‹_›⟩ : PrimeSpectrum R) hn

Premises used: PrimeSpectrum.mk, Order.exists_series_of_height_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
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 := ⋯ } ∧
      (↑(l.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) =
        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 }

Tactic:
rw [hn]