P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
⊢ ¬x ∈ I ∧ ¬y ∈ I → ¬x ⊓ y ∈ I
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
contrapose!
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
F : PFilter P := IsPFilter.toPFilter (_ : IsPFilter (↑Iᶜ))
⊢ ¬x ∈ I ∧ ¬y ∈ I → ¬x ⊓ y ∈ I
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
⊢ ¬x ∈ I ∧ ¬y ∈ I → ¬x ⊓ y ∈ I
let F := hI.compl_filter.toPFilter
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
F : PFilter P := IsPFilter.toPFilter (_ : IsPFilter (↑Iᶜ))
⊢ x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
F : PFilter P := IsPFilter.toPFilter (_ : IsPFilter (↑Iᶜ))
⊢ ¬x ∈ I ∧ ¬y ∈ I → ¬x ⊓ y ∈ I
show x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
no goals
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
F : PFilter P := IsPFilter.toPFilter (_ : IsPFilter (↑Iᶜ))
⊢ x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
exact fun h => inf_mem h.1 h.2