no goals
α : Type u_1
β : Type u_2
γ : Type ?u.40673
ι : Type ?u.40676
inst✝ : SemilatticeSup α
f : Filter β
u v : β → α
bu : α
hu : ∀ᶠ (x : β) in f, u x ≤ bu
bv : α
hv : ∀ᶠ (x : β) in f, v x ≤ bv
⊢ ∀ᶠ (x : β) in f, u x ⊔ v x ≤ bu ⊔ bv
filter_upwards [hu, hv]with _ using sup_le_sup