awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
⊢ ringKrullDim R = 1
have this : ¬ringKrullDim R ≤ 0
Tactic: have : ¬ ringKrullDim R ≤ 0 := fun h ↦ by
      have : Ring.KrullDimLE 0 R := Ring.krullDimLE_iff.mpr h
      exact hn Ring.KrullDimLE.isField_of_isDomain
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
h : Ring.KrullDimLE 1 R
⊢ ringKrullDim R = 1
have h₁ : ringKrullDim R ≤ (↑1 : WithBot ℕ∞)
Tactic: rw [Ring.krullDimLE_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
⊢ ringKrullDim R = 1
have refine_3 : Ring.KrullDimLE 1 R
Tactic: suffices h : Ring.KrullDimLE 1 R by
      rw [Ring.krullDimLE_iff] at h
      exact le_antisymm h (Order.succ_le_of_lt (lt_of_not_ge this))
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
⊢ Ring.KrullDimLE 1 R
have refine_3 : ∀ (I : Ideal R) (hI : I ≠ ⊥) (hI_prime : I.IsPrime), I.IsMaximal
Tactic: refine Ring.krullDimLE_one_iff_of_noZeroDivisors.mpr fun I hI hI_prime ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI : I ≠ ⊥
hI_prime : I.IsPrime
⊢ ∃ x ∈ I, x ≠ 0
have apply : ∀ (h : ¬∃ x ∈ I, x ≠ 0), ∀ x ∈ I, Membership.mem (γ := Submodule R R) ⊥ x
Tactic: apply by_contradiction fun h ↦ (hI (le_antisymm (fun x ↦ ?_) bot_le))
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h_2 : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI : I ≠ ⊥
hI_prime : I.IsPrime
h : ¬∃ x ∈ I, x ≠ 0
x : R
⊢ x ∈ I → Membership.mem (γ := Submodule R R) ⊥ x
have h₁ : ∀ x ∈ I, x = 0
Tactic: simp only [ne_eq, not_exists, not_and, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI : I ≠ ⊥
hI_prime : I.IsPrime
⊢ I.IsMaximal
have refine_3 : ∀ (x : R) (hI : x ∈ I) (hx : x ≠ 0), I.IsMaximal
Tactic: obtain ⟨x, hI, hx⟩ : ∃ (x : R), x ∈ I ∧ x ≠ 0 := by
      apply by_contradiction fun h ↦ (hI (le_antisymm (fun x ↦ ?_) bot_le))
      simp only [ne_eq, not_exists, not_and, not_not] at h
      exact fun hx ↦ h x hx
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this : ¬ringKrullDim R ≤ 0
I : Ideal R
hI_1 : I ≠ ⊥
hI_prime : I.IsPrime
x : R
hI : x ∈ I
hx : x ≠ 0
⊢ I.IsMaximal
have this₁ : IsLocalRing.maximalIdeal R ≤ I
Tactic: have : IsLocalRing.maximalIdeal R ≤ I := le_trans (h x hx)
      ((Ideal.IsRadical.radical_le_iff hI_prime.isRadical).mpr
        ((Ideal.span_singleton_le_iff_mem I).mpr hI))
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.LocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
h_1 : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
hn : ¬IsField R
h : ∀ (x : R), x ≠ 0 → LE.le (α := Ideal R) (IsLocalRing.maximalIdeal R) (Ideal.radical (Ideal.span {x}))
this_1 : ¬ringKrullDim R ≤ 0
I : Ideal R
hI_1 : I ≠ ⊥
hI_prime : I.IsPrime
x : R
hI : x ∈ I
hx : x ≠ 0
this : IsLocalRing.maximalIdeal R ≤ I
⊢ I.IsMaximal
have this₁ : IsLocalRing.maximalIdeal R = I
Tactic: have := Ideal.IsMaximal.eq_of_le (IsLocalRing.maximalIdeal.isMaximal R) hI_prime.ne_top this
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
⊢ supportDim R M ≠ ⊥
have this : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
Tactic: have : Nonempty (Module.support R M) := nonempty_support_of_nontrivial.to_subtype
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
⊢ krullDim.{u_1} (↑(support R M) : Type u_1) =
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) (annihilator R M))
have rw : krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑(annihilator R M) : Set R)) : Type u_1) =
  ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) (annihilator R M))
Tactic: rw [support_eq_zeroLocus, ringKrullDim_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
rw :
  krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑(annihilator R M) : Set R)) : Type u_1) =
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) (annihilator R M))
⊢ krullDim.{u_1} (↑(support R M) : Type u_1) =
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) (annihilator R M))
have rw₁ : krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑(annihilator R M) : Set R)) : Type u_1) =
  krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑(annihilator R M) : Set R)) : Type u_1)
Tactic: rw [support_eq_zeroLocus, ringKrullDim_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
⊢ supportDim R R = ringKrullDim R
have this : Eq (α := _root_.Ideal R) (annihilator R R) ⊥
Tactic: have : annihilator R R = ⊥ :=
    annihilator_eq_bot.mpr ((faithfulSMul_iff_algebraMap_injective R R).mpr fun {a₁ a₂} a ↦ a)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
this : Eq (α := _root_.Ideal R) (annihilator R R) ⊥
⊢ supportDim R R = ringKrullDim R
have rw : ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) ⊥) = ringKrullDim R
Tactic: rw [supportDim_eq_ringKrullDim_quotient_annihilator, this]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
I : _root_.Ideal R
⊢ supportDim R (R ⧸ I) = ringKrullDim.{u_1} (R ⧸ I)
have rw : ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) (annihilator R (R ⧸ I))) = ringKrullDim.{u_1} (R ⧸ I)
Tactic: rw [supportDim_eq_ringKrullDim_quotient_annihilator, Ideal.annihilator_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
I : _root_.Ideal R
rw :
  ringKrullDim.{u_1} (HasQuotient.Quotient R (B := _root_.Ideal R) (annihilator R (R ⧸ I))) = ringKrullDim.{u_1} (R ⧸ I)
⊢ supportDim R (R ⧸ I) = ringKrullDim.{u_1} (R ⧸ I)
have rw₁ : ringKrullDim.{u_1} (R ⧸ I) = ringKrullDim.{u_1} (R ⧸ I)
Tactic: rw [supportDim_eq_ringKrullDim_quotient_annihilator, Ideal.annihilator_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
⊢ Eq (α := Set (PrimeSpectrum R)) (Module.support R N) (PrimeSpectrum.zeroLocus (↑(maximalIdeal R) : Set R))
have rw : Eq (α := Set (PrimeSpectrum R)) (Module.support R N) {{ asIdeal := maximalIdeal R, isPrime := sorry }}
Tactic: rw [PrimeSpectrum.zeroLocus_eq_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
⊢ Eq (α := Set (PrimeSpectrum R)) (Module.support R N) {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}
have a : LE.le (α := Set (PrimeSpectrum R)) (Module.support R N) {{ asIdeal := maximalIdeal R, isPrime := sorry }}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
a : LE.le (α := Set (PrimeSpectrum R)) (Module.support R N) {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}
⊢ Eq (α := Set (PrimeSpectrum R)) (Module.support R N) {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}
have a₁ : LE.le (α := Set (PrimeSpectrum R)) {{ asIdeal := maximalIdeal R, isPrime := sorry }} (Module.support R N)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) {{ asIdeal := maximalIdeal R, isPrime := ⋯ }} p
have a : ∀ (nmem : p ∉ {{ asIdeal := maximalIdeal R, isPrime := sorry }}), False
Tactic: by_contra nmem
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : p ∉ {{ asIdeal := maximalIdeal R, isPrime := ⋯ }}
⊢ False
have nmem₁ : ¬p = { asIdeal := maximalIdeal R, isPrime := sorry }
Tactic: push _ ∈ _ at nmem
Cleared hypotheses: nmem
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
⊢ False
have this : p < { asIdeal := maximalIdeal R, isPrime := sorry }
Tactic: have : p < ⟨maximalIdeal R, IsMaximal.isPrime' (maximalIdeal R)⟩ :=
      lt_of_le_of_ne (IsLocalRing.le_maximalIdeal IsPrime.ne_top') nmem
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
this : p < { asIdeal := maximalIdeal R, isPrime := ⋯ }
⊢ Module.supportDim R N > 0
have simp : ∃ (a : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a ∧
    ∃ (a_1 : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a_1 ∧ a < a_1
Tactic: simp only [Module.supportDim, gt_iff_lt, Order.krullDim_pos_iff, Subtype.exists,
        Subtype.mk_lt_mk, exists_prop]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (goal)
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
this : p < { asIdeal := maximalIdeal R, isPrime := ⋯ }
⊢ ∃ (a : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a ∧
      ∃ (a_1 : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a_1 ∧ a < a_1
have h : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p ∧
  ∃ (a : PrimeSpectrum R), Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) a ∧ p < a
Tactic: use p
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Module (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
this : p < { asIdeal := maximalIdeal R, isPrime := ⋯ }
⊢ False
have this₁ : Module.supportDim R N > 0
Tactic: have : Module.supportDim R N > 0 := by
      simp only [Module.supportDim, gt_iff_lt, Order.krullDim_pos_iff, Subtype.exists,
        Subtype.mk_lt_mk, exists_prop]
      use p
      simpa [hp] using ⟨_, IsLocalRing.closedPoint_mem_support R N, this⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ ringKrullDim.{u_1} (R ⧸ I) = Order.krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑I : Set R)) : Type u_1)
have rw : Order.krullDim.{u_1} (PrimeSpectrum (R ⧸ I)) = Order.krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑I : Set R)) : Type u_1)
Tactic: rw [ringKrullDim, Order.krullDim_eq_of_orderIso I.primeSpectrumQuotientOrderIsoZeroLocus]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
rw :
  Order.krullDim.{u_1} (PrimeSpectrum (R ⧸ I)) =
    Order.krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑I : Set R)) : Type u_1)
⊢ ringKrullDim.{u_1} (R ⧸ I) = Order.krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑I : Set R)) : Type u_1)
have rw₁ : Order.krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑I : Set R)) : Type u_1) =
  Order.krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑I : Set R)) : Type u_1)
Tactic: rw [ringKrullDim, Order.krullDim_eq_of_orderIso I.primeSpectrumQuotientOrderIsoZeroLocus]
-- 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
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
have pos : ∀ (hr' : Eq (α := Ideal R) (Ideal.span {r}) ⊤),
  ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
Tactic: by_cases hr' : Ideal.span {r} = ⊤
-- 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
pos :
  ∀ (hr' : Eq (α := Ideal R) (Ideal.span {r}) ⊤),
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
have neg : ∀ (hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤),
  ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
Tactic: by_cases hr' : Ideal.span {r} = ⊤
-- 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}) ⊤
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
have pos : HAdd.hAdd (α := WithBot ℕ∞) ⊥ 1 ≤ ringKrullDim R
Tactic: rw [hr', ringKrullDim_eq_bot_of_subsingleton]
-- 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}) ⊤
⊢ Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
have rwa : Set.Nonempty (α := PrimeSpectrum R) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R))
Tactic: rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty, ne_eq,
      PrimeSpectrum.zeroLocus_empty_iff_eq_top]
-- 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}) ⊤
rwa : Set.Nonempty (α := PrimeSpectrum R) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R))
⊢ Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
have rwa₁ : Ne (α := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) ∅
Tactic: rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty, ne_eq,
      PrimeSpectrum.zeroLocus_empty_iff_eq_top]
-- 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}) ⊤
rwa : Set.Nonempty (α := PrimeSpectrum R) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R))
rwa₁ : Ne (α := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) ∅
⊢ Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
have rwa₂ : ¬Eq (α := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) ∅
Tactic: rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty, ne_eq,
      PrimeSpectrum.zeroLocus_empty_iff_eq_top]
-- 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}) ⊤
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
have this : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
Tactic: have : Nonempty (PrimeSpectrum.zeroLocus (R := R) (Ideal.span {r})) := by
    rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty, ne_eq,
      PrimeSpectrum.zeroLocus_empty_iff_eq_top]
-- 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 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
have this₁ : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
Tactic: have := Ideal.Quotient.nontrivial_iff.mpr hr'
-- 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 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
have this₁ : Nontrivial R
Tactic: have := (Ideal.Quotient.mk (Ideal.span {r})).domain_nontrivial
-- 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
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
have neg : ∀ (i : LTSeries (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)),
  HAdd.hAdd (α := ℕ∞)
      (↑(i.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: rw [ringKrullDim_quotient, Order.krullDim_eq_iSup_length, ringKrullDim,
    Order.krullDim_eq_iSup_length, ← WithBot.coe_one, ← WithBot.coe_add,
    ENat.iSup_add, WithBot.coe_le_coe, iSup_le_iff]