no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.217823
ι : Sort x
inst✝ : SemilatticeSup β
l : Filter α
f g h : α → β
hf : f ≤ᶠ[l] h
hg : g ≤ᶠ[l] h
⊢ f ⊔ g ≤ᶠ[l] h
filter_upwards [hf, hg] with x hfx hgx using _root_.sup_le hfx hgx