Lie's second fundamental theorem

The graph ${\mathrm{\Gamma }}_{\varphi }=\{(X,\varphi X):X\in \mathrm{Lie}(G)\}$ is a Lie subalgebra of $\mathrm{Lie}(G\times H)$. By [L1] it integrates to a connected immersed subgroup $K\to G\times H$. Projection $p:K\to G$ has identity differential $(X,\varphi X)\mapsto X$, an isomorphism, so it is a local diffeomorphism at the identity and therefore everywhere by translation. Its image is an open subgroup of connected $G$, hence all of $G$.

A surjective local-diffeomorphism homomorphism is a covering: choose an identity neighborhood on which it is a diffeomorphism and shrink it so that distinct kernel translates are disjoint; translating gives evenly covered neighborhoods. The Lie group $G$ is locally path-connected, so [L3], connectedness of $K$, and simple connectedness [L2] make this covering one-sheeted; hence $p$ is a Lie-group isomorphism. Define $F$ as the second projection composed with $p^{-1}$. Its graph is $K$, and its identity differential is $\varphi$.

If $F_1,F_2:G\to H$ have differential $\varphi$, their graphs are connected immersed subgroups of $G\times H$ with Lie algebra ${\mathrm{\Gamma }}_{\varphi }$. Uniqueness in [L1] makes the two immersed images equal; projection to $G$ then forces $F_1=F_2$. This also handles $G$ or $H$ zero-dimensional. Countable choice is used exactly through [L1]'s maximal-leaf construction; all other neighborhood selections are finite.