case intro.intro
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ⊥ < M
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
⊢ ⊥ < M
rcases Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top.1 non_field with ⟨I, Ibot, Itop⟩
case intro.intro.left
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ↑⊥ ⊆ ↑M

case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ¬↑M ⊆ ↑⊥
case intro.intro
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ⊥ < M
constructor
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
⊢ False
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ¬↑M ⊆ ↑⊥
intro mle
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
⊢ ⊤ < ⊤
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
⊢ False
apply lt_irrefl (⊤ : Ideal R)
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
this : M = ⊥
⊢ ⊤ < ⊤
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
⊢ ⊤ < ⊤
have : M = ⊥ := eq_bot_iff.mpr mle
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : M < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
this : M = ⊥
⊢ ⊤ < ⊤
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
this : M = ⊥
⊢ ⊤ < ⊤
rw [←this] at Ibot
no goals
case intro.intro.right
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : M < I
Itop : I < ⊤
mle : ↑M ⊆ ↑⊥
this : M = ⊥
⊢ ⊤ < ⊤
rwa [hm.1.2 I Ibot] at Itop
no goals
case intro.intro.left
α : Type u
β : Type v
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
M : Ideal R
hm : IsMaximal M
non_field : ¬IsField R
I : Ideal R
Ibot : ⊥ < I
Itop : I < ⊤
⊢ ↑⊥ ⊆ ↑M
simp