awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
this : p.IsPrime
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 : ℕ∞)
hn : s.card ≤ n + 1
hR : ∃ (x : IsLocalRing R), p = maximalIdeal R
obtain :
  ∀ (w : IsLocalRing R)
    (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) (maximalIdeal R))
    (this : IsPrime (maximalIdeal R)), height (maximalIdeal R) ≤ (↑(n + 1) : ℕ∞)
⊢ p.height ≤ (↑(n + 1) : ℕ∞)

Tactic:
obtain ⟨_, rfl⟩ := hR

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset 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 : ℕ∞)
hn : s.card ≤ n + 1
w : IsLocalRing R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) (maximalIdeal R)
this : IsPrime (maximalIdeal R)
simp_rw :
  ∀ (q : Ideal R),
    q.IsPrime →
      q < maximalIdeal R → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R) → q.height ≤ (↑n : ℕ∞)
⊢ height (maximalIdeal R) ≤ (↑(n + 1) : ℕ∞)

Tactic:
simp_rw [height_le_iff_covBy, ENat.coe_add, ENat.coe_one, ENat.lt_coe_add_one_iff]

Premises used: ENat.coe_one, Ideal.height_le_iff_covBy, ENat.coe_add, ENat.lt_coe_add_one_iff
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset 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 : ℕ∞)
hn : s.card ≤ n + 1
w : IsLocalRing R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) (maximalIdeal R)
this : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
rw : ¬span (↑s : Set R) ≤ q
⊢ ¬(↑s : Set R) ⊆ (↑q : Set R)

Tactic:
rw [← span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset 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 : ℕ∞)
hn : s.card ≤ n + 1
w : IsLocalRing R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) (maximalIdeal R)
this : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
⊢ ¬span (↑s : Set R) ≤ q

Tactic:
fun e ↦ lt_irrefl _ ((hp.2 ⟨hq, e⟩ hpq.le).trans_lt hpq)

Premises used: lt_irrefl, IsLocalRing.maximalIdeal, LT.lt.le, And.right, And.intro, LE.le.trans_lt, Not
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset 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 : ℕ∞)
hn : s.card ≤ n + 1
w : IsLocalRing R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) (maximalIdeal R)
this : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
⊢ ¬span (↑s : Set R) ≤ q

Tactic:
exact fun e ↦ lt_irrefl _ ((hp.2 ⟨hq, e⟩ hpq.le).trans_lt hpq)

Premises used: lt_irrefl, IsLocalRing.maximalIdeal, LT.lt.le, And.right, And.intro, LE.le.trans_lt
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset 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 : ℕ∞)
hn : s.card ≤ n + 1
w : IsLocalRing R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) (maximalIdeal R)
this : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
⊢ ¬(↑s : Set R) ⊆ (↑q : Set R)

Tactic:
have : ¬(s : Set R) ⊆ q := by
          rw [← span_le]
          exact fun e ↦ lt_irrefl _ ((hp.2 ⟨hq, e⟩ hpq.le).trans_lt hpq)
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset 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 : ℕ∞)
hn : s.card ≤ n + 1
w : IsLocalRing R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) (maximalIdeal 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
this : ¬(↑s : Set R) ⊆ (↑q : Set R)
obtain :
  ∀ (x : R) (hxt : x ∈ (↑s : Set R)) (hxq : x ∉ (↑q : Set R)),
    ∃ (x : R) (s' : Finset R), x ∉ s' ∧ s = insert x s' ∧ x ∉ q
⊢ ∃ (x : R) (s' : Finset R), x ∉ s' ∧ s = insert x s' ∧ x ∉ q

Tactic:
obtain ⟨x, hxt, hxq⟩ := Set.not_subset.mp this

Premises used: Set.not_subset, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset 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 : ℕ∞)
hn : s.card ≤ n + 1
w : IsLocalRing R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) (maximalIdeal 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
this : ¬(↑s : Set R) ⊆ (↑q : Set R)
x : R
hxt : x ∈ (↑s : Set R)
hxq : x ∉ (↑q : Set R)
⊢ ∃ (x : R) (s' : Finset R), x ∉ s' ∧ s = insert x s' ∧ x ∉ q

Tactic:
⟨x, _, fun e ↦ (Finset.mem_erase.mp e).1 rfl, (Finset.insert_erase hxt).symm, hxq⟩

Premises used: Finset.mem_erase, And.left, And.intro, Exists.intro, Iff.mp, Eq.symm, Finset.insert_erase, rfl
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset 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 : ℕ∞)
hn : s.card ≤ n + 1
w : IsLocalRing R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) (maximalIdeal 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
this : ¬(↑s : Set R) ⊆ (↑q : Set R)
x : R
hxt : x ∈ (↑s : Set R)
hxq : x ∉ (↑q : Set R)
⊢ ∃ (x : R) (s' : Finset R), x ∉ s' ∧ s = insert x s' ∧ x ∉ q

Tactic:
exact ⟨x, _, fun e ↦ (Finset.mem_erase.mp e).1 rfl, (Finset.insert_erase hxt).symm, hxq⟩
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
s : Finset 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 : ℕ∞)
hn : s.card ≤ n + 1
w : IsLocalRing R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) (maximalIdeal R)
this : IsPrime (maximalIdeal R)
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
obtain :
  ∀ (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)),
    q.height ≤ (↑n : ℕ∞)
⊢ q.height ≤ (↑n : ℕ∞)

Tactic:
obtain ⟨x, s', hxs', rfl, hxq⟩ : ∃ x s', x ∉ s' ∧ s = insert x s' ∧ x ∉ q := by
        have : ¬(s : Set R) ⊆ q := by
          rw [← span_le]
          exact fun e ↦ lt_irrefl _ ((hp.2 ⟨hq, e⟩ hpq.le).trans_lt hpq)
        obtain ⟨x, hxt, hxq⟩ := Set.not_subset.mp this
        exact ⟨x, _, fun e ↦ (Finset.mem_erase.mp e).1 rfl, (Finset.insert_erase hxt).symm, hxq⟩

Premises used: rfl
-- 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 : 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)
⊢ ∀ (b : Ideal R),
    Membership.mem (γ := Set (Ideal R)) {J : Ideal R | q ⊔ span {x} ≤ J ∧ J.IsPrime} b → maximalIdeal R ≤ b

Tactic:
fun J ⟨hJ, hJ'⟩ ↦ by_contra fun h ↦ hq' J hJ' ((SetLike.lt_iff_le_and_exists.mpr
          ⟨le_sup_left, x, mem_sup_right (mem_span_singleton_self _), hxq⟩).trans_le hJ)
          ((le_maximalIdeal hJ'.ne_top).lt_of_not_ge h)

Premises used: Iff.mpr, LE.le.lt_of_not_ge, SetLike.lt_iff_le_and_exists, le_sup_left, IsLocalRing.maximalIdeal, LE.le, LT.lt.trans_le, And.intro, IsLocalRing.le_maximalIdeal, Exists.intro, by_contra, Ideal.IsPrime.ne_top, Ideal.mem_sup_right, Ideal.mem_span_singleton_self, _private.0.Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes.match_2
-- 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 : 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)
⊢ ∀ (b : Ideal R),
    Membership.mem (γ := Set (Ideal R)) {J : Ideal R | q ⊔ span {x} ≤ J ∧ J.IsPrime} b → maximalIdeal R ≤ b

Tactic:
exact fun J ⟨hJ, hJ'⟩ ↦ by_contra fun h ↦ hq' J hJ' ((SetLike.lt_iff_le_and_exists.mpr
          ⟨le_sup_left, x, mem_sup_right (mem_span_singleton_self _), hxq⟩).trans_le hJ)
          ((le_maximalIdeal hJ'.ne_top).lt_of_not_ge h)
-- 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 : 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)
⊢ maximalIdeal R ≤ (q ⊔ span {x}).radical

Tactic:
have : maximalIdeal R ≤ (q ⊔ span {x}).radical := by
        rw [radical_eq_sInf, le_sInf_iff]
        exact fun J ⟨hJ, hJ'⟩ ↦ by_contra fun h ↦ hq' J hJ' ((SetLike.lt_iff_le_and_exists.mpr
          ⟨le_sup_left, x, mem_sup_right (mem_span_singleton_self _), hxq⟩).trans_le hJ)
          ((le_maximalIdeal hJ'.ne_top).lt_of_not_ge h)
-- 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
⊢ span (↑(insert x s') : Set R) ≤ (q ⊔ span {x}).radical

Tactic:
have := hp.le.trans this
-- 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_2 : maximalIdeal R ≤ (q ⊔ span {x}).radical
this : span (↑(insert x s') : Set R) ≤ (q ⊔ span {x}).radical
⊢ x ∈ (↑(q ⊔ span {x}).radical : Set R) ∧ (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)

Tactic:
rw [span_le, Finset.coe_insert, Set.insert_subset_iff] at this

Premises used: Ideal.span_le, Set.insert_subset_iff, 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_2 : maximalIdeal R ≤ (q ⊔ span {x}).radical
this : x ∈ (↑(q ⊔ span {x}).radical : Set R) ∧ (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
⊢ (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)

Tactic:
this.2

Premises used: And.right
-- 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_2 : maximalIdeal R ≤ (q ⊔ span {x}).radical
this : x ∈ (↑(q ⊔ span {x}).radical : Set R) ∧ (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
⊢ (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)

Tactic:
exact this.2

Premises used: And.right
-- 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
⊢ (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)

Tactic:
have h : (s' : Set R) ⊆ (q ⊔ span {x}).radical := by
        have := hp.le.trans this
        rw [span_le, Finset.coe_insert, Set.insert_subset_iff] at this
        exact this.2
-- 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)
obtain :
  ∀ (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)), q.height ≤ (↑n : ℕ∞)
⊢ q.height ≤ (↑n : ℕ∞)

Tactic:
obtain ⟨t, ht, hspan⟩ := exists_subset_radical_span_sup_of_subset_radical_sup _ _ _ h

Premises used: Ideal.exists_subset_radical_span_sup_of_subset_radical_sup
-- 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_1 : 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
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) q
⊢ Finset.card.{u_1} (α := (↑(↑s' : Set R) : Type u_1)) Finset.univ < (insert x s').card

Tactic:
simpa using Finset.card_lt_card (Finset.ssubset_insert hxs')

Premises used: Finset.card_lt_card, Finset.ssubset_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_1 : 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
hq : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) q
tcard norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : t.card ≤ n
⊢ LE.le (α := ℕ∞) (↑t.card : ℕ∞) (↑n : ℕ∞)

Tactic:
norm_cast
-- 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
suffices : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) q
⊢ q.height ≤ (↑n : ℕ∞)

Tactic:
suffices hq : q ∈ (span t).minimalPrimes from
        have tcard : t.card ≤ n := Nat.le_of_lt_succ ((Finset.card_image_le.trans_lt <| by
          simpa using Finset.card_lt_card (Finset.ssubset_insert hxs')).trans_le hn)
        (H _ (tcard.trans_lt n.lt_succ_self) q t hq rfl).trans (by norm_cast)