-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem eq_jacobson_iff_not_mem :
    I.jacobson = I ↔ ∀ x ∉ I, ∃ M : Ideal R, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Proof state:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∈ I.jacobson
⊢ x ∈ I

Tactic:
contrapose hx

Result:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ x ∉ I.jacobson

Proof state:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ ∃ I_1 ∈ {J | I ≤ J ∧ J.IsMaximal}, x ∉ I_1

Tactic:
exact h x hx

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ I.jacobson = I ↔ ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ I.jacobson = I → ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ (∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I

Proof state:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ x ∉ I.jacobson

Tactic:
rw [Ideal.jacobson, mem_sInf]

Result:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1

Proof state:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ (∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I

Tactic:
refine fun h => le_antisymm (fun x hx => ?_) le_jacobson

Result:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∈ I.jacobson
⊢ x ∈ I

Proof state:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
push_neg at hx

Result:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : ∃ I_1 ∈ {J | I ≤ J ∧ J.IsMaximal}, x ∉ I_1
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Proof state:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : ∃ I_1 ∈ {J | I ≤ J ∧ J.IsMaximal}, x ∉ I_1
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
exact hx

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ I.jacobson = I → ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
intro h x hx

Result:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : x ∉ I
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Proof state:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : x ∉ I
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
rw [← h, Ideal.jacobson, mem_sInf] at hx

Result:
case mp
R : Type u
inst✝ : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
⊢ ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Proof state:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1

Tactic:
push_neg

Result:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ ∃ I_1 ∈ {J | I ≤ J ∧ J.IsMaximal}, x ∉ I_1