∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : CompactSpace G] [inst_3 : ContinuousAdd G]
  (H : OpenNormalAddSubgroup G),
  H.toFiniteIndexNormalAddSubgroup = FiniteIndexNormalAddSubgroup.ofAddSubgroup ↑H.toOpenAddSubgroup