no goals
α : Type u_1
β : Type ?u.4061
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
l : List α
⊢ 𝓝 (a :: l) = Seq.seq (List.cons <$> 𝓝 a) fun x => 𝓝 l
rw [nhds_list, List.traverse_cons _, ← nhds_list]