awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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
⊢ (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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
⊢ q.height ≤ (↑n : ℕ∞)
have h : (↑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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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)
⊢ q.height ≤ (↑n : ℕ∞)
have 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 : ℕ∞)
Tactic: obtain ⟨t, ht, hspan⟩ := exists_subset_radical_span_sup_of_subset_radical_sup _ _ _ h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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
⊢ q.height ≤ (↑n : ℕ∞)
have suffices : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) q
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)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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 (↑t : Set R))) q
have 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
Tactic: rw [Finset.coe_insert] at hp
Cleared hypotheses: hp, this, h, t_1, ht, hspan, t
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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 (↑t : Set R))) q
have h₁ : (↑t : Set R) = Set.range t_1
Tactic: convert! mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert hpq _ _ hp _ ht ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑t : Set R))) q
have convert! : (↑s' : Set R) ⊆ (↑(radical (span (insert x (Set.range t_1)))) : Set R)
Tactic: convert! mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert hpq _ _ hp _ ht ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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)
have refine : LE.le (α := Ideal R) (span (Set.range t_1) ⊔ span {x}) (span (insert x (Set.range t_1)))
Tactic: refine hspan.trans <| radical_mono ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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
⊢ LE.le (α := Ideal R) (span (Set.range t_1) ⊔ span {x}) (span (insert x (Set.range t_1)))
have rw : LE.le (α := Ideal R) (span (Set.range t_1) ⊔ span {x}) (span (Set.range t_1 ∪ {x}))
Tactic: rw [← Set.union_singleton, span_union]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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}))
⊢ LE.le (α := Ideal R) (span (Set.range t_1) ⊔ span {x}) (span (insert x (Set.range t_1)))
have rw₁ : LE.le (α := Ideal R) (span (Set.range t_1) ⊔ span {x}) (span (Set.range t_1) ⊔ span {x})
Tactic: rw [← Set.union_singleton, span_union]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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
⊢ p.height ≤
    (↑(↑(Subtype.mk (p := fun (s_1 : Finset R) ↦
                Eq (α := Submodule R R) (Submodule.span R (↑s_1 : Set R)) (span (↑s : Set R))) s ⋯) :
            Finset R).card :
      ℕ∞)
have induction : ∀ (x : ℕ) (hn : s.card = x), p.height ≤ (↑x : ℕ∞)
Tactic: induction hn : s.card using Nat.strong_induction_on generalizing R with
  | h n H =>
    replace hn : s.card ≤ n := hn.le
    have := hp.isPrime
    cases n with
    | zero =>
      rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_zero_iff, minimalPrimes]
      simp_all
    | succ n =>
      wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R
      · rw [← Localization.AtPrime.under_maximalIdeal (I := p)] at hp ⊢
        rw [IsLocalization.height_under p.primeCompl]
        rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp
        exact this _ (s.image (algebraMap R (Localization p.primeCompl))) (by simpa using hp)
          inferInstance _ H (Finset.card_image_le.trans hn) ⟨inferInstance, rfl⟩
      obtain ⟨_, rfl⟩ := hR
      simp_rw [height_le_iff_covBy, ENat.coe_add, ENat.coe_one, ENat.lt_coe_add_one_iff]
      intro q hq hpq hq'
      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⟩
      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)
      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
      obtain ⟨t, ht, hspan⟩ := exists_subset_radical_span_sup_of_subset_radical_sup _ _ _ h
      let t := Finset.univ.image t
      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)
      rw [Finset.coe_insert] at hp
      convert! mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert hpq _ _ hp _ ht ?_
      · simp [t]
      refine hspan.trans <| radical_mono ?_
      rw [← Set.union_singleton, span_union]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)
have rw : p.height ≤ ⨅ (s : { s : Finset R // Submodule.span R (↑s : Set R) = I }), (↑(↑s : Finset R).card : ℕ∞)
Tactic: classical
  rw [I.spanRank_toENat_eq_iInf_finset_card, le_iInf_iff]
  rintro ⟨s, (rfl : span s = I)⟩
  induction hn : s.card using Nat.strong_induction_on generalizing R with
  | h n H =>
    replace hn : s.card ≤ n := hn.le
    have := hp.isPrime
    cases n with
    | zero =>
      rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_zero_iff, minimalPrimes]
      simp_all
    | succ n =>
      wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R
      · rw [← Localization.AtPrime.under_maximalIdeal (I := p)] at hp ⊢
        rw [IsLocalization.height_under p.primeCompl]
        rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp
        exact this _ (s.image (algebraMap R (Localization p.primeCompl))) (by simpa using hp)
          inferInstance _ H (Finset.card_image_le.trans hn) ⟨inferInstance, rfl⟩
      obtain ⟨_, rfl⟩ := hR
      simp_rw [height_le_iff_covBy, ENat.coe_add, ENat.coe_one, ENat.lt_coe_add_one_iff]
      intro q hq hpq hq'
      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⟩
      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)
      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
      obtain ⟨t, ht, hspan⟩ := exists_subset_radical_span_sup_of_subset_radical_sup _ _ _ h
      let t := Finset.univ.image t
      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)
      rw [Finset.coe_insert] at hp
      convert! mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert hpq _ _ hp _ ht ?_
      · simp [t]
      refine hspan.trans <| radical_mono ?_
      rw [← Set.union_singleton, span_union]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
hp : p ∈ I.minimalPrimes
rw : p.height ≤ ⨅ (s : { s : Finset R // Submodule.span R (↑s : Set R) = I }), (↑(↑s : Finset R).card : ℕ∞)
⊢ p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)
have rw₁ : ∀ (i : { s : Finset R // Submodule.span R (↑s : Set R) = I }), p.height ≤ (↑(↑i : Finset R).card : ℕ∞)
Tactic: classical
  rw [I.spanRank_toENat_eq_iInf_finset_card, le_iInf_iff]
  rintro ⟨s, (rfl : span s = I)⟩
  induction hn : s.card using Nat.strong_induction_on generalizing R with
  | h n H =>
    replace hn : s.card ≤ n := hn.le
    have := hp.isPrime
    cases n with
    | zero =>
      rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_zero_iff, minimalPrimes]
      simp_all
    | succ n =>
      wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R
      · rw [← Localization.AtPrime.under_maximalIdeal (I := p)] at hp ⊢
        rw [IsLocalization.height_under p.primeCompl]
        rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp
        exact this _ (s.image (algebraMap R (Localization p.primeCompl))) (by simpa using hp)
          inferInstance _ H (Finset.card_image_le.trans hn) ⟨inferInstance, rfl⟩
      obtain ⟨_, rfl⟩ := hR
      simp_rw [height_le_iff_covBy, ENat.coe_add, ENat.coe_one, ENat.lt_coe_add_one_iff]
      intro q hq hpq hq'
      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⟩
      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)
      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
      obtain ⟨t, ht, hspan⟩ := exists_subset_radical_span_sup_of_subset_radical_sup _ _ _ h
      let t := Finset.univ.image t
      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)
      rw [Finset.coe_insert] at hp
      convert! mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert hpq _ _ hp _ ht ?_
      · simp [t]
      refine hspan.trans <| radical_mono ?_
      rw [← Set.union_singleton, span_union]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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 ≤ (↑s.card : ℕ∞)
have trans : p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank (span (↑s : Set R)))
Tactic: trans (Cardinal.toENat (Submodule.spanRank (Ideal.span (s : Set R))))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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)))
⊢ p.height ≤ (↑s.card : ℕ∞)
have trans₁ : LE.le (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank (span (↑s : Set R))) : ℕ∞)
  ((↑s.card : ℕ∞) : ℕ∞)
Tactic: trans (Cardinal.toENat (Submodule.spanRank (Ideal.span (s : Set R))))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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 ≤ (↑s.ncard : ℕ∞)
have rw : p.height ≤ (↑hs.toFinset (s := s).card : ℕ∞)
Tactic: rw [s.ncard_eq_toFinset_card hs]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ I.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)
have obtain : ∀ (J : Ideal R) (hJ : J ∈ I.minimalPrimes),
  I.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)
Tactic: obtain ⟨J, hJ⟩ := nonempty_minimalPrimes hI