no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι✝ : Sort ?u.143260
ι : Sort u_1
u : ι → UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a
simp only [@nhds_eq_comap_uniformity _ (iInf u), nhds_iInf,
iInf_uniformity, @nhds_eq_comap_uniformity _ (u _), comap_iInf]