no goals
α : Type u
β : Type v
γ : Type ?u.196613
δ : Type ?u.196616
ε : Type ?u.196619
ζ : Type ?u.196622
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.196633
inst✝¹ : TopologicalSpace α
inst✝ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
a : (i : ι) → π i
⊢ 𝓝 a = Filter.pi fun i => 𝓝 (a i)
simp only [nhds_iInf, nhds_induced, Filter.pi]