P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
h : xᶜ ∈ I → ¬x ∈ I
⊢ ¬x ∈ I ∨ ¬xᶜ ∈ I
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
⊢ ¬x ∈ I ∨ ¬xᶜ ∈ I
have h : xᶜ ∈ I → x ∉ I := hI.not_mem_of_compl_mem
no goals
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
h : xᶜ ∈ I → ¬x ∈ I
⊢ ¬x ∈ I ∨ ¬xᶜ ∈ I
tauto