Is there a better (more direct or intuitive) proof for this proposition than I have come up with below? I am not sure whether it could be simiplified:
Let $G$ be a group with $H \leq G$. Then $K = \bigcap_{g \in G} gHg^{-1}$ is normal in $G$.
Let $a \in K$. Then $a \in gHg^{-1}$ for all $g \in G$. Therefore for all $g_1,g \in G$, $g_1ag_1^{-1} \in g_1gHg^{-1}g_1^{-1} = (g_1g)H(g_1g)^{-1}$ and so $g_1ag_1^{-1} \in K$ since $g_1g \in G$. Then $K$ is normal in $G$.
On
This is not much different in essence, but emphasizes the other important definition of normal subgroup as kernel of homomorphism.
Consider the action of $G$ on the cosets of $H$ given by multiplication. This is a homomorphism $\phi$ from $G$ to the symmetric group on the set $G/H = \{ gH : g \in G \} = \{ \{ gh: h \in H \} : g \in G \}$. As such, it has a kernel $K$, those $k$ such that $kgH = gH$ for all $g \in G$. This is precisely the $k$ such that $kg = gh_g$ for some $h_g \in G$ dependent on $g$, that is $k = gh_g g^{-1} \in gHg^{-1}$. In other words, $\bigcap_{g\in G} gHg^{-1} = \ker(\phi)$.
For every $g\in G$, we have $$ gKg^{-1}=g\left(\bigcap_{g'\in G} g'Hg'^{-1}\right)g^{-1}=\bigcap_{g'\in G} gg'Hg'^{-1}g^{-1}=\bigcap_{g'\in G} gg'H(gg')^{-1} $$ $$ =\bigcap_{g'\in G}g'Hg'^{-1}=K. $$ Note that the less trivial step is the second one. It is due to the fact that $x\longmapsto gxg^{-1}$ is injective for $\supseteq$. The inclusion $\subseteq$ is straightforward.