awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n_1 : ℕ
hn_1 :
  ∀ (m : ℕ),
    n_1 ≤ m →
      Eq.{u_1 + 1} (α := (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) n_1 : (Submodule R R)ᵒᵈ)
        (({ toFun := fun (x : ℕ) ↦ Jac ^ x, monotone' := ⋯ } : (a : ℕ) → (Submodule R R)ᵒᵈ) m : (Submodule R R)ᵒᵈ)
hn_2 : Jac * Jac ^ n_1 = Jac ^ n_1
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n_1 = 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
n : ℕ
hn : Jac ^ n * N = N
rwa : Jac ^ n * Jac * N = N
rwa₁ : Jac ^ n * (Jac * N) = N
rwa₂ rwa₃ rwa₄ rwa₅ : Jac ^ n * N = N
⊢ Jac ^ n.succ * N = N

Tactic:
rwa [Jac.pow_succ, mul_assoc, eq]

Premises used: mul_assoc, Submodule.pow_succ
-- Module: Mathlib.RingTheory.Artinian.Module
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
⊢ Jac ^ n * N = N

Tactic:
have : Jac ^ n * N = N := n.rec (by rw [Jac.pow_zero, N.one_mul])
      fun n hn ↦ by rwa [Jac.pow_succ, mul_assoc, eq]
-- Module: Mathlib.RingTheory.Artinian.Module
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)
x : R
rw : I x ≤ LinearMap.range (LinearMap.toSpanSingleton R R x)
⊢ I x ≤ Ideal.span {x}

Tactic:
rw [Ideal.span, LinearMap.span_singleton_eq_range]

Premises used: Ideal.span, LinearMap.span_singleton_eq_range
-- Module: Mathlib.RingTheory.Artinian.Module
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)
x : R
⊢ I x ≤ LinearMap.range (LinearMap.toSpanSingleton R R x)

Tactic:
LinearMap.map_le_range

Premises used: Set.Mem, LinearMap.map_le_range
-- Module: Mathlib.RingTheory.Artinian.Module
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)
x : R
⊢ I x ≤ LinearMap.range (LinearMap.toSpanSingleton R R x)

Tactic:
exact LinearMap.map_le_range

Premises used: LinearMap.map_le_range
-- Module: Mathlib.RingTheory.Artinian.Module
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)
⊢ ∀ (x : R), I x ≤ Ideal.span {x}

Tactic:
have hI x : I x ≤ Ideal.span {x} := by
      rw [Ideal.span, LinearMap.span_singleton_eq_range]; exact LinearMap.map_le_range
-- Module: Mathlib.RingTheory.Artinian.Module
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}
contrapose! : ∀ (ne : ∀ (x : R) (_ : x ∈ N), I x = ⊥), N = ⊥
⊢ ∃ x ∈ N, I x ≠ ⊥

Tactic:
contrapose! ne
-- Module: Mathlib.RingTheory.Artinian.Module
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
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}
ne : ∀ (x : R) (_ : x ∈ N), I x = ⊥
rw : ∀ r ∈ Jac ^ n, ∀ s ∈ N, Membership.mem (γ := Ideal R) ⊥ (r * s)
⊢ N = ⊥

Tactic:
rw [← this, ← le_bot_iff, Ideal.mul_le]

Premises used: le_bot_iff, Ideal.mul_le
-- Module: Mathlib.RingTheory.Artinian.Module
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
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}
ne : ∀ (x : R) (_ : x ∈ N), I x = ⊥
⊢ ∀ r ∈ Jac ^ n, ∀ s ∈ N, Membership.mem (γ := Ideal R) ⊥ (r * s)

Tactic:
fun ri hi rn hn ↦ ?_
-- Module: Mathlib.RingTheory.Artinian.Module
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
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}
ne : ∀ (x : R) (_ : x ∈ N), I x = ⊥
refine : ∀ (ri : R) (hi : ri ∈ Jac ^ n) (rn : R) (hn : rn ∈ N), Membership.mem (γ := Ideal R) ⊥ (ri * rn)
⊢ ∀ r ∈ Jac ^ n, ∀ s ∈ N, Membership.mem (γ := Ideal R) ⊥ (r * s)

Tactic:
refine fun ri hi rn hn ↦ ?_
-- Module: Mathlib.RingTheory.Artinian.Module
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_2 : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = 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}
ne : ∀ (x : R) (_ : x ∈ N), I x = ⊥
ri : R
hi : ri ∈ Jac ^ n
rn : R
hn : rn ∈ N
rw : ri * rn ∈ I rn
⊢ Membership.mem (γ := Ideal R) ⊥ (ri * rn)

Tactic:
rw [← ne rn hn]
-- Module: Mathlib.RingTheory.Artinian.Module
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_2 : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = 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}
ne : ∀ (x : R) (_ : x ∈ N), I x = ⊥
ri : R
hi : ri ∈ Jac ^ n
rn : R
hn : rn ∈ N
⊢ ri * rn ∈ I rn

Tactic:
⟨ri, hi, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.RingTheory.Artinian.Module
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_2 : Jac * Jac ^ n = Jac ^ n
ne_1 : ¬HPow.hPow (α := Ideal R) (Ring.jacobson R) n = 0
N : Ideal R
eq : Jac * N = 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}
ne : ∀ (x : R) (_ : x ∈ N), I x = ⊥
ri : R
hi : ri ∈ Jac ^ n
rn : R
hn : rn ∈ N
⊢ ri * rn ∈ I rn

Tactic:
exact ⟨ri, hi, rfl⟩
-- Module: Mathlib.RingTheory.Artinian.Module
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}
h : ∀ (x : R) (hx : x ∈ N ∧ I x ≠ ⊥), False
⊢ 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⟩
-- Module: Mathlib.RingTheory.Artinian.Module
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 ≠ ⊥
⊢ Ideal.span {x} ≤ N ∧ I x ≠ ⊥

Tactic:
rw [← Ideal.span_singleton_le_iff_mem] at hx

Premises used: Ideal.span_singleton_le_iff_mem
-- Module: Mathlib.RingTheory.Artinian.Module
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

Tactic:
((hI x).trans hx.1).eq_of_not_lt (min _ ⟨?_, hx.2⟩)

Premises used: LE.le.eq_of_not_lt, And.right, And.left, And.intro, LE.le.trans
-- Module: Mathlib.RingTheory.Artinian.Module
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 ≠ ⊥
refine : Jac * I x = I x
⊢ I x = N

Tactic:
refine ((hI x).trans hx.1).eq_of_not_lt (min _ ⟨?_, hx.2⟩)

Premises used: LE.le.eq_of_not_lt, And.right, And.left, And.intro, LE.le.trans
-- Module: Mathlib.RingTheory.Artinian.Module
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
rw₃ rw₄ : Submodule.map (LinearMap.toSpanSingleton R R x) (Jac ^ n) = I x
⊢ Jac * I x = I x

Tactic:
rw [← smul_eq_mul, ← Submodule.map_smul'', smul_eq_mul, hn]

Premises used: Submodule.map_smul'', smul_eq_mul
-- Module: Mathlib.RingTheory.Artinian.Module
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

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]
-- Module: Mathlib.RingTheory.Artinian.Module
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
⊢ Ideal.span {x} = N

Tactic:
have : Ideal.span {x} = N := le_antisymm hx.1 (this.symm.trans_le <| hI x)
-- Module: Mathlib.RingTheory.Artinian.Module
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 : R ∙ x ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (R ∙ x)
⊢ False

Tactic:
refine (this ▸ ne) ((Submodule.fg_span <| Set.finite_singleton x).eq_bot_of_le_jacobson_smul ?_)
-- Module: Mathlib.RingTheory.Artinian.Module
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
h₃ h₄ : N ≤ N
⊢ R ∙ x ≤ HSMul.hSMul (α := Ideal R) (β := Submodule R R) (Ring.jacobson R) (R ∙ x)

Tactic:
rw [← Ideal.span, this, smul_eq_mul, eq]

Premises used: Ideal.span, smul_eq_mul
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
⊢ IsNilpotent.{u_1} (R := Ideal R) (Ideal.jacobson ⊥)

Tactic:
Ideal.jacobson_bot (R := R) ▸ IsSemiprimaryRing.isNilpotent

Premises used: Ideal.jacobson_bot, Eq.rec, IsSemiprimaryRing.isNilpotent, Eq.symm
-- Module: Mathlib.RingTheory.Artinian.Ring
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
simp_rw₁ :
  Eq.{u_1 + 1} (α := Ideal R) (sInf {J : Ideal R | I ≤ J ∧ J.IsMaximal}) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime})
⊢ I.jacobson = I.radical

Tactic:
simp_rw [Ideal.jacobson, Ideal.radical_eq_sInf, IsArtinianRing.isPrime_iff_isMaximal]

Premises used: Ideal.jacobson, Ideal.radical_eq_sInf, IsArtinianRing.isPrime_iff_isMaximal
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
rw : IsNilpotent.{u_1} (R := Ideal R) (Ideal.jacobson 0)
⊢ IsNilpotent (R := Ideal R) (nilradical R)

Tactic:
rw [nilradical, ← jacobson_eq_radical]

Premises used: nilradical, IsArtinianRing.jacobson_eq_radical
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ IsNilpotent.{u_1} (R := Ideal R) (Ideal.jacobson 0)

Tactic:
isNilpotent_jacobson_bot

Premises used: IsArtinianRing.isNilpotent_jacobson_bot
-- Module: Mathlib.RingTheory.Artinian.Ring
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
⊢ IsNilpotent.{u_1} (R := Ideal R) (Ideal.jacobson 0)

Tactic:
exact isNilpotent_jacobson_bot

Premises used: IsArtinianRing.isNilpotent_jacobson_bot