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
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ : J ∈ I.minimalPrimes
⊢ I.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)
have rw : LE.le (α := ℕ∞) (⨅ J ∈ I.minimalPrimes, J.height : ℕ∞)
  ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
Tactic: rw [I.height_eq_inf_minimalPrimes]
-- 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 ≠ ⊤
⊢ Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
have rw : Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
  ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (↑(Submodule.spanFinrank I) : Cardinal.{u_1}) : ℕ∞)
Tactic: rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I), map_natCast]
-- 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 ≠ ⊤
rw :
  Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (↑(Submodule.spanFinrank I) : Cardinal.{u_1}) : ℕ∞)
⊢ Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑(Submodule.spanFinrank I) : ℕ∞) (↑(Submodule.spanFinrank I) : ℕ∞)
Tactic: rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I), map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ I.height ≤ (↑(Submodule.spanFinrank I) : ℕ∞)
have this : Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
  ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
Tactic: have : I.spanFinrank = I.spanRank.toENat := by
    rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I), map_natCast]
-- 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.{u_1}) ≤ Submodule.spanRank I
have trans : (↑I.height : Cardinal.{u_1}) ≤
  (↑((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)) : Cardinal.{u_1})
Tactic: trans ↑I.spanRank.toENat
-- 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 ≠ ⊤
trans :
  (↑I.height : Cardinal.{u_1}) ≤
    (↑((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)) : Cardinal.{u_1})
⊢ (↑I.height : Cardinal.{u_1}) ≤ Submodule.spanRank I
have trans₁ : (↑((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)) : Cardinal.{u_1}) ≤ Submodule.spanRank I
Tactic: trans ↑I.spanRank.toENat
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ FiniteRingKrullDim R
have apply : ringKrullDim R ≠ ⊥ ∧ ringKrullDim R ≠ ⊤
Tactic: apply finiteRingKrullDim_iff_ne_bot_and_top.mpr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ ringKrullDim R ≠ ⊥ ∧ ringKrullDim R ≠ ⊤
have rw : (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊥ ∧
  (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊤
Tactic: rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊥ ∧
    (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊤
have left : (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
left : (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊥
⊢ (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊥ ∧
    (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊤
have right : (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ (↑(Ideal.height (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞) ≠ ⊤
have right : ¬Ideal.height (IsLocalRing.maximalIdeal R) = ⊤
Tactic: rw [← WithBot.coe_top, ne_eq, WithBot.coe_inj]
-- 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 ≠ ⊤
⊢ ∃ J ≤ I, Submodule.spanRank J = (↑I.height : Cardinal.{u_1}) ∧ J.height = I.height
have obtain : ∀ (J : Ideal R) (hJ₁ : J ≤ I) (hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1}))
  (hJ₃ : (↑I.height.toNat : ℕ∞) ≤ J.height),
  ∃ J ≤ I, Submodule.spanRank J = (↑I.height : Cardinal.{u_1}) ∧ J.height = I.height
Tactic: obtain ⟨J, hJ₁, hJ₂, hJ₃⟩ := exists_spanRank_le_and_le_height_of_le_height I _
    (ENat.coe_toNat_le_self I.height)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : (↑I.height.toNat : ℕ∞) ≤ J.height
⊢ ∃ J ≤ I, Submodule.spanRank J = (↑I.height : Cardinal.{u_1}) ∧ J.height = I.height
have hJ₄ : I.height ≤ J.height
Tactic: rw [ENat.coe_toNat_eq_self.mpr (Ideal.height_ne_top hI)] at hJ₃
Cleared hypotheses: hJ₃
-- 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 ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
⊢ ∃ J ≤ I, Submodule.spanRank J = (↑I.height : Cardinal.{u_1}) ∧ J.height = I.height
have refine_1 : Submodule.spanRank J ≤ (↑I.height : Cardinal.{u_1})
Tactic: refine ⟨J, hJ₁, le_antisymm ?_ (le_trans ?_ (J.height_le_spanRank ?_)),
    le_antisymm (Ideal.height_mono hJ₁) hJ₃⟩
-- 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 ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
refine_1 : Submodule.spanRank J ≤ (↑I.height : Cardinal.{u_1})
⊢ ∃ J ≤ I, Submodule.spanRank J = (↑I.height : Cardinal.{u_1}) ∧ J.height = I.height
have refine_2 : (↑I.height : Cardinal.{u_1}) ≤ (↑J.height : Cardinal.{u_1})
Tactic: refine ⟨J, hJ₁, le_antisymm ?_ (le_trans ?_ (J.height_le_spanRank ?_)),
    le_antisymm (Ideal.height_mono hJ₁) hJ₃⟩
-- 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 ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
refine_1 : Submodule.spanRank J ≤ (↑I.height : Cardinal.{u_1})
refine_2 : (↑I.height : Cardinal.{u_1}) ≤ (↑J.height : Cardinal.{u_1})
⊢ ∃ J ≤ I, Submodule.spanRank J = (↑I.height : Cardinal.{u_1}) ∧ J.height = I.height
have refine_3 : J ≠ ⊤
Tactic: refine ⟨J, hJ₁, le_antisymm ?_ (le_trans ?_ (J.height_le_spanRank ?_)),
    le_antisymm (Ideal.height_mono hJ₁) hJ₃⟩
-- 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 ≠ ⊤
J : Ideal R
hJ₁ : J ≤ I
hJ₂ : Submodule.spanRank J ≤ (↑I.height.toNat : Cardinal.{u_1})
hJ₃ : I.height ≤ J.height
⊢ Submodule.spanRank J ≤ (↑I.height : Cardinal.{u_1})
have h : (↑I.height : Cardinal.{u_1}) = (↑I.height.toNat : Cardinal.{u_1})
Tactic: convert! hJ₂
-- 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
inst_2 : p.IsPrime
n : ℕ∞
⊢ p.height ≤ n ↔ ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
have mp : p.height ≤ n → ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
Tactic: constructor
-- 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
inst_2 : p.IsPrime
n : ℕ∞
mp : p.height ≤ n → ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
⊢ p.height ≤ n ↔ ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
have mpr : (∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})) → p.height ≤ n
Tactic: constructor
-- 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
inst_2 : p.IsPrime
n : ℕ∞
h : p.height ≤ n
⊢ ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
have mp : ∀ (I : Ideal R) (hI : I ≤ p) (e₁ : Submodule.spanRank I = (↑p.height : Cardinal.{u_1})) (e₂ : I.height = p.height),
  ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
Tactic: obtain ⟨I, hI, e₁, e₂⟩ := exists_spanRank_eq_and_height_eq p (IsPrime.ne_top ‹_›)
-- 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
inst_2 : p.IsPrime
n : ℕ∞
h : p.height ≤ n
I : Ideal R
hI : I ≤ p
e₁ : Submodule.spanRank I = (↑p.height : Cardinal.{u_1})
e₂ : I.height = p.height
⊢ ∃ (I : Ideal R), p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ (↑n : Cardinal.{u_1})
have mp : (↑p.height : Cardinal.{u_1}) ≤ (↑n : Cardinal.{u_1})
Tactic: refine ⟨I, Ideal.mem_minimalPrimes_of_height_eq hI e₂.ge, e₁.symm ▸ ?_⟩
-- 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
inst_2 : p.IsPrime
⊢ ∃ (s : Finset R),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p ∧ (↑s.card : ℕ∞) = p.height
have obtain : ∀ (I : Ideal R) (hI : p ∈ I.minimalPrimes) (hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})),
  ∃ (s : Finset R),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p ∧ (↑s.card : ℕ∞) = p.height
Tactic: obtain ⟨I, hI, hr⟩ := (p.height_le_iff_exists_minimalPrimes <| p.height).mp le_rfl
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
⊢ ∃ (s : Finset R),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p ∧ (↑s.card : ℕ∞) = p.height
have hs : (Submodule.generators I).Finite
Tactic: have hs : I.generators.Finite := (IsNoetherian.noetherian I).finite_generators
-- 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
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ Membership.mem (γ := Set (Ideal R))
    (Ideal.minimalPrimes (span (↑(hs.toFinset (s := Submodule.generators I)) : Set R))) p
have rwa : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (Submodule.generators I))) p
Tactic: rwa [hs.coe_toFinset, span, I.span_generators]
-- 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
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
rwa : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (Submodule.generators I))) p
⊢ Membership.mem (γ := Set (Ideal R))
    (Ideal.minimalPrimes (span (↑(hs.toFinset (s := Submodule.generators I)) : Set R))) p
have rwa₁ : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (Submodule.span R (Submodule.generators I))) p
Tactic: rwa [hs.coe_toFinset, span, I.span_generators]
-- 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
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ ∃ (s : Finset R),
    Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p ∧ (↑s.card : ℕ∞) = p.height
have refine : (↑hs.toFinset (s := Submodule.generators I).card : ℕ∞) = p.height
Tactic: refine ⟨hs.toFinset, by rwa [hs.coe_toFinset, span, I.span_generators], ?_⟩
-- 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
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ (↑hs.toFinset (s := Submodule.generators I).card : ℕ∞) = p.height
have rw : (↑(Submodule.spanFinrank I) : ℕ∞) = p.height
Tactic: rw [← Set.ncard_eq_toFinset_card (hs := hs), (IsNoetherian.noetherian I).generators_ncard]
-- 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
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ (↑(Submodule.spanFinrank I) : ℕ∞) = p.height
have refine_1 : (↑(Submodule.spanFinrank I) : ℕ∞) ≤ p.height
Tactic: refine le_antisymm ?_ ?_
-- 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
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
refine_1 : (↑(Submodule.spanFinrank I) : ℕ∞) ≤ p.height
⊢ (↑(Submodule.spanFinrank I) : ℕ∞) = p.height
have refine_2 : p.height ≤ (↑(Submodule.spanFinrank I) : ℕ∞)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p : Ideal R
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ (↑(Submodule.spanFinrank I) : ℕ∞) ≤ p.height
have hr₁ : (↑(Submodule.spanFinrank I) : Cardinal.{u_1}) ≤ (↑p.height : Cardinal.{u_1})
Tactic: rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I)] at hr
Cleared hypotheses: hr, hs
-- 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
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ p.height ≤ (↑(Submodule.spanFinrank I) : ℕ∞)
have h : Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
  ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
Tactic: convert_to p.height ≤ I.spanRank.toENat
-- 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
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
h :
  Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
⊢ p.height ≤ (↑(Submodule.spanFinrank I) : ℕ∞)
have refine_2 : p.height ≤ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I)
Tactic: convert_to p.height ≤ I.spanRank.toENat
-- 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
inst_2 : p.IsPrime
I : Ideal R
hI : p ∈ I.minimalPrimes
hr : Submodule.spanRank I ≤ (↑p.height : Cardinal.{u_1})
hs : (Submodule.generators I).Finite
⊢ Eq (α := ℕ∞) ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
have h : Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Submodule.spanRank I) : ℕ∞)
  ((↑(Submodule.spanFinrank I) : ℕ∞) : ℕ∞)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have this : p'.IsPrime
Tactic: have : p'.IsPrime := isPrime_map_quotientMk_of_isPrime hrp
-- 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
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this : p'.IsPrime
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have obtain : ∀ (s : Finset (R ⧸ I))
  (hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p')
  (hs : (↑s.card : ℕ∞) = p'.height),
  p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
Tactic: obtain ⟨s, hps, hs⟩ := exists_finset_card_eq_height_of_isNoetherianRing p'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
Tactic: have hsp' : (s : Set (R ⧸ I)) ⊆ (p' : Set _) := fun _ hx ↦ hps.le (subset_span hx)
-- 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
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
⊢ Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
have refine : ∀ (x : R ⧸ I) (hx : x ∈ (↑p' : Set (R ⧸ I))),
  Membership.mem (γ := Set (R ⧸ I)) ((⇑(Quotient.mk I) : (a : R) → R ⧸ I) '' (↑p : Set R)) x
Tactic: refine Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_
-- 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
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
x : R ⧸ I
hx : x ∈ (↑p' : Set (R ⧸ I))
⊢ Membership.mem (γ := Set (R ⧸ I)) ((⇑(Quotient.mk I) : (a : R) → R ⧸ I) '' (↑p : Set R)) x
have obtain : ∀ (x : R) (hx : Membership.mem (α := R ⧸ I) (↑p' : Set (R ⧸ I)) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)),
  Membership.mem (α := R ⧸ I) (γ := Set (R ⧸ I)) ((⇑(Quotient.mk I) : (a : R) → R ⧸ I) '' (↑p : Set R))
    ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have this₁ : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
Tactic: have : Set.SurjOn (Ideal.Quotient.mk I) p s := by
    refine Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    exact ⟨x, by simpa [hrp, sup_of_le_left, p'] using hx⟩
-- 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
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have obtain : ∀ (o : Finset R) (hsubset : (↑o : Set R) ⊆ (↑p : Set R))
  (ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R))
  (himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s),
  p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
Tactic: obtain ⟨o, hsubset, ho, himgo⟩ := s.exists_subset_injOn_image_eq_of_surjOn (p : Set R) this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I p : Ideal R
inst_2 : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (F := R →+* R ⧸ I) (algebraMap R (R ⧸ I)) p
this_1 : p'.IsPrime
s : Finset (R ⧸ I)
hps : Membership.mem (γ := Set (Ideal (R ⧸ I))) (Ideal.minimalPrimes (span (↑s : Set (R ⧸ I)))) p'
hs : (↑s.card : ℕ∞) = p'.height
hsp' : (↑s : Set (R ⧸ I)) ⊆ (↑p' : Set (R ⧸ I))
this : Set.SurjOn (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑p : Set R) (↑s : Set (R ⧸ I))
o : Finset R
hsubset : (↑o : Set R) ⊆ (↑p : Set R)
ho : Set.InjOn (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I) (↑o : Set R)
himgo : Finset.image (⇑(Quotient.mk I) : (a : R) → R ⧸ I) o = s
⊢ p.height ≤ height (R := R ⧸ I) (map (F := R →+* R ⧸ I) (Quotient.mk I) p) + (↑(Submodule.spanFinrank I) : ℕ∞)
have hI : I.FG
Tactic: have hI : I.FG := IsNoetherian.noetherian I