[GOAL]
P : Type u_1
inst✝ : Preorder P
x y : P
F s t : PFilter P
p q : P
⊢ principal q ≤ principal p ↔ p ≤ q
[PROOFSTEP]
simp
[GOAL]
P : Type u_1
inst✝ : CompleteSemilatticeInf P
F✝ : PFilter P
x : P
F : (PFilter P)ᵒᵈ
⊢ (fun x => ↑toDual (principal x)) x ≤ F ↔ x ≤ (fun F => sInf ↑(↑ofDual F)) F
[PROOFSTEP]
simp
[GOAL]
P : Type u_1
inst✝ : CompleteSemilatticeInf P
F✝ : PFilter P
x : P
F : (PFilter P)ᵒᵈ
⊢ ↑toDual (principal x) ≤ F ↔ ∀ (b : P), b ∈ ↑ofDual F → x ≤ b
[PROOFSTEP]
rfl
