theorem HerzogSchonheim.subgroup_eq_top_of_singleton_cover {G : Type u_1} [Group G] {ι : Type u_2} (i : ι) (H : ι → Subgroup G) (g : ι → G) (hcover : IsCosetCover {i} H g) : H i = ⊤

If a single listed coset covers the whole group, the corresponding subgroup is ⊤.