∀ {Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [inst : (i : Fin (n + 1)) → TopologicalSpace (A i)]
  {f : Y → (j : Fin (n + 1)) → A j} {l : Filter Y} {x : (j : Fin (n + 1)) → A j},
  Filter.Tendsto f l (nhds x) → Filter.Tendsto (fun a => Fin.tail (f a)) l (nhds (Fin.tail x))