no goals
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.28305
f f₁ f₂ : Filter α
h h₁ h₂ : Set α → Set β
m : γ → β
l : Filter γ
⊢ Tendsto m l (Filter.lift' f h) ↔ ∀ (s : Set α), s ∈ f → ∀ᶠ (a : γ) in l, m a ∈ h s
simp only [Filter.lift', tendsto_lift, tendsto_principal, comp]