awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
⊢ (∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n) ↔
    ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n
have refine_1 : ∀ (h : ∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n) (p : Ideal R) (hp : p.IsPrime),
  (↑p.height : WithBot ℕ∞) ≤ n
Tactic: refine ⟨fun h p hp ↦ ?_, fun h p ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
refine_1 :
  ∀ (h : ∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n) (p : Ideal R) (hp : p.IsPrime),
    (↑p.height : WithBot ℕ∞) ≤ n
⊢ (∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n) ↔
    ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n
have refine_2 : ∀ (h : ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n) (p : PrimeSpectrum R),
  (↑(Order.height p) : WithBot ℕ∞) ≤ n
Tactic: refine ⟨fun h p hp ↦ ?_, fun h p ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ (i : PrimeSpectrum R), (↑(Order.height i) : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
⊢ (↑p.height : WithBot ℕ∞) ≤ n
have refine_1 : (↑p.primeHeight : WithBot ℕ∞) ≤ n
Tactic: rw [Ideal.height_eq_primeHeight]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n
p : PrimeSpectrum R
⊢ (↑(Order.height p) : WithBot ℕ∞) ≤ n
have h₁ : (↑p.asIdeal.height : WithBot ℕ∞) ≤ n
Tactic: specialize h p.2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
p : PrimeSpectrum R
h : (↑p.asIdeal.height : WithBot ℕ∞) ≤ n
⊢ (↑(Order.height p) : WithBot ℕ∞) ≤ n
have refine_2 : ∀ (h : (↑p.asIdeal.primeHeight : WithBot ℕ∞) ≤ n), (↑(Order.height p) : WithBot ℕ∞) ≤ n
Tactic: rwa [Ideal.height_eq_primeHeight] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
⊢ ringKrullDim R ≤ n ↔ ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
have rw : (∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n) ↔
  ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
Tactic: rw [ringKrullDim_le_iff_height_le]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
⊢ (∀ ⦃p : Ideal R⦄, p.IsPrime → (↑p.height : WithBot ℕ∞) ≤ n) ↔
    ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
have refine : ∀ (h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n) (p : Ideal R) (hp : p.IsPrime),
  (↑p.height : WithBot ℕ∞) ≤ n
Tactic: refine ⟨fun h m hm ↦ h hm.isPrime, fun h p hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
⊢ (↑p.height : WithBot ℕ∞) ≤ n
have obtain : ∀ (m : Ideal R) (hm : m.IsMaximal) (hle : p ≤ m), (↑p.height : WithBot ℕ∞) ≤ n
Tactic: obtain ⟨m, hm, hle⟩ := p.exists_le_maximal hp.ne_top
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
m : Ideal R
hm : m.IsMaximal
hle : p ≤ m
⊢ (↑p.height : WithBot ℕ∞) ≤ n
have refine : (↑p.height : WithBot ℕ∞) ≤ (↑m.height : WithBot ℕ∞)
Tactic: refine le_trans ?_ (h hm)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_2
inst : CommRing R
n : WithBot ℕ∞
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → (↑m.height : WithBot ℕ∞) ≤ n
p : Ideal R
hp : p.IsPrime
m : Ideal R
hm : m.IsMaximal
hle : p ≤ m
⊢ (↑p.height : WithBot ℕ∞) ≤ (↑m.height : WithBot ℕ∞)
have norm_cast : p.height ≤ m.height
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
inst_4 : J.IsPrime
⊢ height (comap (F := R →+* A) (algebraMap R A) J) = J.height
have rw : Order.krullDim.{u_2} (↑(Set.Iic { asIdeal := J, isPrime := inst_4 : PrimeSpectrum A }) : Type u_2) =
  Order.krullDim.{u_1} (↑(Set.Iic { asIdeal := comap (F := R →+* A) (algebraMap R A) J, isPrime := sorry }) : Type u_1)
Tactic: rw [eq_comm, Ideal.height_eq_primeHeight, Ideal.height_eq_primeHeight, Ideal.primeHeight,
    Ideal.primeHeight, ← WithBot.coe_inj, Order.height_eq_krullDim_Iic,
    Order.height_eq_krullDim_Iic]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
inst_4 : J.IsPrime
e : OrderIso.{u_2, u_1} { p : Ideal A // p.IsPrime }
  { p : Ideal R // p.IsPrime ∧ Disjoint (↑S : Set R) (↑p : Set R) } :=
  orderIsoOfPrime S A
⊢ Order.krullDim.{u_2} (↑(Set.Iic { asIdeal := J, isPrime := inst_4 : PrimeSpectrum A }) : Type u_2) =
    Order.krullDim.{u_1} (↑(Set.Iic { asIdeal := comap (F := R →+* A) (algebraMap R A) J, isPrime := ⋯ }) : Type u_1)
have H : ∀ (p : Ideal R) (hp : p ≤ comap (F := R →+* A) (algebraMap R A) J), Disjoint (↑S : Set R) (↑p : Set R)
Tactic: have H (p : Ideal R) (hp : p ≤ J.comap (algebraMap R A)) : Disjoint (S : Set R) p :=
    Set.disjoint_of_subset_right hp (e ⟨_, ‹J.IsPrime›⟩).2.2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
⊢ height (under R J) = J.height
have rw : Eq (α := ℕ∞)
  (⨅ (J_1 : Ideal R),
    ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap (F := R →+* A) (algebraMap R A) J)) J_1),
      J_1.height)
  (⨅ J_1 ∈ J.minimalPrimes, J_1.height)
Tactic: rw [(J.comap _).height_eq_inf_minimalPrimes, J.height_eq_inf_minimalPrimes]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
⊢ Eq (α := ℕ∞)
    (⨅ (J_1 : Ideal R),
      ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap (F := R →+* A) (algebraMap R A) J)) J_1),
        J_1.height)
    (⨅ J_1 ∈ J.minimalPrimes, J_1.height)
have simp : Eq (α := ℕ∞) (⨅ b ∈ J.minimalPrimes, height (comap (F := R →+* A) (algebraMap R A) b))
  (⨅ J_1 ∈ J.minimalPrimes, J_1.height)
Tactic: simp only [IsLocalization.minimalPrimes_comap S A, iInf_image]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
⊢ Eq (α := ℕ∞) (⨅ b ∈ J.minimalPrimes, height (comap (F := R →+* A) (algebraMap R A) b))
    (⨅ J_1 ∈ J.minimalPrimes, J_1.height)
have apply : ∀ (p : Ideal A) (hp : p ∈ J.minimalPrimes), height (comap (F := R →+* A) (algebraMap R A) p) = p.height
Tactic: apply iInf_congr (fun p ↦ iInf_congr fun hp ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Submonoid R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J p : Ideal A
hp : p ∈ J.minimalPrimes
⊢ height (comap (F := R →+* A) (algebraMap R A) p) = p.height
have this : p.IsPrime
Tactic: have := hp.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
A : Type u_2
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : IsLocalization.AtPrime A I
⊢ ringKrullDim A = (↑I.height : WithBot ℕ∞)
have this : IsLocalRing A
Tactic: have := IsLocalization.AtPrime.isLocalRing A I
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
A : Type u_2
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : IsLocalization.AtPrime A I
this : IsLocalRing A
⊢ ringKrullDim A = (↑I.height : WithBot ℕ∞)
have rw : (↑(height (IsLocalRing.maximalIdeal A)) : WithBot ℕ∞) = (↑I.height : WithBot ℕ∞)
Tactic: rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim,
      ← IsLocalization.height_under I.primeCompl,
      ← IsLocalization.AtPrime.under_maximalIdeal A I]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
A : Type u_2
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : IsLocalization.AtPrime A I
this : IsLocalRing A
rw : (↑(height (IsLocalRing.maximalIdeal A)) : WithBot ℕ∞) = (↑I.height : WithBot ℕ∞)
⊢ ringKrullDim A = (↑I.height : WithBot ℕ∞)
have rw₁ : (↑(height (under R (IsLocalRing.maximalIdeal A))) : WithBot ℕ∞) = (↑I.height : WithBot ℕ∞)
Tactic: rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim,
      ← IsLocalization.height_under I.primeCompl,
      ← IsLocalization.AtPrime.under_maximalIdeal A I]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.IsPrime
A : Type u_2
inst_2 : CommRing A
inst_3 : Algebra R A
inst_4 : IsLocalization.AtPrime A I
this : IsLocalRing A
rw : (↑(height (IsLocalRing.maximalIdeal A)) : WithBot ℕ∞) = (↑I.height : WithBot ℕ∞)
rw₁ : (↑(height (under R (IsLocalRing.maximalIdeal A))) : WithBot ℕ∞) = (↑I.height : WithBot ℕ∞)
⊢ ringKrullDim A = (↑I.height : WithBot ℕ∞)
have rw₂ : (↑(height (under R (IsLocalRing.maximalIdeal A))) : WithBot ℕ∞) =
  (↑(height (under R (IsLocalRing.maximalIdeal A))) : WithBot ℕ∞)
Tactic: rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim,
      ← IsLocalization.height_under I.primeCompl,
      ← IsLocalization.AtPrime.under_maximalIdeal A I]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
⊢ height.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p) = p.height
have this : P.IsPrime
Tactic: have : P.IsPrime := isPrime_of_isPrime_disjoint M S p ‹_› h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
this : P.IsPrime
⊢ height.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p) = p.height
have this₁ : IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime P) (comap (F := R →+* S) (algebraMap R S) P)
Tactic: have := isLocalization_isLocalization_atPrime_isLocalization (M := M) (Localization.AtPrime P) P
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
this_1 : P.IsPrime
this : IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime P) (comap (F := R →+* S) (algebraMap R S) P)
⊢ height.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p) = p.height
have this₁ : IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) p
Tactic: simp_rw [P, under_map_of_isPrime_disjoint M S _ h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
this_1 : P.IsPrime
this : IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) p
⊢ height.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p) = p.height
have this₁ : ringKrullDim.{u_2} (Localization.AtPrime P) = ringKrullDim.{u_1} (Localization.AtPrime p)
Tactic: have := ringKrullDim_eq_of_ringEquiv (IsLocalization.algEquiv p.primeCompl
    (Localization.AtPrime P) (Localization.AtPrime p)).toRingEquiv
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
p : Ideal R
inst_4 : p.IsPrime
h : Disjoint (↑M : Set R) (↑p : Set R)
P : Ideal S := Ideal.map (F := R →+* S) (algebraMap R S) p
this_1 : P.IsPrime
this_2 :
  IsLocalization.AtPrime.{u_1, u_2} (Localization.AtPrime (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) p
this : ringKrullDim.{u_2} (Localization.AtPrime P) = ringKrullDim.{u_1} (Localization.AtPrime p)
⊢ height.{u_2} (R := S) (Ideal.map (F := R →+* S) (algebraMap R S) p) = p.height
have this₁ : (↑P.height : WithBot ℕ∞) = (↑p.height : WithBot ℕ∞)
Tactic: rw [AtPrime.ringKrullDim_eq_height P, AtPrime.ringKrullDim_eq_height p] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
e' : J.primeHeight = I.height
inst_2 : J.FiniteHeight
⊢ J ∈ I.minimalPrimes
have e'₁ : J.height = I.height
Tactic: rw [← J.height_eq_primeHeight] at e'
Cleared hypotheses: e', inst_2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
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 ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
have succ : ∀ (J : Ideal R) (h₁ : J ≤ I) (h₂ : Submodule.spanRank J ≤ (↑r : Cardinal.{u_1})) (h₃ : (↑r : ℕ∞) ≤ J.height),
  ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
Tactic: obtain ⟨J, h₁, h₂, h₃⟩ := ih ((WithTop.coe_le_coe.mpr r.le_succ).trans hr)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
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 : ℕ∞)}
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
have hS : S.Finite
Tactic: have hS : Set.Finite S := Set.Finite.subset J.finite_minimalPrimes_of_isNoetherianRing
      (fun _ h => h.1)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
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)
have refine_1 : ∀ i ∈ hS.toFinset (s := S), i ≠ ⊥ → i ≠ ⊥ → i.IsPrime
Tactic: refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
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
refine_1 : ∀ i ∈ hS.toFinset (s := S), i ≠ ⊥ → i ≠ ⊥ → i.IsPrime
⊢ ¬(↑I : Set R) ⊆ ⋃ K ∈ hS.toFinset (s := S), (↑K : Set R)
have refine_2 : ¬∃ i ∈ hS.toFinset (s := S), I ≤ i
Tactic: refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
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
K : Ideal R
hK : K ∈ hS.toFinset (s := S)
⊢ K.IsPrime
have hK₁ : K ∈ S
Tactic: rw [Set.Finite.mem_toFinset] at hK
Cleared hypotheses: hK
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
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 ∈ hS.toFinset (s := S), I ≤ i
have refine_2 : ∀ (i : Ideal R) (_ : i ∈ hS.toFinset (s := S)), ¬I ≤ i
Tactic: push Not
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
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
K : Ideal R
hK : K ∈ hS.toFinset (s := S)
e : I ≤ K
⊢ False
have this : (↑(r + 1) : ℕ∞) ≤ K.height
Tactic: have := hr.trans (Ideal.height_mono e)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
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
K : Ideal R
hK : K ∈ hS.toFinset (s := S)
e : I ≤ K
this : (↑(r + 1) : ℕ∞) ≤ K.height
⊢ False
have hK₁ : K ∈ S
Tactic: rw [Set.Finite.mem_toFinset] at hK
Cleared hypotheses: hK, e, this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
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
K : Ideal R
hK : K ∈ S
e : I ≤ K
this : (↑(r + 1) : ℕ∞) ≤ K.height
⊢ False
have this₁ : ¬LT.lt (α := ℕ∞) (↑r : ℕ∞) (↑(r + 1) : ℕ∞)
Tactic: rw [hK.2, ← not_lt] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
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
K : Ideal R
hK : K ∈ S
e : I ≤ K
this : ¬LT.lt (α := ℕ∞) (↑r : ℕ∞) (↑(r + 1) : ℕ∞)
⊢ False
have this₁ : ¬r < r + 1
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
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
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
have this : ¬(↑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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (hypothesis)
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)
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
have this₁ : ∃ 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
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)
⊢ ∃ J ≤ I, Submodule.spanRank J ≤ (↑(r + 1) : Cardinal.{u_1}) ∧ (↑(r + 1) : ℕ∞) ≤ J.height
have 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
Tactic: obtain ⟨x, hx₁, hx₂⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Height (goal)
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
have succ : span {x} ≤ I
Tactic: refine ⟨J ⊔ Ideal.span {x}, sup_le h₁ ?_, ?_, ?_⟩