no goals
α✝ : Type u
β : Type v
γ : Type u_2
δ : Type ?u.37506
ε : Type ?u.37509
ζ : Type ?u.37512
inst✝⁵ : TopologicalSpace α✝
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
α : Type u_1
seq : α → β × γ
f : Filter α
x : β × γ
⊢ Tendsto seq f (𝓝 x) ↔ Tendsto (fun n => (seq n).fst) f (𝓝 x.fst) ∧ Tendsto (fun n => (seq n).snd) f (𝓝 x.snd)
rw [nhds_prod_eq, Filter.tendsto_prod_iff']