no goals
ι : Type ?u.266753
ι' : Type ?u.266756
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ b, c ≤ e b
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop
rw [← comap_embedding_atTop hm hu, tendsto_comap_iff]