α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : Ideal.IsMaximal M
not_field : ¬IsField R
h : M = ⊥
⊢ False
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : Ideal.IsMaximal M
not_field : ¬IsField R
⊢ M ≠ ⊥
rintro h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : Ideal.IsMaximal ⊥
not_field : ¬IsField R
h : M = ⊥
⊢ False
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : Ideal.IsMaximal M
not_field : ¬IsField R
h : M = ⊥
⊢ False
rw [h] at max
case mk.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
not_field : ¬IsField R
h : M = ⊥
_h1 : ⊥ ≠ ⊤
h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤
⊢ False
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
max : Ideal.IsMaximal ⊥
not_field : ¬IsField R
h : M = ⊥
⊢ False
rcases max with ⟨⟨_h1, h2⟩⟩
case mk.intro.intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
not_field : ¬IsField R
h : M = ⊥
_h1 : ⊥ ≠ ⊤
h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤
I : Ideal R
hIbot : ⊥ < I
hItop : I < ⊤
⊢ False
case mk.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
not_field : ¬IsField R
h : M = ⊥
_h1 : ⊥ ≠ ⊤
h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤
⊢ False
obtain ⟨I, hIbot, hItop⟩ := not_isField_iff_exists_ideal_bot_lt_and_lt_top.mp not_field
no goals
case mk.intro.intro.intro
α : Type u
β : Type v
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
M : Ideal R
not_field : ¬IsField R
h : M = ⊥
_h1 : ⊥ ≠ ⊤
h2 : ∀ (b : Ideal R), ⊥ < b → b = ⊤
I : Ideal R
hIbot : ⊥ < I
hItop : I < ⊤
⊢ False
exact ne_of_lt hItop (h2 I hIbot)