Herzog–Schönheim conjecture

The actual formalization is in FormalConjectures.ErdosProblems.«274».

References:

• Wikipedia
• arXiv:1803.08301
• arXiv:1803.03569
• PMC7247885
• arXiv:1804.11103

theorem HerzogSchonheimConjecture.herzog_schonheim_conjecture {G : Type u_1} [Group G] (hG : 1 < ENat.card G) {ι : Type u_2} [Fintype ι] (hι : 1 < Fintype.card ι) (P : Erdos274.Group.ExactCovering G ι) : ∃ (i : ι) (j : ι), i ≠ j ∧ (P.parts i).index = (P.parts j).index