no goals
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.12537
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
m : γ → β
l : Filter γ
⊢ Tendsto m l (Filter.lift f g) ↔ ∀ (s : Set α), s ∈ f → Tendsto m l (g s)
simp only [Filter.lift, tendsto_iInf]