α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
⊢ (I = ⊤ ∨ ∃ x x_1 h, ¬x ∈ I ∧ ¬x_1 ∈ I) ↔ I = ⊤ ∨ ∃ x _hx y _hy, x * y ∈ I
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
⊢ ¬IsPrime I ↔ I = ⊤ ∨ ∃ x _hx y _hy, x * y ∈ I
simp_rw [Ideal.isPrime_iff, not_and_or, Ne.def, Classical.not_not, not_forall, not_or]
no goals
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I : Ideal α
⊢ (I = ⊤ ∨ ∃ x x_1 h, ¬x ∈ I ∧ ¬x_1 ∈ I) ↔ I = ⊤ ∨ ∃ x _hx y _hy, x * y ∈ I
exact
  or_congr Iff.rfl
    ⟨fun ⟨x, y, hxy, hx, hy⟩ => ⟨x, hx, y, hy, hxy⟩, fun ⟨x, hx, y, hy, hxy⟩ =>
      ⟨x, y, hxy, hx, hy⟩⟩