∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] [FirstCountableTopology G]
  (N : Subgroup G) [inst_4 : N.Normal] [CompleteSpace G], CompleteSpace (G ⧸ N)