A connected cover with a chosen lifted identity has a unique lifted Lie-group structure

Give $\tilde{G}$ the canonical smooth structure of [F1]. Its finite products are connected by [F5], and are locally path connected as products of manifold coordinate domains; hence they are path connected by [F6].

Consider the based map $f=m\circ (p\times p):({\tilde{G}}^2,(\tilde{e},\tilde{e}))\to (G,e)$. For a based loop $\gamma =(\alpha ,\beta )$ in ${\tilde{G}}^2$, [F4] gives $[f\circ \gamma ]=[p\circ \alpha ][p\circ \beta ]$. Both factors lie in the subgroup $p_{\ast }{\pi }_1(\tilde{G},\tilde{e})$, so their product does also. The criterion [F2] therefore supplies a unique based lift $\tilde{m}:{\tilde{G}}^2\to \tilde{G}$ satisfying $p(\tilde{m}(a,b))=p(a)p(b)$ and $\tilde{m}(\tilde{e},\tilde{e})=\tilde{e}$.

Similarly, the based map $a\mapsto p(a{)}^{-1}$ lifts to a unique based map $\stackrel{}{\mathrm{inv}}:\tilde{G}\to \tilde{G}$. Indeed, [F4] identifies the class of the pointwise inverse of $p\circ \alpha$ with $[p\circ \alpha {]}^{-1}$, which remains in the subgroup $p_{\ast }{\pi }_1(\tilde{G},\tilde{e})$.

The two maps $(a,b,c)\mapsto \tilde{m}(\tilde{m}(a,b),c)$ and $(a,b,c)\mapsto \tilde{m}(a,\tilde{m}(b,c))$ are lifts through $p$ of the same map $(a,b,c)\mapsto p(a)p(b)p(c)$, and they agree at $(\tilde{e},\tilde{e},\tilde{e})$. Their connected domain and [F3] give associativity. Likewise $a\mapsto \tilde{m}(\tilde{e},a)$, $a\mapsto \tilde{m}(a,\tilde{e})$, and $a\mapsto a$ are lifts of $p$ agreeing at $\tilde{e}$, so $\tilde{e}$ is a two-sided identity.

The maps $a\mapsto \tilde{m}(\stackrel{}{\mathrm{inv}}(a),a)$ and $a\mapsto \tilde{m}(a,\stackrel{}{\mathrm{inv}}(a))$ both project to the constant map with value $e$ and agree at $\tilde{e}$ with the constant map having value $\tilde{e}$. By [F3] they are that constant map, so $\stackrel{}{\mathrm{inv}}(a)$ is the two-sided inverse of $a$. Thus $(\tilde{G},\tilde{m},\stackrel{}{\mathrm{inv}},\tilde{e})$ is a group and $p$ is a group homomorphism.

The lifted maps are smooth. Around any source point choose a neighborhood whose image under a lift lies in one sheet over a smooth coordinate domain; there the lift is the composite of its smooth projection to $G$ with the smooth local inverse of $p$ supplied by [F1]. This applies to $\tilde{m}$ and $\stackrel{}{\mathrm{inv}}$, so the group is a Lie group and $p$ is a covering homomorphism.

Any other such Lie-group structure has the same smooth structure by [F1]. Its multiplication and inversion are based lifts of the two maps used in steps 2.1 and 2.2, so [F2] makes them equal to $\tilde{m}$ and $\stackrel{}{\mathrm{inv}}$. This proves uniqueness. Subgroup closure is the exact property used in steps 2.1 and 2.2, and uniqueness of based lifts supplies every group law. The only choice is the one explicitly chosen basepoint $\tilde{e}$; no choice principle is invoked.