awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
w : IsLocalRing R
this_1 : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑(insert x s') : Set R))) (maximalIdeal R)
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
t_1 : (↑(↑s' : Set R) : Type u_1) → R
ht : Set.range t_1 ⊆ (↑q : Set R)
hspan : (↑s' : Set R) ⊆ (↑(radical (span (Set.range t_1) ⊔ span {x})) : Set R)
t : Finset R := Finset.image t_1 Finset.univ
rw :
  ∀ (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x (↑s' : Set R)))) (maximalIdeal R))
    (this : maximalIdeal R ≤ (q ⊔ span {x}).radical) (h : (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R))
    (t : (↑(↑s' : Set R) : Type u_1) → R) (ht : Set.range t ⊆ (↑q : Set R))
    (hspan : (↑s' : Set R) ⊆ (↑(radical (span (Set.range t) ⊔ span {x})) : Set R)),
    let t := Finset.image t Finset.univ;
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) q
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) q

Tactic:
rw [Finset.coe_insert] at hp

Premises used: Finset.coe_insert
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
w : IsLocalRing R
this_1 : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x (↑s' : Set R)))) (maximalIdeal R)
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
t_1 : (↑(↑s' : Set R) : Type u_1) → R
ht : Set.range t_1 ⊆ (↑q : Set R)
hspan : (↑s' : Set R) ⊆ (↑(radical (span (Set.range t_1) ⊔ span {x})) : Set R)
t : Finset R := Finset.image t_1 Finset.univ
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (Set.range t_1))) q

Tactic:
mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert hpq _ _ hp _ ht ?_

Premises used: Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
w : IsLocalRing R
this_1 : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x (↑s' : Set R)))) (maximalIdeal R)
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
t_1 : (↑(↑s' : Set R) : Type u_1) → R
ht : Set.range t_1 ⊆ (↑q : Set R)
hspan : (↑s' : Set R) ⊆ (↑(radical (span (Set.range t_1) ⊔ span {x})) : Set R)
t : Finset R := Finset.image t_1 Finset.univ
h₁ : (↑t : Set R) = Set.range t_1
convert! : (↑s' : Set R) ⊆ (↑(radical (span (insert x (Set.range t_1)))) : Set R)
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) q

Tactic:
convert! mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert hpq _ _ hp _ ht ?_

Premises used: Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
w : IsLocalRing R
this_1 : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x (↑s' : Set R)))) (maximalIdeal R)
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
t_1 : (↑(↑s' : Set R) : Type u_1) → R
ht : Set.range t_1 ⊆ (↑q : Set R)
hspan : (↑s' : Set R) ⊆ (↑(radical (span (Set.range t_1) ⊔ span {x})) : Set R)
t : Finset R := Finset.image t_1 Finset.univ
⊢ (↑t : Set R) = Set.range t_1

Tactic:
simp [t]
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
w : IsLocalRing R
this_1 : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x (↑s' : Set R)))) (maximalIdeal R)
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
t_1 : (↑(↑s' : Set R) : Type u_1) → R
ht : Set.range t_1 ⊆ (↑q : Set R)
hspan : (↑s' : Set R) ⊆ (↑(radical (span (Set.range t_1) ⊔ span {x})) : Set R)
t : Finset R := Finset.image t_1 Finset.univ
⊢ (↑s' : Set R) ⊆ (↑(radical (span (insert x (Set.range t_1)))) : Set R)

Tactic:
hspan.trans <| radical_mono ?_

Premises used: Ideal.radical_mono, HasSubset.Subset.trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
w : IsLocalRing R
this_1 : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x (↑s' : Set R)))) (maximalIdeal R)
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
t_1 : (↑(↑s' : Set R) : Type u_1) → R
ht : Set.range t_1 ⊆ (↑q : Set R)
hspan : (↑s' : Set R) ⊆ (↑(radical (span (Set.range t_1) ⊔ span {x})) : Set R)
t : Finset R := Finset.image t_1 Finset.univ
refine : LE.le (α := Ideal R) (span (Set.range t_1) ⊔ span {x}) (span (insert x (Set.range t_1)))
⊢ (↑s' : Set R) ⊆ (↑(radical (span (insert x (Set.range t_1)))) : Set R)

Tactic:
refine hspan.trans <| radical_mono ?_

Premises used: Ideal.radical_mono, HasSubset.Subset.trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R)
      (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p) (hn : s.card = m),
      p.height ≤ (↑m : ℕ∞)
w : IsLocalRing R
this_1 : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
x : R
s' : Finset R
hxs' : x ∉ s'
hxq : x ∉ q
hn : (insert x s').card ≤ n + 1
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x (↑s' : Set R)))) (maximalIdeal R)
this : maximalIdeal R ≤ (q ⊔ span {x}).radical
h : (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
t_1 : (↑(↑s' : Set R) : Type u_1) → R
ht : Set.range t_1 ⊆ (↑q : Set R)
hspan : (↑s' : Set R) ⊆ (↑(radical (span (Set.range t_1) ⊔ span {x})) : Set R)
t : Finset R := Finset.image t_1 Finset.univ
rw : LE.le (α := Ideal R) (span (Set.range t_1) ⊔ span {x}) (span (Set.range t_1 ∪ {x}))
rw₁ rw₂ : LE.le (α := Ideal R) (span (Set.range t_1) ⊔ span {x}) (span (Set.range t_1) ⊔ span {x})
⊢ LE.le (α := Ideal R) (span (Set.range t_1) ⊔ span {x}) (span (insert x (Set.range t_1)))

Tactic:
rw [← Set.union_singleton, span_union]

Premises used: Ideal.span_union, Set.union_singleton
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hI : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
trans : p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank (span (↑s : Set R)))
trans₁ :
  LE.le (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank (span (↑s : Set R))) : ℕ∞)
    ((↑s.card : ℕ∞) : ℕ∞)
⊢ p.height ≤ (↑s.card : ℕ∞)

Tactic:
trans (Cardinal.toENat (Submodule.spanRank (Ideal.span (s : Set R))))

Premises used: SetLike.coe, Cardinal.toENat, Ideal.span, DFunLike.coe, Submodule.spanRank
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hI : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
⊢ p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank (span (↑s : Set R)))

Tactic:
Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes _ _ hI

Premises used: Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hI : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
⊢ p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank (span (↑s : Set R)))

Tactic:
exact Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes _ _ hI

Premises used: Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hI : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
⊢ LE.le (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank (span (↑s : Set R))) : ℕ∞)
    ((↑s.card : ℕ∞) : ℕ∞)

Tactic:
simpa using Submodule.spanRank_span_le_card (s : Set R)

Premises used: Submodule.spanRank_span_le_card, SetLike.coe
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Set R
hs : s.Finite
hI : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span s)) p
rw : p.height ≤ (↑hs.toFinset (s := s).card : ℕ∞)
⊢ p.height ≤ (↑s.ncard : ℕ∞)

Tactic:
rw [s.ncard_eq_toFinset_card hs]

Premises used: Set.ncard_eq_toFinset_card
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Set R
hs : s.Finite
hI : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span s)) p
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑(hs.toFinset (s := s)) : Set R))) p

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Set R
hs : s.Finite
hI : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span s)) p
⊢ p.height ≤ (↑hs.toFinset (s := s).card : ℕ∞)

Tactic:
exact Ideal.height_le_card_of_mem_minimalPrimes_span_finset (by simpa)

Premises used: Ideal.height_le_card_of_mem_minimalPrimes_span_finset
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
obtain :
  ∀ (J : Ideal R) (hJ : J ∈ I.minimalPrimes),
    I.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)
⊢ I.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)

Tactic:
obtain ⟨J, hJ⟩ := nonempty_minimalPrimes hI

Premises used: Ideal.nonempty_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ : J ∈ I.minimalPrimes
rw :
  LE.le (α := ℕ∞) (⨅ J ∈ I.minimalPrimes, J.height : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
⊢ I.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)

Tactic:
rw [I.height_eq_inf_minimalPrimes]

Premises used: Ideal.height_eq_inf_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ : J ∈ I.minimalPrimes
⊢ LE.le (α := ℕ∞) (⨅ J ∈ I.minimalPrimes, J.height : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)

Tactic:
(iInf₂_le J hJ).trans (I.height_le_spanRank_toENat_of_mem_minimalPrimes J hJ)

Premises used: iInf₂_le, Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ : J ∈ I.minimalPrimes
⊢ LE.le (α := ℕ∞) (⨅ J ∈ I.minimalPrimes, J.height : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)

Tactic:
exact (iInf₂_le J hJ).trans (I.height_le_spanRank_toENat_of_mem_minimalPrimes J hJ)

Premises used: iInf₂_le, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
rw :
  Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (↑(Submodule.spanFinrank I) : Cardinal.{u_1}) : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑(Submodule.spanFinrank I) : ℕ∞) (↑(Submodule.spanFinrank I) : ℕ∞)
⊢ Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)

Tactic:
rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I), map_natCast]

Premises used: Submodule.fg_iff_spanRank_eq_spanFinrank, Iff.mpr, IsNoetherian.noetherian, map_natCast
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)

Tactic:
have : I.spanFinrank = I.spanRank.toENat := by
    rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I), map_natCast]
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
this :
  Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
⊢ I.height ≤ (↑(Submodule.spanFinrank I) : ℕ∞)

Tactic:
this ▸ height_le_spanRank_toENat I hI

Premises used: Eq.rec, Ideal.height_le_spanRank_toENat, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
this :
  Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
⊢ I.height ≤ (↑(Submodule.spanFinrank I) : ℕ∞)

Tactic:
exact this ▸ height_le_spanRank_toENat I hI
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
trans :
  (↑I.height : Cardinal.{u_1}) ≤
    (↑((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)) : Cardinal.{u_1})
trans₁ :
  (↑((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)) : Cardinal.{u_1}) ≤ Submodule.spanRank I
⊢ (↑I.height : Cardinal.{u_1}) ≤ Submodule.spanRank I

Tactic:
trans ↑I.spanRank.toENat

Premises used: Cardinal.toENat, DFunLike.coe, Submodule.spanRank
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ (↑I.height : Cardinal.{u_1}) ≤
    (↑((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)) : Cardinal.{u_1})

Tactic:
exact_mod_cast I.height_le_spanRank_toENat hI

Premises used: Ideal.height_le_spanRank_toENat
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ (↑((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)) : Cardinal.{u_1}) ≤ Submodule.spanRank I

Tactic:
I.spanRank.ofENat_toENat_le

Premises used: Cardinal.ofENat_toENat_le, Submodule.spanRank
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ (↑((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)) : Cardinal.{u_1}) ≤ Submodule.spanRank I

Tactic:
exact I.spanRank.ofENat_toENat_le

Premises used: Cardinal.ofENat_toENat_le, Submodule.spanRank
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
⊢ I.FiniteHeight

Tactic:
finiteHeight_iff_lt.mpr <| Or.elim (em (I = ⊤)) Or.inl
  fun h ↦ Or.inr <| (I.height_le_spanFinrank h).trans_lt (ENat.coe_lt_top _)

Premises used: Iff.mpr, Ideal.height_le_spanFinrank, em, Submodule.spanFinrank, Ideal.finiteHeight_iff_lt, Or.inl, Top.top, Or.elim, LE.le.trans_lt, Eq, Or.inr, ENat.coe_lt_top
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
apply : ringKrullDim R ≠ ⊥ ∧ ringKrullDim R ≠ ⊤
⊢ FiniteRingKrullDim R

Tactic:
apply finiteRingKrullDim_iff_ne_bot_and_top.mpr

Premises used: Iff.mpr, finiteRingKrullDim_iff_ne_bot_and_top
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
rw :
  (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊥ ∧
    (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊤
⊢ ringKrullDim R ≠ ⊥ ∧ ringKrullDim R ≠ ⊤

Tactic:
rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim]

Premises used: IsLocalRing.maximalIdeal_height_eq_ringKrullDim
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
left : (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊥
right : (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊤
⊢ (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊥ ∧
    (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊤

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊥

Tactic:
WithBot.coe_ne_bot

Premises used: WithBot.coe_ne_bot
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊥

Tactic:
exact WithBot.coe_ne_bot

Premises used: WithBot.coe_ne_bot
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
right : ¬Ideal.height (IsLocalRing.maximalIdeal R) = ⊤
⊢ (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊤

Tactic:
rw [← WithBot.coe_top, ne_eq, WithBot.coe_inj]

Premises used: ne_eq, WithBot.coe_top, WithBot.coe_inj
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ ¬Ideal.height (IsLocalRing.maximalIdeal R) = ⊤

Tactic:
((IsLocalRing.maximalIdeal R).finiteHeight_iff.mp
      (IsLocalRing.maximalIdeal R).finiteHeight_of_isNoetherianRing).resolve_left
        Ideal.IsPrime.ne_top'

Premises used: IsLocalRing.maximalIdeal, Ideal.finiteHeight_of_isNoetherianRing, Or.resolve_left, Ideal.finiteHeight_iff, Iff.mp, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ ¬Ideal.height (IsLocalRing.maximalIdeal R) = ⊤

Tactic:
exact ((IsLocalRing.maximalIdeal R).finiteHeight_iff.mp
      (IsLocalRing.maximalIdeal R).finiteHeight_of_isNoetherianRing).resolve_left
        Ideal.IsPrime.ne_top'

Premises used: IsLocalRing.maximalIdeal, Ideal.finiteHeight_of_isNoetherianRing, Or.resolve_left, Ideal.finiteHeight_iff, Iff.mp, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
obtain :
  ∀ (J : Ideal R) (hJ₁ : J ≤ I) (hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1}))
    (hJ₃ : (↑I.height.toNat : ℕ∞) ≤ J.height),
    ∃ J ≤ I, Submodule.spanRank J = (↑I.height : Cardinal.{u_1}) ∧ J.height = I.height
⊢ ∃ J ≤ I, Submodule.spanRank J = (↑I.height : Cardinal.{u_1}) ∧ J.height = I.height

Tactic:
obtain ⟨J, hJ₁, hJ₂, hJ₃⟩ := exists_spanRank_le_and_le_height_of_le_height I _
    (ENat.coe_toNat_le_self I.height)

Premises used: exists_spanRank_le_and_le_height_of_le_height, ENat.coe_toNat_le_self, Ideal.height
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : (↑I.height.toNat : ℕ∞) ≤ J.height
⊢ I.height ≤ J.height

Tactic:
rw [ENat.coe_toNat_eq_self.mpr (Ideal.height_ne_top hI)] at hJ₃

Premises used: Iff.mpr, ENat.coe_toNat_eq_self, Ideal.height_ne_top
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
⊢ ∃ J ≤ I, Submodule.spanRank J = (↑I.height : Cardinal.{u_1}) ∧ J.height = I.height

Tactic:
⟨J, hJ₁, le_antisymm ?_ (le_trans ?_ (J.height_le_spanRank ?_)),
    le_antisymm (Ideal.height_mono hJ₁) hJ₃⟩

Premises used: Ideal.height_le_spanRank, Ideal.height_mono, le_antisymm, And.intro, Exists.intro, le_trans
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
refine_1 : Submodule.spanRank J ≤ (↑I.height : Cardinal.{u_1})
refine_2 : (↑I.height : Cardinal.{u_1}) ≤ (↑J.height : Cardinal.{u_1})
refine_3 : J ≠ ⊤
⊢ ∃ J ≤ I, Submodule.spanRank J = (↑I.height : Cardinal.{u_1}) ∧ J.height = I.height

Tactic:
refine ⟨J, hJ₁, le_antisymm ?_ (le_trans ?_ (J.height_le_spanRank ?_)),
    le_antisymm (Ideal.height_mono hJ₁) hJ₃⟩