case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ jacobson I = I → ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M

case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ (∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M) → jacobson I = I
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ jacobson I = I ↔ ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
constructor
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : jacobson I = I
x : R
hx : ¬x ∈ I
⊢ ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ jacobson I = I → ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
intro h x hx
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : jacobson I = I
x : R
hx : ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsMaximal J} → x ∈ I_1
⊢ ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : jacobson I = I
x : R
hx : ¬x ∈ I
⊢ ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
erw [← h, mem_sInf] at hx
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : jacobson I = I
x : R
hx : Exists fun ⦃I_1⦄ => I_1 ∈ {J | I ≤ J ∧ IsMaximal J} ∧ ¬x ∈ I_1
⊢ ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : jacobson I = I
x : R
hx : ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsMaximal J} → x ∈ I_1
⊢ ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
push_neg  at hx
no goals
case mp
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : jacobson I = I
x : R
hx : Exists fun ⦃I_1⦄ => I_1 ∈ {J | I ≤ J ∧ IsMaximal J} ∧ ¬x ∈ I_1
⊢ ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
exact hx
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : x ∈ jacobson I
⊢ x ∈ I
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
⊢ (∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M) → jacobson I = I
refine fun h => le_antisymm (fun x hx => ?_) le_jacobson
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : ¬x ∈ I
⊢ ¬x ∈ jacobson I
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : x ∈ jacobson I
⊢ x ∈ I
contrapose hx
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : ¬x ∈ I
⊢ ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsMaximal J} → x ∈ I_1
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : ¬x ∈ I
⊢ ¬x ∈ jacobson I
erw [mem_sInf]
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : ¬x ∈ I
⊢ Exists fun ⦃I_1⦄ => I_1 ∈ {J | I ≤ J ∧ IsMaximal J} ∧ ¬x ∈ I_1
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : ¬x ∈ I
⊢ ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsMaximal J} → x ∈ I_1
push_neg
no goals
case mpr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
h : ∀ (x : R), ¬x ∈ I → ∃ M, (I ≤ M ∧ IsMaximal M) ∧ ¬x ∈ M
x : R
hx : ¬x ∈ I
⊢ Exists fun ⦃I_1⦄ => I_1 ∈ {J | I ≤ J ∧ IsMaximal J} ∧ ¬x ∈ I_1
exact h x hx