awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this_2 : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
this : Membership.mem (γ := Submodule R R) (comap f r) x
⊢ LE.le (α := Ideal R) (span (insert x t)) (comap f r)
have refine_1 : x ∈ (↑(comap f r) : Set R) ∧ t ⊆ (↑(comap f r) : Set R)
Tactic: rw [span_le, Set.insert_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
| p
have rw : comap f (map f p)
Tactic: rw [← sup_eq_left.mpr hI'p, ← (span t).mk_ker, RingHom.ker_eq_comap_bot,
      ← comap_map_of_surjective f hf p]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this_1 : p.IsPrime
this : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
r : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))
h : (fun (q : Ideal (HasQuotient.Quotient R (B := Ideal R) (span t))) ↦ q.IsPrime ∧ map (R := R) f (span {x}) ≤ q) r
hrp : r ≤ map f p
hr : r.IsPrime
hxr : map (R := R) f (span {x}) ≤ r
⊢ comap f r ≤ p
have refine_2 : LE.le (α := Ideal R) (comap f r) (comap f (map f p))
Tactic: conv_rhs => rw [← sup_eq_left.mpr hI'p, ← (span t).mk_ker, RingHom.ker_eq_comap_bot,
      ← comap_map_of_surjective f hf p]
-- 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 : ∀ (i : { s : Finset R // Submodule.span R (↑s : Set R) = I }), p.height ≤ (↑(↑i : Finset R).card : ℕ∞)
Tactic: rw [I.spanRank_toENat_eq_iInf_finset_card, le_iInf_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
n : ℕ
H :
  ∀ m < n,
    ∀ {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 : ℕ∞)
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
hn : s.card = n
⊢ p.height ≤ (↑n : ℕ∞)
have hn₁ : s.card ≤ n
Tactic: replace hn : s.card ≤ n := hn.le
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
n : ℕ
H :
  ∀ m < n,
    ∀ {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 : ℕ∞)
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
hn : s.card ≤ n
⊢ p.height ≤ (↑n : ℕ∞)
have this : p.IsPrime
Tactic: have := hp.isPrime
-- 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
this : p.IsPrime
H :
  ∀ m < 0,
    ∀ {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 ≤ 0
⊢ p.height ≤ (↑0 : ℕ∞)
have h : Membership.mem (γ := Set (Ideal R)) {p : Ideal R | IsMinimalPrime p} p
Tactic: rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_zero_iff, minimalPrimes]
-- 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
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
⊢ p.height ≤ (↑(n + 1) : ℕ∞)
have h : ∀
  (this :
    ∀ {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) (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), p.height ≤ (↑(n + 1) : ℕ∞))
  (hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞)
Tactic: wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal 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
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
h :
  ∀
    (this :
      ∀ {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) (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), p.height ≤ (↑(n + 1) : ℕ∞))
    (hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R), p.height ≤ (↑(n + 1) : ℕ∞)
⊢ p.height ≤ (↑(n + 1) : ℕ∞)
have wlog : ∀ {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) (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), p.height ≤ (↑(n + 1) : ℕ∞)
Tactic: wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R
Cleared hypotheses: R, inst, inst_1, p, s, hp, this, n, H, hn
-- 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
this_1 : 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
this :
  ∀ {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) (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), p.height ≤ (↑(n + 1) : ℕ∞)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ p.height ≤ (↑(n + 1) : ℕ∞)
have h : ∀
  (hp :
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R)))
      (under R (B := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl))))
  (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)
  (this :
    ∀ {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) (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), p.height ≤ (↑(n + 1) : ℕ∞))
  (hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R),
  height (under R (B := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl))) ≤
    (↑(n + 1) : ℕ∞)
Tactic: rw [← Localization.AtPrime.under_maximalIdeal (I := p)] at hp ⊢
Cleared hypotheses: hp, n, H, hn, this, hR
-- 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
this_1 : p.IsPrime
hp :
  Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R)))
    (under R (B := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)))
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
this :
  ∀ {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) (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), p.height ≤ (↑(n + 1) : ℕ∞)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ height (under R (B := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl))) ≤
    (↑(n + 1) : ℕ∞)
have h : height.{u_1} (R := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)) ≤
  (↑(n + 1) : ℕ∞)
Tactic: rw [IsLocalization.height_under p.primeCompl]
-- 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
this_1 : p.IsPrime
hp :
  Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R)))
    (under R (B := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)))
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
this :
  ∀ {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) (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), p.height ≤ (↑(n + 1) : ℕ∞)
hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R
⊢ height.{u_1} (R := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)) ≤
    (↑(n + 1) : ℕ∞)
have h : ∀
  (hp :
    Membership.mem (γ := Set (Ideal (Localization (M := R) p.primeCompl)))
      (Ideal.minimalPrimes
        (span
          ((⇑(algebraMap R (Localization (M := R) p.primeCompl)) : (a : R) → Localization p.primeCompl) ''
            (↑s : Set R))))
      (maximalIdeal (Localization (M := R) p.primeCompl)))
  (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)
  (this :
    ∀ {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) (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), p.height ≤ (↑(n + 1) : ℕ∞))
  (hR : ¬∃ (x : IsLocalRing R), p = maximalIdeal R),
  height.{u_1} (R := Localization (M := R) p.primeCompl) (maximalIdeal (Localization (M := R) p.primeCompl)) ≤
    (↑(n + 1) : ℕ∞)
Tactic: rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp
Cleared hypotheses: hp, n, H, hn, this, hR
-- 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
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
⊢ p.height ≤ (↑(n + 1) : ℕ∞)
have 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) : ℕ∞)
Tactic: obtain ⟨_, rfl⟩ := hR
Cleared hypotheses: p, hp, this, hR
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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)
⊢ height (maximalIdeal R) ≤ (↑(n + 1) : ℕ∞)
have simp_rw : ∀ (q : Ideal R),
  q.IsPrime → q < maximalIdeal R → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R) → q.height ≤ (↑n : ℕ∞)
Tactic: simp_rw [height_le_iff_covBy, ENat.coe_add, ENat.coe_one, ENat.lt_coe_add_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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)
have rw : ¬span (↑s : Set R) ≤ q
Tactic: rw [← span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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
⊢ ∃ (x : R) (s' : Finset R), x ∉ s' ∧ s = insert x s' ∧ x ∉ q
have this₁ : ¬(↑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)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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) (s' : Finset R), x ∉ s' ∧ s = insert x s' ∧ x ∉ q
have 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
Tactic: obtain ⟨x, hxt, hxq⟩ := Set.not_subset.mp this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
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
⊢ q.height ≤ (↑n : ℕ∞)
have 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 : ℕ∞)
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⟩
Cleared hypotheses: s, hn, hp
-- 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 : 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)
⊢ q.height ≤ (↑n : ℕ∞)
have this₁ : 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)
-- 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
⊢ (↑s' : Set R) ⊆ (↑(q ⊔ span {x}).radical : Set R)
have this₁ : span (↑(insert x s') : Set R) ≤ (q ⊔ span {x}).radical
Tactic: have := hp.le.trans this