α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : Semiring R
P : Ideal R
hmax : ∀ (m : Ideal R), P < m → ¬IsMaximal m
J : Ideal R
hPJ : P < J
hnonmax : ¬J = ⊤
⊢ False
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : Semiring R
P : Ideal R
hmax : ∀ (m : Ideal R), P < m → ¬IsMaximal m
J : Ideal R
hPJ : P < J
⊢ J = ⊤
by_contra hnonmax
case intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : Semiring R
P : Ideal R
hmax : ∀ (m : Ideal R), P < m → ¬IsMaximal m
J : Ideal R
hPJ : P < J
hnonmax : ¬J = ⊤
M : Ideal R
hM1 : IsMaximal M
hM2 : J ≤ M
⊢ False
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : Semiring R
P : Ideal R
hmax : ∀ (m : Ideal R), P < m → ¬IsMaximal m
J : Ideal R
hPJ : P < J
hnonmax : ¬J = ⊤
⊢ False
rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩
no goals
case intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : Semiring R
P : Ideal R
hmax : ∀ (m : Ideal R), P < m → ¬IsMaximal m
J : Ideal R
hPJ : P < J
hnonmax : ¬J = ⊤
M : Ideal R
hM1 : IsMaximal M
hM2 : J ≤ M
⊢ False
exact hmax M (lt_of_lt_of_le hPJ hM2) hM1