no goals
α : Type u_1
β : Type u_2
γ : Type ?u.132666
ι : Type ?u.132669
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
h : ∀ (x : β), p x → q x
a : α
ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → a ≤ u x}
⊢ ∀ (x : β), (q x → a ≤ u x) → p x → a ≤ u x
tauto