no goals
α : Type u_1
β : Type u_2
γ : Type ?u.130759
ι : Type ?u.130762
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 → u x ≤ a}
⊢ ∀ (x : β), (q x → u x ≤ a) → p x → u x ≤ a
tauto