theorem HerzogSchonheim.herzog_schoenheim_conjecture {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (H : ι → Subgroup G) (g : ι → G) : IsDisjointCosetCover s H g → ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ (H i).index = (H j).index

Herzog-Schoenheim conjecture: in a finite disjoint cover of a group by left cosets of subgroups, two distinct cosets must come from subgroups of equal index.