awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : IsLocalRing R
rs : List R
reg : Sequence.IsRegular M rs
nil :
  ∀ {M : Type u_2} [inst_6 : AddCommGroup M] [inst_7 : Module R M] [Module.Finite R M]
    (reg : Sequence.IsRegular.{u_1, u_2} (R := R) M []),
    supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal R) (β := Submodule R M) (ofList []) ⊤) +
        (↑(List.length.{u_1} (α := R) []) : WithBot ℕ∞) =
      supportDim R M
⊢ supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (ofList rs) ⊤) +
      (↑rs.length : WithBot ℕ∞) =
    supportDim R M
have cons : ∀ (x : R) (rs' : List R)
  (ih :
    ∀ {M : Type u_2} [inst_6 : AddCommGroup M] [inst_7 : Module R M] [Module.Finite R M]
      (reg : Sequence.IsRegular M rs'),
      supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (ofList rs') ⊤) +
          (↑rs'.length : WithBot ℕ∞) =
        supportDim R M)
  {M : Type u_2} [inst_6 : AddCommGroup M] [inst_7 : Module R M] [Module.Finite R M]
  (reg : Sequence.IsRegular M (x :: rs')),
  supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (ofList (x :: rs')) ⊤) +
      (↑(x :: rs').length : WithBot ℕ∞) =
    supportDim R M
Tactic: induction rs generalizing M with
  | nil =>
    rw [ofList_nil, Submodule.bot_smul]
    simpa using supportDim_eq_of_equiv (Submodule.quotEquivOfEqBot ⊥ rfl)
  | cons x rs' ih =>
    have mem : x ∈ maximalIdeal R := by
      simpa using fun isu ↦ reg.2 (by simp [span_singleton_eq_top.mpr isu])
    simp [supportDim_eq_of_equiv (Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M x _),
      ← supportDim_quotSMulTop_succ_eq_supportDim ((isRegular_cons_iff M _ _).mp reg).1 mem,
      ← ih ((isRegular_cons_iff M _ _).mp reg).2, ← add_assoc]
Cleared hypotheses: M, inst_2, inst_3, inst_4, rs, reg
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (ofList rs)) + (↑rs.length : WithBot ℕ∞) = ringKrullDim R
have eq : ofList rs = HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤
Tactic: have eq : ofList rs = ofList rs • (⊤ : Ideal R) := by simp
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
eq : ofList rs = HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (ofList rs)) + (↑rs.length : WithBot ℕ∞) = ringKrullDim R
have rw : supportDim R (R ⧸ HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤) + (↑rs.length : WithBot ℕ∞) = supportDim R R
Tactic: rw [ringKrullDim_eq_of_ringEquiv (quotientEquivAlgOfEq R eq).toRingEquiv,
    ← supportDim_quotient_eq_ringKrullDim, ← supportDim_self_eq_ringKrullDim]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
I J : Ideal R
inst_2 : I.IsPrime
⊢ I ∈ J.minimalPrimes ↔ J ≤ I
have rwa : I.IsPrime ∧ J ≤ I ↔ J ≤ I
Tactic: rwa [mem_minimalPrimes_iff, and_iff_right]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
I J : Ideal R
inst_2 : I.IsPrime
rwa : I.IsPrime ∧ J ≤ I ↔ J ≤ I
⊢ I ∈ J.minimalPrimes ↔ J ≤ I
have rwa₁ : J ≤ I ↔ J ≤ I
Tactic: rwa [mem_minimalPrimes_iff, and_iff_right]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
⊢ Eq (α := Set (Ideal R)) (minimalPrimes R) {I : Ideal R | I.IsPrime}
have h : ∀ (x : Ideal R),
  Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x ↔
    Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsPrime} x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
⊢ Eq (α := Set (Ideal R)) (minimalPrimes R) {I : Ideal R | I.IsMaximal}
have h : ∀ (x : Ideal R),
  Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x ↔
    Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
inst_2 : IsDomain R
⊢ IsField R
have by_contra : ∀ (h : ¬IsField R), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
inst_2 : IsDomain R
h : ¬IsField R
⊢ False
have obtain : ∀ (p : Ideal R) (hp : p ≠ ⊥) (h : p.IsPrime), False
Tactic: obtain ⟨p, hp, h⟩ := Ring.not_isField_iff_exists_prime.mp h
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ Ring.KrullDimLE 0 R ↔ ringKrullDim R = 0
have rw : ringKrullDim R ≤ 0 → 0 ≤ ringKrullDim R
Tactic: rw [Ring.KrullDimLE, Order.krullDimLE_iff, le_antisymm_iff, ← ringKrullDim, Nat.cast_zero,
    iff_self_and]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
h₁ : KrullDimLE 0 R
h₂ : IsLocalRing R
x : R
⊢ IsNilpotent x ↔ ¬IsUnit x
have change : Membership.mem (γ := Ideal R) (nilradical R) x ↔ Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) x
Tactic: change x ∈ nilradical R ↔ x ∈ IsLocalRing.maximalIdeal R
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
h₁ : KrullDimLE 0 R
h₂ : IsLocalRing R
x : R
⊢ Membership.mem (γ := Ideal R) (nilradical R) x ↔ Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) x
have rw : Membership.mem (γ := Ideal R) (sInf {J : Ideal R | 0 ≤ J ∧ J.IsPrime}) x ↔
  Membership.mem (γ := Ideal R) (IsLocalRing.maximalIdeal R) x
Tactic: rw [nilradical, Ideal.radical_eq_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ [KrullDimLE 0 R ∧ IsLocalRing R, ∃! I : Ideal R, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x,
      Ideal.IsMaximal (nilradical R)].TFAE
have tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
Tactic: tfae_have 1 → 3 := by
    intro ⟨h₁, h₂⟩ x
    change x ∈ nilradical R ↔ x ∈ IsLocalRing.maximalIdeal R
    rw [nilradical, Ideal.radical_eq_sInf]
    simp [← Ideal.isMaximal_iff_isPrime, IsLocalRing.isMaximal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
⊢ ∀ (a : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x), Ideal.IsMaximal (nilradical R)
have refine_1 : ∀ (H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x) (e : Eq (α := Ideal R) (nilradical R) ⊤), False
Tactic: refine fun H ↦ ⟨fun e ↦ ?_, fun I hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
refine_1 : ∀ (H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x) (e : Eq (α := Ideal R) (nilradical R) ⊤), False
⊢ ∀ (a : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x), Ideal.IsMaximal (nilradical R)
have refine_2 : ∀ (H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x) (I : Ideal R) (hI : nilradical R < I), I = ⊤
Tactic: refine fun H ↦ ⟨fun e ↦ ?_, fun I hI ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
e : Eq (α := Ideal R) (nilradical R) ⊤
⊢ False
have refine_1 : ∀ (n : ℕ) (hn : Membership.mem (γ := Ideal R) 0 (HPow.hPow (α := R) 1 n)), False
Tactic: obtain ⟨n, hn⟩ := (Ideal.eq_top_iff_one _).mp e
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
H : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
I : Ideal R
hI : nilradical R < I
⊢ I = ⊤
have refine_2 : ∀ (x : R) (hx : x ∈ I) (hx' : x ∉ nilradical R), I = ⊤
Tactic: obtain ⟨x, hx, hx'⟩ := (SetLike.lt_iff_le_and_exists.mp hI).2
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
⊢ [KrullDimLE 0 R ∧ IsLocalRing R, ∃! I : Ideal R, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x,
      Ideal.IsMaximal (nilradical R)].TFAE
have tfae_3_to_4 : ∀ (a : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x), Ideal.IsMaximal (nilradical R)
Tactic: tfae_have 3 → 4 := by
    refine fun H ↦ ⟨fun e ↦ ?_, fun I hI ↦ ?_⟩
    · obtain ⟨n, hn⟩ := (Ideal.eq_top_iff_one _).mp e
      exact (H 0).mp .zero ((show (1 : R) = 0 by simpa using hn) ▸ isUnit_one)
    · obtain ⟨x, hx, hx'⟩ := (SetLike.lt_iff_le_and_exists.mp hI).2
      exact Ideal.eq_top_of_isUnit_mem _ hx (not_not.mp ((H x).not.mp hx'))
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
tfae_3_to_4 : ∀ (a : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x), Ideal.IsMaximal (nilradical R)
⊢ [KrullDimLE 0 R ∧ IsLocalRing R, ∃! I : Ideal R, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x,
      Ideal.IsMaximal (nilradical R)].TFAE
have tfae_4_to_2 : ∀ (a : Ideal.IsMaximal (nilradical R)), ∃! I : Ideal R, I.IsPrime
Tactic: tfae_have 4 → 2 := fun H ↦ ⟨_, H.isPrime, fun p (hp : p.IsPrime) ↦
      (H.eq_of_le hp.ne_top (nilradical_le_prime p)).symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
tfae_3_to_4 : ∀ (a : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x), Ideal.IsMaximal (nilradical R)
tfae_4_to_2 : ∀ (a : Ideal.IsMaximal (nilradical R)), ∃! I : Ideal R, I.IsPrime
P : Ideal R
hP₁ : P.IsPrime
hP₂ : ∀ (y : Ideal R), (fun (I : Ideal R) ↦ I.IsPrime) y → y = P
⊢ KrullDimLE 0 R ∧ IsLocalRing R
have obtain : ∀ (P : Ideal R) (hP₃ : P.IsMaximal), KrullDimLE 0 R ∧ IsLocalRing R
Tactic: obtain ⟨P, hP₃, -⟩ := P.exists_le_maximal hP₁.ne_top
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
tfae_3_to_4 : ∀ (a : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x), Ideal.IsMaximal (nilradical R)
tfae_4_to_2 : ∀ (a : Ideal.IsMaximal (nilradical R)), ∃! I : Ideal R, I.IsPrime
P_1 : Ideal R
hP₁ : P_1.IsPrime
hP₂ : ∀ (y : Ideal R), (fun (I : Ideal R) ↦ I.IsPrime) y → y = P_1
P : Ideal R
hP₃ : P.IsMaximal
⊢ KrullDimLE 0 R ∧ IsLocalRing R
have hP₄ : P.IsPrime
Tactic: obtain rfl := hP₂ P hP₃.isPrime
Cleared hypotheses: P_1, hP₁, hP₂
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
tfae_3_to_4 : ∀ (a : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x), Ideal.IsMaximal (nilradical R)
tfae_4_to_2 : ∀ (a : Ideal.IsMaximal (nilradical R)), ∃! I : Ideal R, I.IsPrime
P_1 : Ideal R
hP₁ : P_1.IsPrime
hP₂ : ∀ (y : Ideal R), (fun (I : Ideal R) ↦ I.IsPrime) y → y = P_1
P : Ideal R
hP₃ : P.IsMaximal
hP₄ : P.IsPrime
⊢ KrullDimLE 0 R ∧ IsLocalRing R
have hP₅ : ∀ (y : Ideal R), (fun (I : Ideal R) ↦ I.IsPrime) y → y = P
Tactic: obtain rfl := hP₂ P hP₃.isPrime
Cleared hypotheses: P_1, hP₁, hP₂
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
tfae_1_to_3 : ∀ (a : KrullDimLE 0 R ∧ IsLocalRing R) (x : R), IsNilpotent x ↔ ¬IsUnit x
tfae_3_to_4 : ∀ (a : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x), Ideal.IsMaximal (nilradical R)
tfae_4_to_2 : ∀ (a : Ideal.IsMaximal (nilradical R)), ∃! I : Ideal R, I.IsPrime
⊢ [KrullDimLE 0 R ∧ IsLocalRing R, ∃! I : Ideal R, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x,
      Ideal.IsMaximal (nilradical R)].TFAE
have tfae_2_to_1 : ∀ (a : ∃! I : Ideal R, I.IsPrime), KrullDimLE 0 R ∧ IsLocalRing R
Tactic: tfae_have 2 → 1 := by
    rintro ⟨P, hP₁, hP₂⟩
    obtain ⟨P, hP₃, -⟩ := P.exists_le_maximal hP₁.ne_top
    obtain rfl := hP₂ P hP₃.isPrime
    exact ⟨.mk₀ fun Q h ↦ hP₂ Q h ▸ hP₃, .of_unique_max_ideal ⟨P, hP₃, fun Q h ↦ hP₂ Q h.isPrime⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Ring.KrullDimLE 0 R
inst_2 : IsLocalRing R
M : Submonoid R
⊢ M ≤ IsUnit.submonoid R ↔ 0 ∉ M
have this : ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x
Tactic: have := ((Ring.krullDimLE_zero_and_isLocalRing_tfae R).out 0 2 rfl rfl).mp ⟨‹_›, ‹_›⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
inst_2 : IsLocalRing R
I : Ideal R
hI : I ≠ ⊤
⊢ I.radical = IsLocalRing.maximalIdeal R
have rw : Eq (α := Ideal R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) (IsLocalRing.maximalIdeal R)
Tactic: rw [Ideal.radical_eq_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
inst_2 : IsLocalRing R
I : Ideal R
hI : I ≠ ⊤
⊢ Eq (α := Ideal R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) (IsLocalRing.maximalIdeal R)
have refine_1 : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} (IsLocalRing.maximalIdeal R)
Tactic: refine (sInf_le ?_).antisymm (le_sInf ?_)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
inst_2 : IsLocalRing R
I : Ideal R
hI : I ≠ ⊤
refine_1 : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} (IsLocalRing.maximalIdeal R)
⊢ Eq (α := Ideal R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) (IsLocalRing.maximalIdeal R)
have refine_2 : ∀ (b : Ideal R),
  Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} b → IsLocalRing.maximalIdeal R ≤ b
Tactic: refine (sInf_le ?_).antisymm (le_sInf ?_)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
inst_2 : IsReduced R
inst_3 : IsLocalRing R
⊢ IsField R
have rw : Eq (α := Ideal R) (IsLocalRing.maximalIdeal R) ⊥
Tactic: rw [IsLocalRing.isField_iff_maximalIdeal_eq, ← nilradical_eq_maximalIdeal,
    nilradical_eq_zero, Ideal.zero_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
inst_2 : IsReduced R
inst_3 : IsLocalRing R
rw : Eq (α := Ideal R) (IsLocalRing.maximalIdeal R) ⊥
⊢ IsField R
have rw₁ : Eq (α := Ideal R) (nilradical R) ⊥
Tactic: rw [IsLocalRing.isField_iff_maximalIdeal_eq, ← nilradical_eq_maximalIdeal,
    nilradical_eq_zero, Ideal.zero_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
inst_2 : IsReduced R
inst_3 : IsLocalRing R
rw : Eq (α := Ideal R) (IsLocalRing.maximalIdeal R) ⊥
rw₁ : Eq (α := Ideal R) (nilradical R) ⊥
⊢ IsField R
have rw₂ : Eq.{u_1 + 1} (α := Ideal R) 0 ⊥
Tactic: rw [IsLocalRing.isField_iff_maximalIdeal_eq, ← nilradical_eq_maximalIdeal,
    nilradical_eq_zero, Ideal.zero_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
inst_2 : IsReduced R
inst_3 : IsLocalRing R
rw : Eq (α := Ideal R) (IsLocalRing.maximalIdeal R) ⊥
rw₁ : Eq (α := Ideal R) (nilradical R) ⊥
rw₂ : Eq.{u_1 + 1} (α := Ideal R) 0 ⊥
⊢ IsField R
have rw₃ : Eq.{u_1 + 1} (α := Ideal R) ⊥ ⊥
Tactic: rw [IsLocalRing.isField_iff_maximalIdeal_eq, ← nilradical_eq_maximalIdeal,
    nilradical_eq_zero, Ideal.zero_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsReduced R
inst_2 : Nontrivial R
⊢ Subsingleton.{u_2 + 1} (PrimeSpectrum R) ↔ IsField R
have refine : ∀ (H : Subsingleton.{u_2 + 1} (PrimeSpectrum R)), IsField R
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ letI := H.toField; inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsReduced R
inst_2 : Nontrivial R
H : Subsingleton.{u_2 + 1} (PrimeSpectrum R)
⊢ IsField R
have this : Subsingleton.{u_2 + 1} (MaximalSpectrum R)
Tactic: have : Subsingleton (MaximalSpectrum R) := MaximalSpectrum.toPrimeSpectrum_injective.subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsReduced R
inst_2 : Nontrivial R
H : Subsingleton.{u_2 + 1} (PrimeSpectrum R)
this : Subsingleton.{u_2 + 1} (MaximalSpectrum R)
⊢ IsField R
have this₁ : IsLocalRing R
Tactic: have : IsLocalRing R := .of_singleton_maximalSpectrum
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommRing R
I_1 : Ideal R
inst_1 : Ring.KrullDimLE 0 R
I : Ideal R
hI : I.IsRadical
⊢ I.jacobson = I
have rw : I.radical = I
Tactic: rw [I.jacobson_eq_radical, hI.radical]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Zero (goal)
Goal:
R : Type u_1
inst : CommRing R
I_1 : Ideal R
inst_1 : Ring.KrullDimLE 0 R
I : Ideal R
hI : I.IsRadical
rw : I.radical = I
⊢ I.jacobson = I
have rw₁ : I = I
Tactic: rw [I.jacobson_eq_radical, hI.radical]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s : Finset (Submodule R M)
IH :
  ∀ s_1 ∈ s,
    ∀ (hs : (s.erase s_1).inf id = N),
      ∃ t ⊆ s.erase s_1, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
hs : s.inf id = N
⊢ ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
have pos : ∀ (H : ∀ J ∈ s, ¬(s.erase J).inf id ≤ J), ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
Tactic: by_cases! H : ∀ J ∈ s, ¬ (s.erase J).inf id ≤ J
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s : Finset (Submodule R M)
IH :
  ∀ s_1 ∈ s,
    ∀ (hs : (s.erase s_1).inf id = N),
      ∃ t ⊆ s.erase s_1, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
hs : s.inf id = N
pos :
  ∀ (H : ∀ J ∈ s, ¬(s.erase J).inf id ≤ J),
    ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
have neg : ∀ (H : ∃ J ∈ s, (s.erase J).inf id ≤ J), ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
Tactic: by_cases! H : ∀ J ∈ s, ¬ (s.erase J).inf id ≤ J
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s : Finset (Submodule R M)
IH :
  ∀ s_1 ∈ s,
    ∀ (hs : (s.erase s_1).inf id = N),
      ∃ t ⊆ s.erase s_1, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
hs : s.inf id = N
H : ∃ J ∈ s, (s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
have neg : ∀ (J : Submodule R M) (hJ : J ∈ s) (hJ' : (s.erase J).inf id ≤ J),
  ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
Tactic: obtain ⟨J, hJ, hJ'⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s : Finset (Submodule R M)
IH :
  ∀ s_1 ∈ s,
    ∀ (hs : (s.erase s_1).inf id = N),
      ∃ t ⊆ s.erase s_1, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
hs : s.inf id = N
J : Submodule R M
hJ : J ∈ s
hJ' : (s.erase J).inf id ≤ J
⊢ ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
have neg : (s.erase J).inf id = N
Tactic: refine (IH _ hJ ?_).imp
      fun t ↦ And.imp_left (fun ht ↦ ht.trans (Finset.erase_subset _ _))
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s : Finset (Submodule R M)
IH :
  ∀ s_1 ∈ s,
    ∀ (hs : (s.erase s_1).inf id = N),
      ∃ t ⊆ s.erase s_1, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
hs : s.inf id = N
J : Submodule R M
hJ : J ∈ s
hJ' : (s.erase J).inf id ≤ J
⊢ (s.erase J).inf id = N
have hs₁ : (insert J (s.erase J)).inf id = N
Tactic: rw [← Finset.insert_erase hJ] at hs
Cleared hypotheses: hs, hJ, hJ'
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
⊢ ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
have H : ∀ (s : Finset (Submodule R M))
  (IH :
    ∀ s_1 ∈ s,
      ∀ (hs : (s.erase s_1).inf id = N),
        ∃ t ⊆ s.erase s_1, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J)
  (hs : s.inf id = N), ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
Tactic: induction s using Finset.eraseInduction with
  | H s IH =>
    by_cases! H : ∀ J ∈ s, ¬ (s.erase J).inf id ≤ J
    · exact ⟨s, Finset.Subset.rfl, hs, H⟩
    obtain ⟨J, hJ, hJ'⟩ := H
    refine (IH _ hJ ?_).imp
      fun t ↦ And.imp_left (fun ht ↦ ht.trans (Finset.erase_subset _ _))
    rw [← Finset.insert_erase hJ] at hs
    simp [← hs, hJ']
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
⊢ ∃ (t : Finset (Submodule R M)),
    t.inf id = N ∧
      (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
        (↑t : Set (Submodule R M)).Pairwise
          ((fun (x1 x2 : Ideal R) ↦ x1 ≠ x2) on fun (J : Submodule R M) ↦ (J.colon Set.univ).radical)
have refine_1 : Finset.inf
    (Finset.image (fun (t : Finset (Submodule R M)) ↦ t.inf id)
      (Finset.image (fun (J : Submodule R M) ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s))
    id =
  N
Tactic: refine ⟨(s.image fun J ↦ {I ∈ s | (I.colon .univ).radical = (J.colon .univ).radical}).image
    fun t ↦ t.inf id, ?_, ?_, ?_⟩