awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
⊢ ¬(↑I : Set R) ⊆ ⋃ K ∈ hS.toFinset (s := S), (↑K : Set R)

Tactic:
have : ¬(I : Set R) ⊆ ⋃ K ∈ hS.toFinset, (K : Set R) := by
      refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_
      · rintro K hK - -
        rw [Set.Finite.mem_toFinset] at hK
        exact hK.1.isPrime
      · push Not
        intro K hK e
        have := hr.trans (Ideal.height_mono e)
        rw [Set.Finite.mem_toFinset] at hK
        rw [hK.2, ← not_lt] at this
        norm_cast at this
        exact this r.lt_succ_self
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
this : ¬(↑I : Set R) ⊆ ⋃ K ∈ hS.toFinset (s := S), (↑K : Set R)
⊢ ∃ a ∈ (↑I : Set R), ∀ (x : Ideal R) (x_1 : x ∈ S), a ∉ (↑x : Set R)

Tactic:
simp_rw [Set.not_subset, Set.mem_iUnion, not_exists, Set.Finite.mem_toFinset] at this

Premises used: Set.Finite.mem_toFinset, Set.mem_iUnion, not_exists, Set.not_subset
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
this : ∃ a ∈ (↑I : Set R), ∀ (x : Ideal R) (x_1 : x ∈ S), a ∉ (↑x : Set R)
succ :
  ∀ (x : R) (hx₁ : x ∈ (↑I : Set R)) (hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)),
    ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := this
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height

Tactic:
⟨J ⊔ Ideal.span {x}, sup_le h₁ ?_, ?_, ?_⟩

Premises used: Max.max, And.intro, Exists.intro, sup_le, Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
succ : span {x} ≤ I
succ₁ : Submodule.spanRank (J ⊔ span {x}) ≤ (↑(r + 1) : Cardinal.{u_1})
succ₂ : (↑(r + 1) : ℕ∞) ≤ (J ⊔ span {x}).height
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height

Tactic:
refine ⟨J ⊔ Ideal.span {x}, sup_le h₁ ?_, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
succ : {x} ⊆ (↑I : Set R)
succ₁ succ₂ succ₃ succ₄ : x ∈ (↑I : Set R)
⊢ span {x} ≤ I

Tactic:
rwa [Ideal.span_le, Set.singleton_subset_iff]

Premises used: Ideal.span_le, Set.singleton_subset_iff
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
succ : Submodule.spanRank J + Submodule.spanRank (R := R) (span {x}) ≤ (↑(r + 1) : Cardinal.{u_1})
⊢ Submodule.spanRank (J ⊔ span {x}) ≤ (↑(r + 1) : Cardinal.{u_1})

Tactic:
apply Submodule.spanRank_sup_le_sum_spanRank.trans

Premises used: Submodule.spanRank_sup_le_sum_spanRank, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
succ :
  Submodule.spanRank J + Submodule.spanRank (R := R) (span {x}) ≤
    HAdd.hAdd (α := Cardinal.{u_1}) (↑r : Cardinal.{u_1}) 1
⊢ Submodule.spanRank J + Submodule.spanRank (R := R) (span {x}) ≤ (↑(r + 1) : Cardinal.{u_1})

Tactic:
push_cast
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
⊢ Cardinal.mk (↑{x} : Type u_1) ≤ 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
⊢ Submodule.spanRank J + Submodule.spanRank (R := R) (span {x}) ≤
    HAdd.hAdd (α := Cardinal.{u_1}) (↑r : Cardinal.{u_1}) 1

Tactic:
exact add_le_add h₂ ((Submodule.spanRank_span_le_card _).trans (by simp))

Premises used: add_le_add, Submodule.spanRank_span_le_card, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
⊢ (↑(r + 1) : ℕ∞) ≤ (J ⊔ span {x}).height

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

Premises used: le_iInf₂, Ideal.height
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
succ : ∀ (p : Ideal R) (hp : p ∈ (J ⊔ span {x}).minimalPrimes), (↑(r + 1) : ℕ∞) ≤ p.primeHeight
⊢ (↑(r + 1) : ℕ∞) ≤ (J ⊔ span {x}).height

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

Premises used: le_iInf₂
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
⊢ p.IsPrime

Tactic:
have := hp.isPrime
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
succ : (↑(r + 1) : ℕ∞) ≤ p.height
⊢ (↑(r + 1) : ℕ∞) ≤ p.primeHeight

Tactic:
rw [← p.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 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
pos : ∀ (h : p.height = ⊤), (↑(r + 1) : ℕ∞) ≤ p.height
neg : ∀ (h : ¬p.height = ⊤), (↑(r + 1) : ℕ∞) ≤ p.height
⊢ (↑(r + 1) : ℕ∞) ≤ p.height

Tactic:
by_cases h : p.height = ⊤

Premises used: Ideal.height
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
h : p.height = ⊤
⊢ (↑(r + 1) : ℕ∞) ≤ p.height

Tactic:
le_of_le_of_eq le_top h.symm

Premises used: le_of_le_of_eq, le_top, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
h : p.height = ⊤
⊢ (↑(r + 1) : ℕ∞) ≤ p.height

Tactic:
exact le_of_le_of_eq le_top h.symm

Premises used: le_of_le_of_eq, le_top, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this : p.IsPrime
h : ¬p.height = ⊤
⊢ p.FiniteHeight

Tactic:
have : p.FiniteHeight := ⟨Or.inr h⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h : ¬p.height = ⊤
this : p.FiniteHeight
⊢ J.height ≤ p.height

Tactic:
have := Ideal.height_mono (le_sup_left.trans hp.le)
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h_1 : ¬p.height = ⊤
this_2 : p.FiniteHeight
this : J.height ≤ p.height
h : (↑r : ℕ∞) ≠ p.height
⊢ (↑(r + 1) : ℕ∞) ≤ p.height

Tactic:
Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)

Premises used: WithTop.map₂, WithTop.some, LE.le.trans, Order.add_one_le_of_lt, lt_of_le_of_ne, Option.map₂
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h_1 : ¬p.height = ⊤
this_2 : p.FiniteHeight
this : J.height ≤ p.height
h : (↑r : ℕ∞) ≠ p.height
⊢ (↑(r + 1) : ℕ∞) ≤ p.height

Tactic:
exact Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)

Premises used: LE.le.trans, Order.add_one_le_of_lt, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h : ¬p.height = ⊤
this_2 : p.FiniteHeight
this : J.height ≤ p.height
neg : (↑r : ℕ∞) ≠ p.height
⊢ (↑(r + 1) : ℕ∞) ≤ p.height

Tactic:
suffices h : (r : ℕ∞) ≠ p.height by
        exact Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h : ¬p.height = ⊤
this_2 : p.FiniteHeight
this : J.height ≤ p.height
e : (↑r : ℕ∞) = p.height
neg : p ∈ S
neg₁ : x ∈ (↑p : Set R)
⊢ False

Tactic:
apply hx₂ p
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h : ¬p.height = ⊤
this_2 : p.FiniteHeight
this : J.height ≤ p.height
e : (↑r : ℕ∞) = p.height
⊢ p ∈ S

Tactic:
⟨mem_minimalPrimes_of_height_eq (le_sup_left.trans hp.le) (e.symm.trans_le h₃),
          e.symm⟩

Premises used: le_sup_left, Ideal.mem_minimalPrimes_of_height_eq, Set.Mem, Ideal.IsMinimalPrime.le, setOf, Eq.trans_le, And.intro, LE.le.trans, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h : ¬p.height = ⊤
this_2 : p.FiniteHeight
this : J.height ≤ p.height
e : (↑r : ℕ∞) = p.height
⊢ p ∈ S

Tactic:
refine ⟨mem_minimalPrimes_of_height_eq (le_sup_left.trans hp.le) (e.symm.trans_le h₃),
          e.symm⟩
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height
hr : (↑(r + 1) : ℕ∞) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})
h₃ : (↑r : ℕ∞) ≤ J.height
S : Set (Ideal R) := {K : Ideal R | K ∈ J.minimalPrimes ∧ K.height = (↑r : ℕ∞)}
hS : S.Finite
x : R
hx₁ : x ∈ (↑I : Set R)
hx₂ : ∀ (x_1 : Ideal R) (x_2 : x_1 ∈ S), x ∉ (↑x_1 : Set R)
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this_1 : p.IsPrime
h : ¬p.height = ⊤
this_2 : p.FiniteHeight
this : J.height ≤ p.height
e : (↑r : ℕ∞) = p.height
⊢ x ∈ (↑p : Set R)

Tactic:
apply hp.le <| Ideal.mem_sup_right <| mem_span_singleton_self x

Premises used: Ideal.IsMinimalPrime.le, Ideal.mem_sup_right, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
r : ℕ
hr : (↑r : ℕ∞) ≤ I.height
zero : ∀ (hr : (↑0 : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑0 : Cardinal.{u_1}) ∧ (↑0 : ℕ∞) ≤ J.height
succ :
  ∀ (r : ℕ)
    (ih : ∀ (hr : (↑r : ℕ∞) ≤ I.height), ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height)
    (hr : (↑(r + 1) : ℕ∞) ≤ I.height),
    ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑r : Cardinal.{u_1}) ∧ (↑r : ℕ∞) ≤ J.height

Tactic:
induction r with
  | zero => simp
  | succ r ih =>
    obtain ⟨J, h₁, h₂, h₃⟩ := ih ((WithTop.coe_le_coe.mpr r.le_succ).trans hr)
    let S := { K | K ∈ J.minimalPrimes ∧ Ideal.height K = r }
    have hS : Set.Finite S := Set.Finite.subset J.finite_minimalPrimes_of_isNoetherianRing
      (fun _ h => h.1)
    have : ¬(I : Set R) ⊆ ⋃ K ∈ hS.toFinset, (K : Set R) := by
      refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_
      · rintro K hK - -
        rw [Set.Finite.mem_toFinset] at hK
        exact hK.1.isPrime
      · push Not
        intro K hK e
        have := hr.trans (Ideal.height_mono e)
        rw [Set.Finite.mem_toFinset] at hK
        rw [hK.2, ← not_lt] at this
        norm_cast at this
        exact this r.lt_succ_self
    simp_rw [Set.not_subset, Set.mem_iUnion, not_exists, Set.Finite.mem_toFinset] at this
    obtain ⟨x, hx₁, hx₂⟩ := this
    refine ⟨J ⊔ Ideal.span {x}, sup_le h₁ ?_, ?_, ?_⟩
    · rwa [Ideal.span_le, Set.singleton_subset_iff]
    · apply Submodule.spanRank_sup_le_sum_spanRank.trans
      push_cast
      exact add_le_add h₂ ((Submodule.spanRank_span_le_card _).trans (by simp))
    · refine le_iInf₂ (fun p hp ↦ ?_)
      have := hp.isPrime
      rw [← p.height_eq_primeHeight]
      by_cases h : p.height = ⊤
      · exact le_of_le_of_eq le_top h.symm
      have : p.FiniteHeight := ⟨Or.inr h⟩
      have := Ideal.height_mono (le_sup_left.trans hp.le)
      suffices h : (r : ℕ∞) ≠ p.height by
        exact Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)
      intro e
      apply hx₂ p
      · refine ⟨mem_minimalPrimes_of_height_eq (le_sup_left.trans hp.le) (e.symm.trans_le h₃),
          e.symm⟩
      · apply hp.le <| Ideal.mem_sup_right <| mem_span_singleton_self x

Premises used: Ideal.span_le, Set.singleton_subset_iff, Set.Finite.mem_toFinset, Set.mem_iUnion, not_exists, le_iInf₂, Submodule.spanRank_sup_le_sum_spanRank, Set.not_subset, LE.le.trans, Ideal.mem_sup_right
-- 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
a₁ : ringKrullDim R ≤ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞)
⊢ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) = ringKrullDim R

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
a : ⨆ (i : Ideal R), (↑(⨆ (_ : i ≠ ⊤), i.height) : WithBot ℕ∞) ≤ ringKrullDim R
⊢ (↑(⨆ (I : Ideal R), ⨆ (_ : I ≠ ⊤), I.height) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
rw [WithBot.coe_iSup ⟨⊤, fun _ _ => le_top⟩]

Premises used: WithBot.coe_iSup, le_top, Exists.intro, Top.top
-- Module: Mathlib.RingTheory.Ideal.Height
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
⊢ ⨆ (i : Ideal R), (↑(⨆ (_ : i ≠ ⊤), i.height) : WithBot ℕ∞) ≤ ringKrullDim R

Tactic:
iSup_le fun I => ?_

Premises used: iSup_le