R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ (∃ M, (∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤) ∧ I = sInf M) → jacobson I = I
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ jacobson I = I ↔ ∃ M, (∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤) ∧ I = sInf M
use fun hI => ⟨{ J : Ideal R | I ≤ J ∧ J.IsMaximal }, ⟨fun _ hJ => Or.inl hJ.right, hI.symm⟩⟩
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I = sInf M
⊢ jacobson I = I
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ (∃ M, (∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤) ∧ I = sInf M) → jacobson I = I
rintro ⟨M, hM, hInf⟩
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I = sInf M
x : R
hx : x ∈ jacobson I
⊢ x ∈ I
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I = sInf M
⊢ jacobson I = I
refine le_antisymm (fun x hx => ?_) le_jacobson
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I = sInf M
x : R
hx : x ∈ jacobson I
⊢ ∀ ⦃I : Ideal R⦄, I ∈ M → x ∈ I
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I = sInf M
x : R
hx : x ∈ jacobson I
⊢ x ∈ I
rw [hInf, mem_sInf]
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ jacobson I✝
I : Ideal R
hI : I ∈ M
⊢ x ∈ I
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I = sInf M
x : R
hx : x ∈ jacobson I
⊢ ∀ ⦃I : Ideal R⦄, I ∈ M → x ∈ I
intro I hI
case intro.intro.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ jacobson I✝
I : Ideal R
hI : I ∈ M
is_max : IsMaximal I
⊢ x ∈ I

case intro.intro.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ jacobson I✝
I : Ideal R
hI : I ∈ M
is_top : I = ⊤
⊢ x ∈ I
case intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ jacobson I✝
I : Ideal R
hI : I ∈ M
⊢ x ∈ I
cases' hM I hI with is_max is_top
no goals
case intro.intro.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ jacobson I✝
I : Ideal R
hI : I ∈ M
is_max : IsMaximal I
⊢ x ∈ I
exact (mem_sInf.1 hx) ⟨le_sInf_iff.1 (le_of_eq hInf) I hI, is_max⟩
no goals
case intro.intro.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ (J : Ideal R), J ∈ M → IsMaximal J ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ jacobson I✝
I : Ideal R
hI : I ∈ M
is_top : I = ⊤
⊢ x ∈ I
exact is_top.symm ▸ Submodule.mem_top