R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
⊢ IsNilpotent (Ideal.jacobson ⊥)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
⊢ IsNilpotent (Ideal.jacobson ⊥)
let Jac := Ideal.jacobson (⊥ : Ideal R)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
⊢ IsNilpotent (Ideal.jacobson ⊥)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
⊢ IsNilpotent (Ideal.jacobson ⊥)
let f : ℕ →o (Ideal R)ᵒᵈ := ⟨fun n => Jac ^ n, fun _ _ h => Ideal.pow_le_pow h⟩
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
⊢ IsNilpotent (Ideal.jacobson ⊥)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
⊢ IsNilpotent (Ideal.jacobson ⊥)
obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → Jac ^ n = Jac ^ m := IsArtinian.monotone_stabilizes f
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
⊢ Ideal.jacobson ⊥ ^ n = 0
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
⊢ IsNilpotent (Ideal.jacobson ⊥)
refine' ⟨n, _⟩
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
⊢ Ideal.jacobson ⊥ ^ n = 0
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
⊢ Ideal.jacobson ⊥ ^ n = 0
let J : Ideal R := annihilator (Jac ^ n)
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
⊢ J = ⊤
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
⊢ Ideal.jacobson ⊥ ^ n = 0
suffices J = ⊤ by
  have hJ : J • Jac ^ n = ⊥ := annihilator_smul (Jac ^ n)
  simpa only [this, top_smul, Ideal.zero_eq_bot] using hJ
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : ¬J = ⊤
⊢ False
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
⊢ J = ⊤
by_contra hJ
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
⊢ False
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : ¬J = ⊤
⊢ False
change J ≠ ⊤ at hJ
case intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
⊢ False
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
⊢ False
rcases IsArtinian.set_has_minimal { J' : Ideal R | J < J' } ⟨⊤, hJ.lt_top⟩ with
  ⟨J', hJJ' : J < J', hJ' : ∀ I, J < I → ¬I < J'⟩
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ False
case intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
⊢ False
rcases SetLike.exists_of_lt hJJ' with ⟨x, hxJ', hxJ⟩
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
⊢ False
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
⊢ False
have : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x} :=
  sup_le_sup_left (smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ False
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
⊢ False
have : Jac * Ideal.span {x} ≤ J := by by_contra H
  refine' H (smul_sup_le_of_le_smul_of_le_jacobson_bot (fg_span_singleton _) le_rfl
    (this.eq_of_not_lt (hJ' _ _)).ge)
  exact lt_of_le_of_ne le_sup_left fun h => H <| h.symm ▸ le_sup_right
case this
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥

case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
⊢ False
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ False
have : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
⊢ False
case this
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥

case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
⊢ False
calc
  Ideal.span {x} * Jac ^ (n + 1) = Ideal.span {x} * Jac * Jac ^ n := by rw [pow_succ, ← mul_assoc]
  _ ≤ J * Jac ^ n := (mul_le_mul (by rwa [mul_comm]) le_rfl)
  _ = ⊥ := by simp
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
y : R
hy : y ∈ Jac ^ n
⊢ x • y ∈ ⊥
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
⊢ False
refine' hxJ (mem_annihilator.2 fun y hy => (mem_bot R).1 _)
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
y : R
hy : y ∈ Jac ^ n
⊢ y ∈ Jac ^ (n + 1)
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
y : R
hy : y ∈ Jac ^ n
⊢ x • y ∈ ⊥
refine' this (mul_mem_mul (mem_span_singleton_self x) _)
no goals
case intro.intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this✝ : Jac * Ideal.span {x} ≤ J
this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
y : R
hy : y ∈ Jac ^ n
⊢ y ∈ Jac ^ (n + 1)
rwa [← hn (n + 1) (Nat.le_succ _)]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
this : J = ⊤
hJ : J • Jac ^ n = ⊥
⊢ Ideal.jacobson ⊥ ^ n = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
this : J = ⊤
⊢ Ideal.jacobson ⊥ ^ n = 0
have hJ : J • Jac ^ n = ⊥ := annihilator_smul (Jac ^ n)
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
this : J = ⊤
hJ : J • Jac ^ n = ⊥
⊢ Ideal.jacobson ⊥ ^ n = 0
simpa only [this, top_smul, Ideal.zero_eq_bot] using hJ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J ⊔ Ideal.span {x} ≤ J'

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J < J ⊔ Ideal.span {x}
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J ⊔ Ideal.span {x} = J'
apply eq_of_le_of_not_lt _ (hJ' (J ⊔ Ideal.span {x}) _)
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J ⊔ Ideal.span {x} ≤ J'
exact sup_le hJJ'.le (span_le.2 (singleton_subset_iff.2 hxJ'))
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J ≤ J ⊔ Ideal.span {x} ∧ ∃ x_1, x_1 ∈ J ⊔ Ideal.span {x} ∧ ¬x_1 ∈ J
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J < J ⊔ Ideal.span {x}
rw [SetLike.lt_iff_le_and_exists]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
J' : Submodule R R
hJJ' : J < J'
hJ' : ∀ (I : Ideal R), J < I → ¬I < J'
x : R
hxJ' : x ∈ J'
hxJ : ¬x ∈ J
⊢ J ≤ J ⊔ Ideal.span {x} ∧ ∃ x_1, x_1 ∈ J ⊔ Ideal.span {x} ∧ ¬x_1 ∈ J
exact ⟨le_sup_left, ⟨x, mem_sup_right (mem_span_singleton_self x), hxJ⟩⟩
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
H : ¬Jac * Ideal.span {x} ≤ J
⊢ False
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
⊢ Jac * Ideal.span {x} ≤ J
by_contra H
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
H : ¬Jac * Ideal.span {x} ≤ J
⊢ J < J ⊔ Jac • Ideal.span {x}
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
H : ¬Jac * Ideal.span {x} ≤ J
⊢ False
refine' H (smul_sup_le_of_le_smul_of_le_jacobson_bot (fg_span_singleton _) le_rfl
  (this.eq_of_not_lt (hJ' _ _)).ge)
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
H : ¬Jac * Ideal.span {x} ≤ J
⊢ J < J ⊔ Jac • Ideal.span {x}
exact lt_of_le_of_ne le_sup_left fun h => H <| h.symm ▸ le_sup_right
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ Ideal.span {x} * Jac ^ (n + 1) = Ideal.span {x} * Jac * Jac ^ n
rw [pow_succ, ← mul_assoc]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ Ideal.span {x} * Jac ≤ J
rwa [mul_comm]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ideal.jacobson ⊥
f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := (_ : ∀ (x x_1 : ℕ), x ≤ x_1 → Jac ^ x_1 ≤ Jac ^ x) }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m
J : Ideal R := annihilator (Jac ^ n)
hJ : J ≠ ⊤
x : R
hxJ : ¬x ∈ J
hJJ' : J < J ⊔ Ideal.span {x}
hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}
hxJ' : x ∈ J ⊔ Ideal.span {x}
this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}
this : Jac * Ideal.span {x} ≤ J
⊢ J * Jac ^ n = ⊥
simp