Solution (source code)

= Solution

Define
$$
\mathfrak h=\{X\in\mathfrak g:\exp(tX)\in H\text{ for every }t\in\mathbb R\}.
$$
It contains zero, and $X\in\mathfrak h$ implies $aX\in\mathfrak h$ for every real scalar $a$, by replacing $t$ with $at$.

For $X,Y\in\mathfrak h$, we prove closure under addition using the <Lie product formula in a Lie group>. In the <local exponential chart>, let $Z(s)=\log(\exp(sX)\exp(sY))$. Smooth multiplication has differential $(U,V)\mapsto U+V$ at the identity, so <Taylor's theorem> gives
$$
Z(s)=s(X+Y)+O(s^2).
$$
For each fixed real $t$ and all sufficiently large positive <integers> $m$,
$$
\left[\exp(tX/m)\exp(tY/m)\right]^m=\exp\bigl(mZ(t/m)\bigr)
\longrightarrow\exp(t(X+Y)).
$$
Every term belongs to $H$, and $H$ is closed, proving $X+Y\in\mathfrak h$. Thus $\mathfrak h$ is a real <vector subspace>. It is also closed: if $X_j\to X$ with $X_j\in\mathfrak h$, continuity of the <Exponential map of a Lie group> gives $\exp(tX)\in H$ for each $t$.

For the <Lie bracket>, use the <Adjoint representation of a Lie group>. Conjugating a <one-parameter subgroup> gives
$$
\exp(sX)\exp(tY)\exp(-sX)=\exp\bigl(t\operatorname{Ad}_{\exp(sX)}Y\bigr)\in H.
$$
Consequently $\operatorname{Ad}_{\exp(sX)}Y\in\mathfrak h$. For $s\ne0$, linearity puts $\bigl(\operatorname{Ad}_{\exp(sX)}Y-Y\bigr)/s$ in $\mathfrak h$. Its limit as $s\to0$ is $\operatorname{ad}_XY=[X,Y]$. Closedness of $\mathfrak h$ therefore gives $[X,Y]\in\mathfrak h$, proving that the <Lie algebra of a closed subgroup> is a <Lie subalgebra> of $\mathfrak g$.