awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
inst_1 : IsEmpty σ
⊢ ringKrullDim (MvPolynomial σ R) = ringKrullDim R

Tactic:
ringKrullDim_eq_of_ringEquiv (isEmptyRingEquiv _ _)

Premises used: ringKrullDim_eq_of_ringEquiv, MvPolynomial.isEmptyRingEquiv
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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)

Tactic:
H
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 ℕ∞)
h₁ : ringKrullDim (MvPolynomial α R) = ringKrullDim (MvPolynomial β R)
⊢ ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial β R)

Tactic:
convert! ← H using 1
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 h₁ : ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)
⊢ ringKrullDim R + (↑(Nat.card α) : WithBot ℕ∞) = ringKrullDim R + (↑(Nat.card β) : WithBot ℕ∞)

Tactic:
rw [Nat.card_congr e]

Premises used: Nat.card_congr
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 (MvPolynomial α R) = ringKrullDim (MvPolynomial β R)

Tactic:
ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv

Premises used: ringKrullDim_eq_of_ringEquiv, AlgEquiv.toRingEquiv, MvPolynomial.renameEquiv
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 (MvPolynomial α R) = ringKrullDim (MvPolynomial β R)

Tactic:
exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv

Premises used: ringKrullDim_eq_of_ringEquiv, AlgEquiv.toRingEquiv, MvPolynomial.renameEquiv
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
inst_1 : Finite σ
⊢ ringKrullDim R + (↑(Nat.card PEmpty.{u_3 + 1}) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial PEmpty.{u_3 + 1} R)

Tactic:
simp
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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)
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)
⊢ ringKrullDim R + (↑(Nat.card.{u_3} (Option α)) : WithBot ℕ∞) ≤ 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 ⊢

Premises used: add_assoc, Fintype.card_option, Nat.cast_add, Nat.cast_one, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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)
h_option : ringKrullDim (Polynomial (MvPolynomial α R)) ≤ ringKrullDim (MvPolynomial.{u_3, u_1} (Option α) R)
⊢ ringKrullDim R + (↑(Fintype.card α) : WithBot ℕ∞) + 1 ≤ ringKrullDim (MvPolynomial.{u_3, u_1} (Option α) R)

Tactic:
grw [IH, ringKrullDim_succ_le_ringKrullDim_polynomial]

Premises used: ringKrullDim_succ_le_ringKrullDim_polynomial
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 (Polynomial (MvPolynomial α R)) ≤ ringKrullDim (MvPolynomial.{u_3, u_1} (Option α) R)

Tactic:
(ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv).ge

Premises used: Eq.ge, ringKrullDim_eq_of_ringEquiv, AlgEquiv.toRingEquiv, MvPolynomial.optionEquivLeft
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 (Polynomial (MvPolynomial α R)) ≤ ringKrullDim (MvPolynomial.{u_3, u_1} (Option α) R)

Tactic:
exact (ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv).ge

Premises used: Eq.ge, ringKrullDim_eq_of_ringEquiv, AlgEquiv.toRingEquiv, MvPolynomial.optionEquivLeft
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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)
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)
⊢ 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

Premises used: ringKrullDim_succ_le_ringKrullDim_polynomial, Eq.ge, Finite.induction_empty_option, add_assoc, ringKrullDim_eq_of_ringEquiv, Fintype.card_option, Nat.cast_add, AlgEquiv.toRingEquiv, MvPolynomial.optionEquivLeft, Nat.cast_one, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
inl : Finite σ → ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
inr : Infinite σ → ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
⊢ ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
cases finite_or_infinite σ

Premises used: finite_or_infinite
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Finite σ
inl : ringKrullDim R + (↑(↑(Nat.card σ) : ℕ∞) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)
⊢ ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
rw [ENat.card_eq_coe_natCard]

Premises used: ENat.card_eq_coe_natCard
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Finite σ
⊢ ringKrullDim R + (↑(Nat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial _

Premises used: WithBot, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Finite σ
⊢ ringKrullDim R + (↑(Nat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
exact ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial _

Premises used: ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
inr : ringKrullDim R + ⊤ ≤ ringKrullDim (MvPolynomial σ R)
⊢ ringKrullDim R + (↑(ENat.card σ) : WithBot ℕ∞) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
simp only [ENat.card_eq_top_of_infinite, WithBot.coe_top]

Premises used: ENat.card_eq_top_of_infinite, WithBot.coe_top
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
this : ringKrullDim (MvPolynomial σ R) = ⊤
⊢ ringKrullDim R + ⊤ ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
inr : ringKrullDim (MvPolynomial σ R) = ⊤
⊢ ringKrullDim R + ⊤ ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
suffices ringKrullDim (MvPolynomial σ R) = ⊤ by simp_all
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
σ : Type u_3
h : Nontrivial R
h_1 : Infinite σ
inr : ∀ (a : ℕ), (↑(↑a : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim (MvPolynomial σ R)
⊢ ringKrullDim (MvPolynomial σ R) = ⊤

Tactic:
rw [WithBot.eq_top_iff_forall_ge]

Premises used: WithBot.eq_top_iff_forall_ge
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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
⊢ Function.Surjective (Function.invFun ι)

Tactic:
have := Function.invFun_surjective (f := ι) ((Infinite.natEmbedding σ).2.comp Fin.val_injective)
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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)

Tactic:
le_trans ?_ (ringKrullDim_le_of_surjective
      (rename (R := R) _).toRingHom (rename_surjective _ this))

Premises used: MvPolynomial.rename, AlgHom.toRingHom, ringKrullDim_le_of_surjective, MvPolynomial.rename_surjective, le_trans
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 ι)
inr : (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim.{u_1} (MvPolynomial (Fin (n + 1)) R)
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
refine le_trans ?_ (ringKrullDim_le_of_surjective
      (rename (R := R) _).toRingHom (rename_surjective _ this))

Premises used: MvPolynomial.rename, AlgHom.toRingHom, ringKrullDim_le_of_surjective, MvPolynomial.rename_surjective, le_trans
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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)

Tactic:
le_trans ?_ (ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial _)

Premises used: ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, le_trans
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 ι)
inr : (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim R + (↑(Nat.card (Fin (n + 1))) : WithBot ℕ∞)
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim.{u_1} (MvPolynomial (Fin (n + 1)) R)

Tactic:
refine le_trans ?_ (ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial _)

Premises used: ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, le_trans
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 ι)
inr : (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim R + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim R + (↑(Nat.card (Fin (n + 1))) : WithBot ℕ∞)

Tactic:
simp only [ENat.some_eq_coe, Nat.card_eq_fintype_card, Fintype.card_fin, Nat.cast_add,
      Nat.cast_one]

Premises used: ENat.some_eq_coe, Fintype.card_fin, Nat.cast_add, Nat.cast_one, Nat.card_eq_fintype_card
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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
trans₁ :
  HAdd.hAdd (α := WithBot (WithTop ℕ)) (↑n : WithBot (WithTop ℕ)) 1 ≤
    ringKrullDim R + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ ringKrullDim R + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1

Tactic:
trans n + 1
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 ι)
norm_cast : n ≤ n + 1
⊢ (↑(↑n : WithTop ℕ) : WithBot (WithTop ℕ)) ≤ HAdd.hAdd (α := WithBot (WithTop ℕ)) (↑n : WithBot (WithTop ℕ)) 1

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 ≤ n + 1

Tactic:
simp
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 ι)
⊢ HAdd.hAdd (α := WithBot (WithTop ℕ)) (↑n : WithBot (WithTop ℕ)) 1 ≤
    ringKrullDim R + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1

Tactic:
WithBot.le_add_self Order.bot_lt_krullDim.ne' _

Premises used: WithBot, Order.bot_lt_krullDim, LT.lt.ne', ENat, WithBot.le_add_self, ringKrullDim, WithTop
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
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 ι)
⊢ HAdd.hAdd (α := WithBot (WithTop ℕ)) (↑n : WithBot (WithTop ℕ)) 1 ≤
    ringKrullDim R + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1

Tactic:
exact WithBot.le_add_self Order.bot_lt_krullDim.ne' _

Premises used: Order.bot_lt_krullDim, LT.lt.ne', WithBot.le_add_self
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
⊢ ringKrullDim R + 1 ≤ ringKrullDim.{u_1} R⟦X⟧

Tactic:
ringKrullDim_succ_le_of_surjective constantCoeff (⟨C ·, rfl⟩)
    MvPowerSeries.X_mem_nonzeroDivisors constantCoeff_X

Premises used: PowerSeries.constantCoeff_X, ringKrullDim_succ_le_of_surjective, PowerSeries.constantCoeff, PowerSeries.C, Exists.intro, MvPowerSeries.X_mem_nonzeroDivisors, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
⊢ Ring.KrullDimLE 1 R

Tactic:
Ring.krullDimLE_one_iff.2 fun I hI ↦ or_iff_not_imp_left.2 fun hI' ↦ ?_

Premises used: Iff.mpr, Ring.krullDimLE_one_iff, Classical.or_iff_not_imp_left
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
refine : ∀ (I : Ideal R) (hI : I.IsPrime) (hI' : I ∉ minimalPrimes R), I.IsMaximal
⊢ Ring.KrullDimLE 1 R

Tactic:
refine Ring.krullDimLE_one_iff.2 fun I hI ↦ or_iff_not_imp_left.2 fun hI' ↦ ?_

Premises used: Iff.mpr, Ring.krullDimLE_one_iff, Classical.or_iff_not_imp_left
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
hI' : I ∉ minimalPrimes R
⊢ ∃ y < I, y.IsPrime

Tactic:
rw [minimalPrimes_eq_minimals, Set.notMem_setOf_iff, not_minimal_iff_exists_lt hI] at hI'

Premises used: minimalPrimes_eq_minimals, not_minimal_iff_exists_lt, Set.notMem_setOf_iff
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
I : Ideal R
hI : I.IsPrime
hI' : ∃ y < I, y.IsPrime
obtain : ∀ (P : Ideal R) (hlt : P < I) (hP : P.IsPrime), I.IsMaximal
⊢ I.IsMaximal

Tactic:
obtain ⟨P, hlt, hP⟩ := hI'
-- Module: Mathlib.RingTheory.KrullDimension.PID
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
⊢ IsPrincipalIdealRing.{u_1} (R ⧸ P)

Tactic:
have := IsPrincipalIdealRing.of_surjective (Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.KrullDimension.PID
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)
⊢ RingHom.ker (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) ≤ I

Tactic:
simpa using hlt.le

Premises used: LT.lt.le
-- Module: Mathlib.RingTheory.KrullDimension.PID
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.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)
-- Module: Mathlib.RingTheory.KrullDimension.PID
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)

Tactic:
IsPrime.to_maximal_ideal ?_

Premises used: IsPrime.to_maximal_ideal
-- Module: Mathlib.RingTheory.KrullDimension.PID
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)
refine : Ne (α := Ideal (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)

Tactic:
refine IsPrime.to_maximal_ideal ?_

Premises used: IsPrime.to_maximal_ideal
-- Module: Mathlib.RingTheory.KrullDimension.PID
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)
rw : ¬I ≤ P
⊢ Ne (α := Ideal (R ⧸ P)) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I) ⊥

Tactic:
rw [ne_eq, Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker]

Premises used: ne_eq, Ideal.mk_ker, Ideal.map_eq_bot_iff_le_ker
-- Module: Mathlib.RingTheory.KrullDimension.PID
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)
⊢ ¬I ≤ P

Tactic:
hlt.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.RingTheory.KrullDimension.PID
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)
⊢ ¬I ≤ P

Tactic:
exact hlt.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.RingTheory.KrullDimension.PID
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)

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
-- Module: Mathlib.RingTheory.KrullDimension.PID
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)
⊢ 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))
-- Module: Mathlib.RingTheory.KrullDimension.PID
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_2 : Ideal.IsMaximal (α := R ⧸ P) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I)
this :
  Ideal.IsMaximal
    (Ideal.comap (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) (Ideal.map (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) I))
⊢ I.IsMaximal

Tactic:
simpa [Ideal.comap_map_of_surjective' (Ideal.Quotient.mk P) Ideal.Quotient.mk_surjective,
    hlt.le] using this

Premises used: Ideal.Quotient.mk, LT.lt.le, Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective'
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
apply : ringKrullDim R ≤ 1
apply₁ : ∀ (h' : ringKrullDim R < 1), IsField R
⊢ ringKrullDim R = 1

Tactic:
apply eq_of_le_of_not_lt ?_ fun h' ↦ h ?_

Premises used: eq_of_le_of_not_lt
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
rw : Ring.KrullDimLE 1 R
⊢ ringKrullDim R ≤ 1

Tactic:
rw [← Nat.cast_one, ← Ring.krullDimLE_iff]

Premises used: Ring.krullDimLE_iff, Nat.cast_one
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
⊢ Ring.KrullDimLE 1 R

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.KrullDimension.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
h : ¬IsField R
h' : ringKrullDim R < 1
⊢ ringKrullDim R ≤ 0

Tactic:
have h'' : ringKrullDim R ≤ 0 := Order.le_of_lt_succ h'