case inl
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)
cases subsingleton_or_nontrivial R
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (¬∃ I, ⊥ < I ∧ I < ⊤) ↔ ¬¬IsSimpleOrder (Ideal R)
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)
rw [← not_iff_not, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top, ← not_iff_not]
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), ⊥ < I → ¬I < ⊤) ↔ IsSimpleOrder (Ideal R)
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (¬∃ I, ⊥ < I ∧ I < ⊤) ↔ ¬¬IsSimpleOrder (Ideal R)
push_neg
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder (Ideal R)
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), ⊥ < I → ¬I < ⊤) ↔ IsSimpleOrder (Ideal R)
simp_rw [lt_top_iff_ne_top, bot_lt_iff_ne_bot, ← or_iff_not_imp_left, not_ne_iff]
no goals
case inr
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder (Ideal R)
exact ⟨fun h => ⟨h⟩, fun h => h.2⟩
no goals
case inl
α : Type u
β : Type v
R : Type u_1
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)
exact
  ⟨fun h => (not_isField_of_subsingleton _ h).elim, fun h =>
    (false_of_nontrivial_of_subsingleton <| Ideal R).elim⟩