P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ False
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
⊢ ¬x ∈ I
intro hx
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ ⊤ ∈ I
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ False
apply hI.top_not_mem
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
ht : x ⊔ xᶜ ∈ I
⊢ ⊤ ∈ I
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ ⊤ ∈ I
have ht : x ⊔ xᶜ ∈ I := sup_mem ‹_› ‹_›
no goals
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
ht : x ⊔ xᶜ ∈ I
⊢ ⊤ ∈ I
rwa [sup_compl_eq_top] at ht