no goals
ι : Sort ?u.23236
α : Type ?u.23239
β : Type ?u.23242
X : Type u_1
Y : Type ?u.23248
inst✝ : TopologicalSpace X
x : X
⊢ (⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 s) = comap 𝓝 (𝓝 (𝓝 x))
simp (config := { contextual := true }) only [nhds_nhds, comap_iInf, comap_principal,
  Iic_principal, preimage_setOf_eq, ← mem_interior_iff_mem_nhds, setOf_mem_eq,
  IsOpen.interior_eq]