Pullback metric on a cover of a complete manifold is complete

The pullback is a Riemannian metric and $\pi$ is a local isometry. [F1, given] Since $\pi$ is a local diffeomorphism, $d{\pi }_x$ is injective for every $x\in N$, so the radical $\ker d{\pi }_x$ of [F1] is trivial and [F1] makes ${\pi }^{\ast }g$ a Riemannian metric on $N$. By the definition of the pullback, $({\pi }^{\ast }g{)}_x(v,w)=g_{\pi (x)}(d{\pi }_{x}v,d{\pi }_{x}w)$ for all $v,w\in T_{x}N$; since $\pi$ is also a local diffeomorphism, it is a local isometry from $(N,{\pi }^{\ast }g)$ to $(M,g)$ in the sense of [F2]. In dimension $n=0$ both manifolds have discrete points and the empty bilinear form is positive definite, so the claim holds vacuously; if $N$ is empty then so is $M$ (as $\pi$ is surjective), and both statements are vacuous.

Geodesics of $N$ project to geodesics of $M$. Let $\gamma :I\to N$ be an affinely parametrized geodesic of $(N,{\pi }^{\ast }g)$ and put $\sigma :=\pi \circ \gamma$. Since $\pi$ is the identity map of the metric in the sense of step 1.1, [F2] applied to the field $W=\dot{\gamma }$ gives $D_t^M\dot{\sigma }=D_t^M(d{\pi }_{\gamma (t)}\dot{\gamma }(t))=d{\pi }_{\gamma (t)}(D_t^N\dot{\gamma }(t))=0,$ so $\sigma$ is an affinely parametrized geodesic of $(M,g)$.

Local lifts of geodesics are geodesics. Conversely, let $\sigma :J\to M$ be an affinely parametrized geodesic and let $\gamma :J\to N$ be a smooth curve with $\pi \circ \gamma =\sigma$. Applying [F2] to $W=\dot{\gamma }$ and using $D_t^M\dot{\sigma }=0$ gives $d{\pi }_{\gamma (t)}(D_t^N\dot{\gamma }(t))=D_t^M\dot{\sigma }(t)=0$ for all $t$; since $d\pi$ is injective at every point (step 1.1 and the local-diffeomorphism hypothesis), $D_t^N\dot{\gamma }=0$ and $\gamma$ is a geodesic of $(N,{\pi }^{\ast }g)$. In particular every path lift of a geodesic of $M$ is a geodesic of $N$.

Maximal geodesics of the complete base. Since $(M,g)$ is complete, [F4] and [F5] say that every maximal geodesic of $M$ is defined on all of $\mathbb{R}$: given $q\in M$ and $u\in T_{q}M$, the unique maximal geodesic with initial data $(q,u)$ — which exists by [F5] — has domain $\mathbb{R}$ by the equivalence of [F4] applied to the complete manifold. This is the only place where completeness of $M$ enters.

Extending a maximal geodesic of $N$ to an $M$-geodesic on all of $\mathbb{R}$. Let $\gamma :I\to N$ be a maximal geodesic of $(N,{\pi }^{\ast }g)$; maximality is with respect to the maximal-geodesic convention of [F5], and $0\in I$ with $I$ an open interval. By step 2.1, ${\sigma }_0:=\pi \circ \gamma$ is a geodesic of $M$ on $I$; it is the restriction of the unique maximal $M$-geodesic $\sigma$ with the initial data $\sigma (0)=\pi (\gamma (0))$ and $\dot{\sigma }(0)=d{\pi }_{\gamma (0)}\dot{\gamma }(0)$, whose domain is $\mathbb{R}$ by step 4.1. Now lift the path $\sigma :\mathbb{R}\to M$ through the covering $\pi$ with initial point $\gamma (0)$: by [F3] there is a unique path $\tilde{\gamma }:\mathbb{R}\to N$ with $\pi \circ \tilde{\gamma }=\sigma$ and $\tilde{\gamma }(0)=\gamma (0)$.

The lift is a geodesic agreeing with $\gamma$, so $N$ is geodesically complete. Since $\pi \circ \tilde{\gamma }=\sigma$ is smooth and $\pi$ is a local diffeomorphism, $\tilde{\gamma }$ is smooth; being a path lift of the geodesic $\sigma$, it is a geodesic of $(N,{\pi }^{\ast }g)$ by step 3.1. On the interval $I$ both $\tilde{\gamma }$ and $\gamma$ are paths in $N$ covering the same path $\sigma {\mathrm{\mid }}_I$ and both start at $\gamma (0)$; by the uniqueness clause of [F3], $\tilde{\gamma }{\mathrm{\mid }}_I=\gamma$. Hence the maximal geodesic $\gamma$ of $N$ is the restriction of the geodesic $\tilde{\gamma }$ defined on $\mathbb{R}$, and by the maximality convention of [F5] its domain is $I=\mathbb{R}$. Therefore every maximal geodesic of $(N,{\pi }^{\ast }g)$ has domain $\mathbb{R}$: the manifold $(N,{\pi }^{\ast }g)$ is geodesically complete, and [F4] applied to the nonempty connected manifold $N$ makes it complete as a metric space. This proves both assertions.

Boundary and choice audit. Every hypothesis is used where it is needed: the local-diffeomorphism hypothesis is exactly what makes ${\pi }^{\ast }g$ positive definite in step 1.1 and makes the projected covariant derivative vanish in step 3.1; surjectivity of $\pi$ keeps $N$ nonempty when $M$ is; and completeness of $M$ is used only in step 4.1 through Hopf–Rinow. The geodesic-completeness definition of [F5] includes the zero initial vector, and the zero vector case is also covered by steps 2.1 and 3.1 (constant geodesics project to constant geodesics and lift to constant geodesics). In dimension zero every constant map is a geodesic and both completeness notions hold, so the argument is a special case of the same steps. No step selects a family of curves: the unique lift is produced by [F3] and the unique maximal geodesic by [F5]. Exactly [A1] is inherited and no further choice is spent.