A lemma of B. H. Neumann.

[bustercopley]

Let the group $G$ be the union of finitely many, let us say $n$, left cosets of subgroups $C₁$, $C₂$, ..., $Cₙ$: $$G = ⋃_{i = 1}^n C_i g_i.$$ Then the index of (at least) one of these subgroups does not exceed $n$.

---

Suggested by @alreadydone Zulip

[Rida-Hamadani]

Run scripts/mk_all.sh in your terminal then commit again.

[bustercopley]

Moved to #13047