Existence of an open normal subgroup in any clopen neighborhood of the neutral element

This file proves the lemma TopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhd_of_one, which states that in a compact topological group, for any clopen neighborhood of 1, there exists an open normal subgroup contained within it.

This file is split out from the file OpenSubgroup because it needs more imports.

theorem TopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhd_of_one {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 1 ∈ W) : ∃ (H : OpenNormalSubgroup G), ↑H ⊆ W