no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.313910
ι : Sort x
f : α → β
x : Filter α
y₁ y₂ : Filter β
⊢ Tendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂
simp only [Tendsto, le_inf_iff, iff_self_iff]