α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I J : Ideal α
⊢ I ≤ J ∧ ¬J ≤ I → J = ⊤ ↔ ∀ (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I J : Ideal α
⊢ I < J → J = ⊤ ↔ ∀ (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
rw [lt_iff_le_not_le]
no goals
α : Type u
β : Type v
inst✝ : Semiring α
I✝ : Ideal α
a b : α
I J : Ideal α
⊢ I ≤ J ∧ ¬J ≤ I → J = ⊤ ↔ ∀ (x : α), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
exact
  ⟨fun H x h hx₁ hx₂ => J.eq_top_iff_one.1 <| H ⟨h, not_subset.2 ⟨_, hx₂, hx₁⟩⟩,
    fun H ⟨h₁, h₂⟩ =>
    let ⟨x, xJ, xI⟩ := not_subset.1 h₂
    J.eq_top_iff_one.2 <| H x h₁ xI xJ⟩