P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ ∀ {x y : P}, x ⊓ y ∈ I → ¬x ∈ I → y ∈ I
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ IsPrime I
simp only [isPrime_iff_mem_or_mem, or_iff_not_imp_left]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
⊢ y ∈ I
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ ∀ {x y : P}, x ⊓ y ∈ I → ¬x ∈ I → y ∈ I
intro x y hxy hxI
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
hxcI : xᶜ ∈ I
⊢ y ∈ I
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
⊢ y ∈ I
have hxcI : xᶜ ∈ I := h.resolve_left hxI
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
hxcI : xᶜ ∈ I
ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I
⊢ y ∈ I
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
hxcI : xᶜ ∈ I
⊢ y ∈ I
have ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I := sup_mem hxy (I.lower inf_le_right hxcI)
no goals
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
hxcI : xᶜ ∈ I
ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I
⊢ y ∈ I
rwa [inf_comm, sup_inf_inf_compl] at ass