no goals
ι : Type ?u.47181
ι' : Type ?u.47184
α : Type u_2
β : Type u_1
γ : Type ?u.47193
inst✝ : Preorder β
m : α → β
f : Filter α
⊢ Tendsto m f atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a
simp only [atTop, tendsto_iInf, tendsto_principal, mem_Ici]