-- Mathlib/RingTheory/Ideal/Basic.lean
theorem not_isField_iff_exists_ideal_bot_lt_and_lt_top [Nontrivial R] :
    ¬IsField R ↔ ∃ I : Ideal R, ⊥ < I ∧ I < ⊤

Proof state:
case mpr.intro.intro.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
x : R
mem : x ∈ I
ne_zero : x ∉ ⊥
⊢ False

Tactic:
rw [Submodule.mem_bot] at ne_zero

Result:
case mpr.intro.intro.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
x : R
mem : x ∈ I
ne_zero : ¬x = 0
⊢ False

Proof state:
case mpr.intro.intro.intro.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
x : R
mem : x ∈ I
ne_zero : ¬x = 0
y : R
hy : x * y = 1
⊢ False

Tactic:
rw [lt_top_iff_ne_top, Ne, Ideal.eq_top_iff_one, ← hy] at lt_top

Result:
case mpr.intro.intro.intro.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
hf : IsField R
x : R
mem : x ∈ I
ne_zero : ¬x = 0
y : R
lt_top : x * y ∉ I
hy : x * y = 1
⊢ False

Proof state:
case mp
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬IsField R → ∃ I, ⊥ < I ∧ I < ⊤

Tactic:
intro h

Result:
case mp
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
⊢ ∃ I, ⊥ < I ∧ I < ⊤

Proof state:
case h
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
x : R
nz : x ≠ 0
nu : ¬IsUnit x
⊢ Ideal.span {x} ≠ ⊥ ∧ Ideal.span {x} ≠ ⊤

Tactic:
exact ⟨mt Ideal.span_singleton_eq_bot.mp nz, mt Ideal.span_singleton_eq_top.mp nu⟩

Result:
no goals

Proof state:
case mp
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
⊢ ∃ I, ⊥ < I ∧ I < ⊤

Tactic:
obtain ⟨x, nz, nu⟩ := exists_not_isUnit_of_not_isField h

Result:
case mp.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
x : R
nz : x ≠ 0
nu : ¬IsUnit x
⊢ ∃ I, ⊥ < I ∧ I < ⊤

Proof state:
case mp.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
x : R
nz : x ≠ 0
nu : ¬IsUnit x
⊢ ∃ I, ⊥ < I ∧ I < ⊤

Tactic:
use Ideal.span {x}

Result:
case h
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
x : R
nz : x ≠ 0
nu : ¬IsUnit x
⊢ ⊥ < Ideal.span {x} ∧ Ideal.span {x} < ⊤

Proof state:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬IsField R ↔ ∃ I, ⊥ < I ∧ I < ⊤

Tactic:
constructor

Result:
case mp
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬IsField R → ∃ I, ⊥ < I ∧ I < ⊤

case mpr
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (∃ I, ⊥ < I ∧ I < ⊤) → ¬IsField R

Proof state:
case mpr
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (∃ I, ⊥ < I ∧ I < ⊤) → ¬IsField R

Tactic:
rintro ⟨I, bot_lt, lt_top⟩ hf

Result:
case mpr.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
⊢ False

Proof state:
case h
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
x : R
nz : x ≠ 0
nu : ¬IsUnit x
⊢ ⊥ < Ideal.span {x} ∧ Ideal.span {x} < ⊤

Tactic:
rw [bot_lt_iff_ne_bot, lt_top_iff_ne_top]

Result:
case h
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
x : R
nz : x ≠ 0
nu : ¬IsUnit x
⊢ Ideal.span {x} ≠ ⊥ ∧ Ideal.span {x} ≠ ⊤

Proof state:
case mpr.intro.intro.intro.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
hf : IsField R
x : R
mem : x ∈ I
ne_zero : ¬x = 0
y : R
lt_top : x * y ∉ I
hy : x * y = 1
⊢ False

Tactic:
exact lt_top (I.mul_mem_right _ mem)

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
⊢ False

Tactic:
obtain ⟨x, mem, ne_zero⟩ := SetLike.exists_of_lt bot_lt

Result:
case mpr.intro.intro.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
x : R
mem : x ∈ I
ne_zero : x ∉ ⊥
⊢ False

Proof state:
case mpr.intro.intro.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
x : R
mem : x ∈ I
ne_zero : ¬x = 0
⊢ False

Tactic:
obtain ⟨y, hy⟩ := hf.mul_inv_cancel ne_zero

Result:
case mpr.intro.intro.intro.intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
bot_lt : ⊥ < I
lt_top : I < ⊤
hf : IsField R
x : R
mem : x ∈ I
ne_zero : ¬x = 0
y : R
hy : x * y = 1
⊢ False