no goals
ι : Type ?u.47838
ι' : Type ?u.47841
α : Type u_2
β : Type u_1
γ : Type ?u.47850
inst✝ : Preorder β
l : Filter α
f₁ f₂ : α → β
h : f₁ ≤ᶠ[l] f₂
h₁ : Tendsto f₁ l atTop
b : β
⊢ ∀ᶠ (a : α) in l, b ≤ f₂ a
filter_upwards [tendsto_atTop.1 h₁ b, h] with x using le_trans