awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
⊢ False
have h : ∀ (x : R) (hx : x ∈ N ∧ I x ≠ ⊥), False
Tactic: have ⟨x, hx⟩ : ∃ x ∈ N, I x ≠ ⊥ := by
      contrapose! ne
      rw [← this, ← le_bot_iff, Ideal.mul_le]
      refine fun ri hi rn hn ↦ ?_
      rw [← ne rn hn]
      exact ⟨ri, hi, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : x ∈ N ∧ I x ≠ ⊥
⊢ False
have hx₁ : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
Tactic: rw [← Ideal.span_singleton_le_iff_mem] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
⊢ I x = N
have refine : Jac * I x = I x
Tactic: refine ((hI x).trans hx.1).eq_of_not_lt (min _ ⟨?_, hx.2⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
⊢ Jac * I x = I x
have rw : Jac • I x = I x
Tactic: rw [← smul_eq_mul, ← Submodule.map_smul'', smul_eq_mul, hn]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
rw : Jac • I x = I x
⊢ Jac * I x = I x
have rw₁ : Submodule.map (LinearMap.toSpanSingleton R R x) (Jac • Jac ^ n) = I x
Tactic: rw [← smul_eq_mul, ← Submodule.map_smul'', smul_eq_mul, hn]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
rw : Jac • I x = I x
rw₁ : Submodule.map (LinearMap.toSpanSingleton R R x) (Jac • Jac ^ n) = I x
⊢ Jac * I x = I x
have rw₂ : Submodule.map (LinearMap.toSpanSingleton R R x) (Jac * Jac ^ n) = I x
Tactic: rw [← smul_eq_mul, ← Submodule.map_smul'', smul_eq_mul, hn]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
rw : Jac • I x = I x
rw₁ : Submodule.map (LinearMap.toSpanSingleton R R x) (Jac • Jac ^ n) = I x
rw₂ : Submodule.map (LinearMap.toSpanSingleton R R x) (Jac * Jac ^ n) = I x
⊢ Jac * I x = I x
have rw₃ : Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n) = I x
Tactic: rw [← smul_eq_mul, ← Submodule.map_smul'', smul_eq_mul, hn]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
⊢ False
have this₁ : I x = N
Tactic: have : I x = N := by
      refine ((hI x).trans hx.1).eq_of_not_lt (min _ ⟨?_, hx.2⟩)
      rw [← smul_eq_mul, ← Submodule.map_smul'', smul_eq_mul, hn]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this_1 : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
this : I x = N
⊢ False
have this₁ : Ideal.span {x} = N
Tactic: have : Ideal.span {x} = N := le_antisymm hx.1 (this.symm.trans_le <| hI x)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this_1 : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
this_2 : I x = N
this : Ideal.span {x} = N
⊢ False
have h : R ∙ x ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (R ∙ x)
Tactic: refine (this ▸ ne) ((Submodule.fg_span <| Set.finite_singleton x).eq_bot_of_le_jacobson_smul ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this_1 : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
this_2 : I x = N
this : Ideal.span {x} = N
⊢ R ∙ x ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (R ∙ x)
have h : Ideal.span {x} ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (Ideal.span {x})
Tactic: rw [← Ideal.span, this, smul_eq_mul, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this_1 : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
this_2 : I x = N
this : Ideal.span {x} = N
h : Ideal.span {x} ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (Ideal.span {x})
⊢ R ∙ x ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (R ∙ x)
have h₁ : N ≤ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N
Tactic: rw [← Ideal.span, this, smul_eq_mul, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this_1 : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
this_2 : I x = N
this : Ideal.span {x} = N
h : Ideal.span {x} ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (Ideal.span {x})
h₁ : N ≤ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N
⊢ R ∙ x ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (R ∙ x)
have h₂ : N ≤ Ring.jacobson R * N
Tactic: rw [← Ideal.span, this, smul_eq_mul, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn_1 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = N
ne : N ≠ ⊥
min : ∀ (x : Ideal R), Membership.mem (γ := Set (Ideal R)) {N : Ideal R | Jac * N = N ∧ N ≠ ⊥} x → ¬x < N
this_1 : Jac ^ n * N = N
I : (x : R) → Submodule R R := fun (x : R) ↦ Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n)
hI : ∀ (x : R), I x ≤ Ideal.span {x}
x : R
hx : Ideal.span {x} ≤ N ∧ I x ≠ ⊥
this_2 : I x = N
this : Ideal.span {x} = N
h : Ideal.span {x} ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (Ideal.span {x})
h₁ : N ≤ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N
h₂ : N ≤ Ring.jacobson R * N
⊢ R ∙ x ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (R ∙ x)
have h₃ : N ≤ N
Tactic: rw [← Ideal.span, this, smul_eq_mul, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
I : Ideal R
⊢ I.jacobson = I.radical
have simp_rw : sInf {J : Ideal R | I ≤ J ∧ J.IsMaximal} = I.radical
Tactic: simp_rw [Ideal.jacobson, Ideal.radical_eq_sInf, IsArtinianRing.isPrime_iff_isMaximal]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
I : Ideal R
simp_rw : sInf {J : Ideal R | I ≤ J ∧ J.IsMaximal} = I.radical
⊢ I.jacobson = I.radical
have simp_rw₁ : Eq.{u_1 + 1} (α := Ideal R) (sInf {J : Ideal R | I ≤ J ∧ J.IsMaximal}) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime})
Tactic: simp_rw [Ideal.jacobson, Ideal.radical_eq_sInf, IsArtinianRing.isPrime_iff_isMaximal]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ IsNilpotent (R := Ideal R) (nilradical R)
have rw : IsNilpotent.{u_1} (R := Ideal R) (Ideal.jacobson 0)
Tactic: rw [nilradical, ← jacobson_eq_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r' : L
⊢ ∃ (a : R), (algebraMap R L : (a : R) → L) a = r'
have obtain : ∀ (r₁ : R) (s : ↥S), ∃ (a : R), (algebraMap R L : (a : R) → L) a = IsLocalization.mk' L r₁ s
Tactic: obtain ⟨r₁, s, rfl⟩ := IsLocalization.exists_mk'_eq S r'
Cleared hypotheses: r'
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
⊢ ∃ (a : R), (algebraMap R L : (a : R) → L) a = IsLocalization.mk' L r₁ s
have rsuffices : ∀ (r₂ : R) (h : IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r₂),
  ∃ (a : R), (algebraMap R L : (a : R) → L) a = IsLocalization.mk' L r₁ s
Tactic: rsuffices ⟨r₂, h⟩ : ∃ r : R, IsLocalization.mk' L 1 s = algebraMap R L r
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
rsuffices :
  ∀ (r₂ : R) (h : IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r₂),
    ∃ (a : R), (algebraMap R L : (a : R) → L) a = IsLocalization.mk' L r₁ s
⊢ ∃ (a : R), (algebraMap R L : (a : R) → L) a = IsLocalization.mk' L r₁ s
have rsuffices₁ : ∃ (r : R), IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
Tactic: rsuffices ⟨r₂, h⟩ : ∃ r : R, IsLocalization.mk' L 1 s = algebraMap R L r
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r₂
⊢ (algebraMap R L : (a : R) → L) (r₁ * r₂) = IsLocalization.mk' L r₁ s
have rw : (algebraMap R L : (a : R) → L) (r₁ * r₂) =
  HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) r₁ : L) (IsLocalization.mk' L 1 s)
Tactic: rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r₂
rw :
  (algebraMap R L : (a : R) → L) (r₁ * r₂) =
    HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) r₁ : L) (IsLocalization.mk' L 1 s)
⊢ (algebraMap R L : (a : R) → L) (r₁ * r₂) = IsLocalization.mk' L r₁ s
have rw₁ : HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) r₁ : L) ((algebraMap R L : (a : R) → L) r₂ : L) =
  HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) r₁ : L) (IsLocalization.mk' L 1 s)
Tactic: rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
r₂ : R
h : IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r₂
rw :
  (algebraMap R L : (a : R) → L) (r₁ * r₂) =
    HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) r₁ : L) (IsLocalization.mk' L 1 s)
rw₁ :
  HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) r₁ : L) ((algebraMap R L : (a : R) → L) r₂ : L) =
    HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) r₁ : L) (IsLocalization.mk' L 1 s)
⊢ (algebraMap R L : (a : R) → L) (r₁ * r₂) = IsLocalization.mk' L r₁ s
have rw₂ : HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) r₁ : L) ((algebraMap R L : (a : R) → L) r₂ : L) =
  HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) r₁ : L) ((algebraMap R L : (a : R) → L) r₂ : L)
Tactic: rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
⊢ ∃ (r : R), IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have obtain : ∀ (n : ℕ) (r : R) (hr : (↑s : R) ^ n.succ • r = HSMul.hSMul (β := R) ((↑s : R) ^ n) 1),
  ∃ (r : R), IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
Tactic: obtain ⟨n, r, hr⟩ := IsArtinian.exists_pow_succ_smul_dvd (s : R) (1 : R)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : (↑s : R) ^ n.succ • r = HSMul.hSMul (β := R) ((↑s : R) ^ n) 1
⊢ ∃ (r : R), IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have h : IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
Tactic: use r
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : (↑s : R) ^ n.succ • r = HSMul.hSMul (β := R) ((↑s : R) ^ n) 1
⊢ IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have hr₁ : (↑s : R) ^ n * ((↑s : R) * r) = (↑s : R) ^ n * 1
Tactic: rw [smul_eq_mul, smul_eq_mul, pow_succ, mul_assoc] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : (↑s : R) ^ n * ((↑s : R) * r) = (↑s : R) ^ n * 1
⊢ IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have hr₁ : Eq.{u_2 + 1} (α := L) ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n * ((↑s : R) * r)) : L)
  ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n * 1) : L)
Tactic: apply_fun algebraMap R L at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst_2 : CommSemiring L
inst_3 : Algebra R L
inst_4 : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr :
  Eq.{u_2 + 1} (α := L) ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n * ((↑s : R) * r)) : L)
    ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n * 1) : L)
⊢ IsLocalization.mk' L 1 s = (algebraMap R L : (a : R) → L) r
have hr₁ : HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n) : L)
    (HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) (↑s : R) : L) ((algebraMap R L : (a : R) → L) r : L)) =
  HMul.hMul (α := L) (β := L) ((algebraMap R L : (a : R) → L) ((↑s : R) ^ n) : L) ((algebraMap R L : (a : R) → L) 1 : L)
Tactic: simp only [map_mul] at hr
Cleared hypotheses: hr