A group $G$ with a subgroup $H$ of index $n$ has a normal subgroup $K\subset H$ whose index in $G$ divides $n!$

I would be very thankful if someone could give me a hint with proving this. It's a very common exercise in abstract algebra textbooks.

If $G$ is a group with a subgroup $H$ of finite index $n$, then $G$ has a normal subgroup $K$ contained in $H$ whose index in $G$ is finite and divides $n!$.

I found the proof on this Wikipedia page at some point (although the proof appears to be no longer there), but I got lost in one of the details.

The proof is really simple. Let $X$ be the set of left cosets of $H$. Consider $\phi: G \to \text{Sym}(X)$ given by $\phi(x)(aH)=(xa)H$. Then $\phi$ is a homomorphism. Consider now $K=\ker \phi$. Then $K$ is a normal subgroup of $G$ contained in $H$. Finally, $G/K$ is isomorphic to a subgroup of $\text{Sym}(X)$, which has order $n!$, where $n=[G:H]$. Thus, $[G:K]$ is finite and divides $n!$.

A stronger result to the one in the question is the following. A characteristic subgroup is one which is fixed (setwise) by all automorphisms of $G$. Characteristic subgroups are normal (as conjugation corresponds to inner automorphisms).

Theorem. Let $G$ be a finitely generated group, with generating set of size $m$. There exists a characteristic subgroup of index $n^{(n!)^{m}}$ in $G$.

We start our proof with two lemmas.

Lemma 1. Let $G$ be a finitely generated group, with generating set of size $m$. Then $G$ has at most $(n!)^m$ subgroups of index $n<\infty$.

Proof. Firstly note that by lhf's answer, every subgroup $K$ of index $n$ corresponds to a map $\phi_K: G\rightarrow \operatorname{Sym}(G/K)\cong S_n$. Now, if $K_1\neq K_2$ then $\phi_{K_1}\neq\phi_{K_2}$, and to see this consider $x\in K_1$ but $x\not\in K_2$. Then $\phi_{K_1}(x)(K_1)=xK_1=K_1$, so $\phi_{K_1}(x)$ corresponds to the identity of $S_n$, but $\phi_{K_2}(x)(K_2)=xK_2\neq K_2$, and so $\phi_{K_2}(x)$ is not the identity.

Such a map $\phi_K$ is defined by the image of the $m$ generators of $G$. There are $n!$ choices for each generator, and so there are at most $(n!)^m$ maps $\phi_K$. By the above, no two maps define the same subgroup, and so there are at most $(n!)^m$ subgroups $K$ of index $n$. QED

Lemma 2. If $H, K$ are finite index subgroups of a group $G$ then $H\cap K$ has finite index, and indeed $|G:H\cap K|\leq |G:H|\cdot |G:K|$.

Proof. Let $L=H\cap K$ and let $a\in Lb$ where $Lb$ is one of your finite number of cosets. Then $ab^{-1}\in L\Rightarrow a\in Hb\cap Kb\Rightarrow Lb\leq Hb\cap Kb$. Clearly $Lb\leq Hb\cap Kb$, so $Hb\cap Lb=Db$. Thus, the number of cosets of $L$ is $\leq |G:H|\cdot |G:K|$ as required. QED

We can now prove the theorem.

Proof of Theorem. By combining Lemmas 1 and 2, intersecting all subgroups of a fixed index $n$ will give you a subgroup of order $\text{index}^{\text{# subgroups}}\leq n^{(n!)^{m}}$. Moreover, this subgroup is characteristic, because automorphisms fix the index of subgroups. That is, if $\phi$ is an automorphism of $G$ then $|G:H|=|G:\phi(H)|$. So, $\cap \phi(H_i)=\cap H_i$ so your group is fixed by all automorphisms. QED

An application. The following application of the above is a theorem of Gilbert Baumslag from 1963. It is quite unusual, as it is surprising (residual finiteness is usually very hard to prove), and it has a very short proof (the paper is a page-and-a-half long, and contains three applications of this result. The half-page is all references.)

Theorem. If $G$ is a finitely generated residually finite group then $\operatorname{Aut}(G)$ is residually finite.

A group is residually finite if for any element $g\in G$ there exists a homomorphism onto a finite group $F$, $\phi: G\rightarrow F$ say, such that $g\phi\neq 1$. This is a very strong finiteness condition. Equivalently, all the finite index subgroups intersect trivially (we proved above that finitely many intersect with finite index, but there are infinitely many in general so this makes sense).

Proof. Let $1\neq \alpha\in \operatorname{Aut(G)}$. Then there exists $g\in G$ such that $\alpha(g)\neq g$ and write $h=\alpha(g)g^{-1} (\neq 1)$. As the finite index subgroups intersect non-trivially, there is a finite index subgroup of $G$ not containing $h$, $K$ say. One can take this to be characteristic, by intersecting all subgroups of that index, as above (if $h\not\in A$ then $h\not\in A\cap B$ whatever $B$ is). Now, $\operatorname{Aut(G)}$ induces a finite group ($A\cong \operatorname{Aut(G)}/L$) of automorphism of $G/K$, as $G/K$ if finite and $K$ is characteristic. As $h\not\in K$ we have that $\alpha$ induces a non-trivial automorphism of $G/K$, so $\alpha\not\in L$, and so $\operatorname{Aut(G)}$ is residually finite, as required. QED

Grossman extended this result to $\operatorname{Out}(G)$ (Grossman, Edna K. "On the residual finiteness of certain mapping class groups." Journal of the London Mathematical Society 2.1 (1974): 160-164.).