awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this_1 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
this_2 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
this : Nontrivial R
l : LTSeries (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(l.length (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (PrimeSpectrum R)),
      (↑(p.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
have neg : ∀ (p : Ideal R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p)
  (hp' :
    p ≤
      (↑(RelSeries.head (r :=
              {x :
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
                match (motive :=
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                      (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                    Prop)
                  x with
                | (a, b) => a < b})
              l) :
          PrimeSpectrum R).asIdeal),
  HAdd.hAdd (α := ℕ∞)
      (↑(l.length (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (PrimeSpectrum R)),
      (↑(p.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
Tactic: obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le (J := l.head.1.asIdeal) bot_le
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this_1 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
this_2 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
this : Nontrivial R
l : LTSeries (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
hp' :
  p ≤
    (↑(RelSeries.head (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})
            l) :
        PrimeSpectrum R).asIdeal
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(l.length (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (PrimeSpectrum R)),
      (↑(p.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
have hp'₁ : p' <
  (↑(RelSeries.head (r :=
        {x :
          (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
            (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
          match (motive :=
            (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
              Prop)
            x with
          | (a, b) => a < b})
        l) :
    PrimeSpectrum R)
Tactic: have hp' : p' < l.head := lt_of_le_of_ne hp' fun h ↦ Set.disjoint_iff.mp
    (Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes hp)
    ⟨show r ∈ p by simpa [← h] using l.head.2, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
⊢ ringKrullDim S + 1 ≤ ringKrullDim R
have refine : ringKrullDim S + 1 ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1
Tactic: refine le_trans ?_ (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hr)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
⊢ ringKrullDim S + 1 ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1
have bc : ringKrullDim S ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
inst_1 : Finite σ
α β : Type u_3
e : α ≃ β
H : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial α R)
⊢ ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial β R)
have h : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
Tactic: convert! ← H using 1
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
inst_1 : Finite σ
α β : Type u_3
e : α ≃ β
H : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial α R)
h : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
⊢ ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial β R)
have h₁ : ringKrullDim (MvPolynomial α R) = ringKrullDim (MvPolynomial β R)
Tactic: convert! ← H using 1
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
inst_1 : Finite σ
α β : Type u_3
e : α ≃ β
H : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial α R)
⊢ ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
have h : ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
Tactic: rw [Nat.card_congr e]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
inst_1 : Finite σ
α : Type u_3
inst_2 : Fintype α
IH : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial α R)
⊢ ringKrullDim R + (↑(Nat.card.{u_3} (Option α)) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial.{u_3, u_1} (Option α) R)
have h_option : ∀ (IH : ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial α R)),
  ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1 ≤ ringKrullDim (MvPolynomial.{u_3, u_1} (Option α) R)
Tactic: simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
inst_1 : Finite σ
α : Type u_3
inst_2 : Fintype α
IH : ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial α R)
⊢ ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1 ≤ ringKrullDim (MvPolynomial.{u_3, u_1} (Option α) R)
have h_option : ringKrullDim (Polynomial (MvPolynomial α R)) ≤ ringKrullDim (MvPolynomial.{u_3, u_1} (Option α) R)
Tactic: grw [IH, ringKrullDim_succ_le_ringKrullDim_polynomial]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
inst_1 : Finite σ
⊢ ringKrullDim R + (↑(Nat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
have of_equiv : ∀ {α β : Type u_3} (e : α ≃ β) (H : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial α R)),
  ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial β R)
Tactic: induction σ using Finite.induction_empty_option with
  | of_equiv e H =>
    convert! ← H using 1
    · rw [Nat.card_congr e]
    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
  | h_empty => simp
  | h_option IH =>
    simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
    grw [IH, ringKrullDim_succ_le_ringKrullDim_polynomial]
    exact (ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv).ge
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
inst_1 : Finite σ
of_equiv :
  ∀ {α β : Type u_3} (e : α ≃ β) (H : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial α R)),
    ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial β R)
⊢ ringKrullDim R + (↑(Nat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
have h_empty : ringKrullDim R + (↑(Nat.card PEmpty.{u_3 + 1}) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial PEmpty.{u_3 + 1} R)
Tactic: induction σ using Finite.induction_empty_option with
  | of_equiv e H =>
    convert! ← H using 1
    · rw [Nat.card_congr e]
    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
  | h_empty => simp
  | h_option IH =>
    simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
    grw [IH, ringKrullDim_succ_le_ringKrullDim_polynomial]
    exact (ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv).ge
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
inst_1 : Finite σ
of_equiv :
  ∀ {α β : Type u_3} (e : α ≃ β) (H : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial α R)),
    ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial β R)
h_empty : ringKrullDim R + (↑(Nat.card PEmpty.{u_3 + 1}) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial PEmpty.{u_3 + 1} R)
⊢ ringKrullDim R + (↑(Nat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
have h_option : ∀ {α : Type u_3} [Fintype α] (IH : ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial α R)),
  ringKrullDim R + (↑(Nat.card.{u_3} (Option α)) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial.{u_3, u_1} (Option α) R)
Tactic: induction σ using Finite.induction_empty_option with
  | of_equiv e H =>
    convert! ← H using 1
    · rw [Nat.card_congr e]
    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
  | h_empty => simp
  | h_option IH =>
    simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
    grw [IH, ringKrullDim_succ_le_ringKrullDim_polynomial]
    exact (ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv).ge
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
⊢ ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
⊢ ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
have inl : Finite σ → ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
Tactic: cases finite_or_infinite σ
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
inl : Finite σ → ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
⊢ ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
have inr : Infinite σ → ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
Tactic: cases finite_or_infinite σ
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Finite σ
⊢ ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
have inl : ringKrullDim R + (↑(↑(Nat.card σ) : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
Tactic: rw [ENat.card_eq_coe_natCard]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
⊢ ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
have inr : ringKrullDim R + ⊤ ≤ ringKrullDim (MvPolynomial σ R)
Tactic: simp only [ENat.card_eq_top_of_infinite, WithBot.coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
⊢ ringKrullDim R + ⊤ ≤ ringKrullDim (MvPolynomial σ R)
have inr : ringKrullDim (MvPolynomial σ R) = ⊤
Tactic: suffices ringKrullDim (MvPolynomial σ R) = ⊤ by simp_all
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
⊢ ringKrullDim (MvPolynomial σ R) = ⊤
have inr : ∀ (a : ℕ), (↑(↑a : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim (MvPolynomial σ R)
Tactic: rw [WithBot.eq_top_iff_forall_ge]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := (⇑(Infinite.natEmbedding σ) : (a : ℕ) → σ) ∘ Fin.val
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim (MvPolynomial σ R)
have this : Function.Surjective (Function.invFun ι)
Tactic: have := Function.invFun_surjective (f := ι) ((Infinite.natEmbedding σ).2.comp Fin.val_injective)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := (⇑(Infinite.natEmbedding σ) : (a : ℕ) → σ) ∘ Fin.val
this : Function.Surjective (Function.invFun ι)
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim (MvPolynomial σ R)
have inr : (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim.{u_1} (MvPolynomial (Fin (n + 1)) R)
Tactic: refine le_trans ?_ (ringKrullDim_le_of_surjective
      (rename (R := R) _).toRingHom (rename_surjective _ this))
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := (⇑(Infinite.natEmbedding σ) : (a : ℕ) → σ) ∘ Fin.val
this : Function.Surjective (Function.invFun ι)
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim.{u_1} (MvPolynomial (Fin (n + 1)) R)
have inr : (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim R + (↑(Nat.card (Fin (n + 1))) : WithBot ℕ∞)
Tactic: refine le_trans ?_ (ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial _)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := (⇑(Infinite.natEmbedding σ) : (a : ℕ) → σ) ∘ Fin.val
this : Function.Surjective (Function.invFun ι)
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim R + (↑(Nat.card (Fin (n + 1))) : WithBot ℕ∞)
have inr : (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim R + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
Tactic: simp only [ENat.some_eq_coe, Nat.card_eq_fintype_card, Fintype.card_fin, Nat.cast_add,
      Nat.cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := (⇑(Infinite.natEmbedding σ) : (a : ℕ) → σ) ∘ Fin.val
this : Function.Surjective (Function.invFun ι)
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim R + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
have trans : (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ HAdd.hAdd (α := WithBot (WithTop ℕ)) (↑n : WithBot (WithTop ℕ)) 1
Tactic: trans n + 1
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := (⇑(Infinite.natEmbedding σ) : (a : ℕ) → σ) ∘ Fin.val
this : Function.Surjective (Function.invFun ι)
trans : (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ HAdd.hAdd (α := WithBot (WithTop ℕ)) (↑n : WithBot (WithTop ℕ)) 1
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim R + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
have trans₁ : HAdd.hAdd (α := WithBot (WithTop ℕ)) (↑n : WithBot (WithTop ℕ)) 1 ≤
  ringKrullDim R + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
Tactic: trans n + 1
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := (⇑(Infinite.natEmbedding σ) : (a : ℕ) → σ) ∘ Fin.val
this : Function.Surjective (Function.invFun ι)
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ HAdd.hAdd (α := WithBot (WithTop ℕ)) (↑n : WithBot (WithTop ℕ)) 1
have norm_cast : n ≤ n + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
⊢ Ring.KrullDimLE 1 R
have refine : ∀ (I : Ideal R) (hI : I.IsPrime) (hI' : I ∉ minimalPrimes R), I.IsMaximal
Tactic: refine Ring.krullDimLE_one_iff.2 fun I hI ↦ or_iff_not_imp_left.2 fun hI' ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
hI' : I ∉ minimalPrimes R
⊢ I.IsMaximal
have hI'₁ : ∃ y < I, y.IsPrime
Tactic: rw [minimalPrimes_eq_minimals, Set.notMem_setOf_iff, not_minimal_iff_exists_lt hI] at hI'
Cleared hypotheses: hI'
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
hI' : ∃ y < I, y.IsPrime
⊢ I.IsMaximal
have obtain : ∀ (P : Ideal R) (hlt : P < I) (hP : P.IsPrime), I.IsMaximal
Tactic: obtain ⟨P, hlt, hP⟩ := hI'
Cleared hypotheses: hI'
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
⊢ I.IsMaximal
have this : IsPrincipalIdealRing.{u_1} (R ⧸ P)
Tactic: have := IsPrincipalIdealRing.of_surjective (Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this : IsPrincipalIdealRing.{u_1} (R ⧸ P)
⊢ Ideal.IsMaximal (α := R ⧸ P) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I)
have this₁ : Ideal.IsPrime (α := R ⧸ P) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I)
Tactic: have := Ideal.map_isPrime_of_surjective (f := Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective
      (I := I) (by simpa using hlt.le)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this_1 : IsPrincipalIdealRing.{u_1} (R ⧸ P)
this : Ideal.IsPrime (α := R ⧸ P) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I)
⊢ Ideal.IsMaximal (α := R ⧸ P) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I)
have refine : Ne (α := Ideal (R ⧸ P)) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I) ⊥
Tactic: refine IsPrime.to_maximal_ideal ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this_1 : IsPrincipalIdealRing.{u_1} (R ⧸ P)
this : Ideal.IsPrime (α := R ⧸ P) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I)
⊢ Ne (α := Ideal (R ⧸ P)) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I) ⊥
have rw : ¬I ≤ P
Tactic: rw [ne_eq, Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this : IsPrincipalIdealRing.{u_1} (R ⧸ P)
⊢ I.IsMaximal
have this₁ : Ideal.IsMaximal (α := R ⧸ P) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I)
Tactic: have : (I.map (Ideal.Quotient.mk P)).IsMaximal := by
    have := Ideal.map_isPrime_of_surjective (f := Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective
      (I := I) (by simpa using hlt.le)
    refine IsPrime.to_maximal_ideal ?_
    rw [ne_eq, Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker]
    exact hlt.not_ge
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
P : Ideal R
hlt : P < I
hP : P.IsPrime
this_1 : IsPrincipalIdealRing.{u_1} (R ⧸ P)
this : Ideal.IsMaximal (α := R ⧸ P) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I)
⊢ I.IsMaximal
have this₁ : Ideal.IsMaximal
  (Ideal.comap (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I))
Tactic: have := Ideal.comap_isMaximal_of_surjective (Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective
    (K := I.map (Ideal.Quotient.mk P))
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.PID (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
⊢ ringKrullDim R = 1
have apply : ringKrullDim R ≤ 1
Tactic: apply eq_of_le_of_not_lt ?_ fun h' ↦ h ?_