-- Mathlib/RingTheory/Ideal/Basic.lean
theorem bot_lt_of_maximal (M : Ideal R) [hm : M.IsMaximal] (non_field : ¬IsField R) : ⊥ < M

Proof state:
case intro.intro.right
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
⊢ False

Tactic:
apply lt_irrefl (⊤ : Ideal R)

Result:
case intro.intro.right
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
⊢ ⊤ < ⊤

Proof state:
case intro.intro.right
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ¬↑M ⊆ ↑⊥

Tactic:
intro mle

Result:
case intro.intro.right
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
⊢ False

Proof state:
case intro.intro.right
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
this : M = ⊥
⊢ ⊤ < ⊤

Tactic:
rw [← this] at Ibot

Result:
case intro.intro.right
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : M < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
this : M = ⊥
⊢ ⊤ < ⊤

Proof state:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
⊢ ⊥ < M

Tactic:
rcases Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top.1 non_field with ⟨I, Ibot, Itop⟩

Result:
case intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ⊥ < M

Proof state:
case intro.intro
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ⊥ < M

Tactic:
constructor

Result:
case intro.intro.left
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ↑⊥ ⊆ ↑M

case intro.intro.right
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ¬↑M ⊆ ↑⊥

Proof state:
case intro.intro.right
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
⊢ ⊤ < ⊤

Tactic:
have : M = ⊥ := eq_bot_iff.mpr mle

Result:
case intro.intro.right
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
this : M = ⊥
⊢ ⊤ < ⊤

Proof state:
case intro.intro.left
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ↑⊥ ⊆ ↑M

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.right
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
hm : M.IsMaximal
non_field : ¬IsField R
I : Ideal R
Ibot : M < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
this : M = ⊥
⊢ ⊤ < ⊤

Tactic:
rwa [hm.1.2 I Ibot] at Itop

Result:
no goals