A complete local isometry is a covering map

$F$ is an open map. [F1, given] Let $O\subseteq N$ be open and let $x\in O$. By [F1] there are open neighbourhoods $W\subseteq O$ of $x$ and $W^{\mathrm{\prime }}$ of $F(x)$ such that $F{\mathrm{\mid }}_W:W\to W^{\mathrm{\prime }}$ is a diffeomorphism; then $F(W)\subseteq F(O)$ is an open neighbourhood of $F(x)$. Hence every point of $F(O)$ is interior, so $F(O)$ is open.

Naturality of the exponential map. [F2, F3, F4, given] For $x\in N$ and $w\in T_{x}N$, the curve $t\mapsto F({\exp }_x(tw))$ is an affinely parametrized geodesic of $M$ by [F2], with initial data $F(x)$ and $d{F}_{x}w$. The maximal geodesic of $M$ with those initial data is unique by [F3]. Since $N$ is complete, [F4] gives ${\mathcal{E}}_x=T_{x}N$, so ${\exp }_x(tw)$ is defined for every $t\in \mathbb{R}$; consequently $F({\exp }_x(tw))={\exp }_{F(x)}(td{F}_{x}w)$ for every $t$ for which the right-hand side is defined, and in particular for all $t$ with $\mathrm{\mid }t\mathrm{\mid }\le 1$ once $\mathrm{\mid }d{F}_{x}w\mathrm{\mid }$ is small enough that ${\exp }_{F(x)}$ is defined on the radial segment up to time $1$.

Geodesic lifting. [F1, F3, step 1.2] Let $\gamma :I\to M$ be an affinely parametrized geodesic, $t_0\in I$ and $p\in F^{-1}(\gamma (t_0))$. By [F1], $(d{F}_p{)}^{-1}$ is defined on the image of $d{F}_p$; put $w:=(d{F}_p{)}^{-1}\dot{\gamma }(t_0)$ and $\tilde{\gamma }(t):={\exp }_p((t-t_0)w)$. This is defined for all $t\in \mathbb{R}$ and is a geodesic of $N$ by [F4] and the definition of the exponential; by step 1.2 applied at $x=p$, $F(\tilde{\gamma }(t))={\exp }_{\gamma (t_0)}((t-t_0)\dot{\gamma }(t_0))=\gamma (t)$ for $t\in I$, the last equality by uniqueness of the geodesic with prescribed initial data [F3]. If ${\tilde{\gamma }}_1$ is any other geodesic lift of $\gamma$ with ${\tilde{\gamma }}_1(t_0)=p$, then $d{F}_p{\dot{\tilde{\gamma }}}_1(t_0)=\dot{\gamma }(t_0)=d{F}_{p}w$ and $d{F}_p$ is injective, so ${\dot{\tilde{\gamma }}}_1(t_0)=w$; uniqueness of the geodesic with initial data $(p,w)$ [F3] gives ${\tilde{\gamma }}_1=\tilde{\gamma }$. Thus geodesics lift uniquely through any point of the fibre and lift over the whole interval of definition.

$F$ is surjective. [F5, step 1.1, step 2.1] By step 1.1 the image $F(N)$ is open, and it is nonempty because $N$ is. If $F(N)\mathrm{\ne }M$, then since $M$ is connected and $F(N)$ is a nonempty proper open subset, $F(N)$ is not closed, so there is $p\in \overline{F(N)}\setminus F(N)$. By [F5] choose a normal neighbourhood $U_p={\exp }_p(V)$ of $p$; since $p$ is a limit point of $F(N)$, and $U_p$ is a neighbourhood of $p$, there is $q\in F(N)\cap U_p$, say $q={\exp }_p(v)$ with $v\in V$. The radial curve $\gamma (t):={\exp }_p(tv)$, $t\in [0,1]$, is an affinely parametrized geodesic from $p$ to $q$ by [F5]. Choose $p_0\in F^{-1}(q)$, which exists because $q\in F(N)$, and lift $\gamma$ through $p_0$ by step 2.1; the lift is defined on $[0,1]$, so $p=\gamma (0)=F(\tilde{\gamma }(0))$ lies in $F(N)$, a contradiction. Hence $F(N)=M$.

The sheets over a normal ball. Fix $q\in M$ and a normal neighbourhood $U={\exp }_q(V)$ as in [F5], with $V$ star-shaped, ${\exp }_q:V\to U$ a diffeomorphism. For $y\in U$ write $v_y:={\exp }_q^{-1}(y)\in V$ and let ${\gamma }_y(t):={\exp }_q(t{v}_y)$ for $t\in [0,1]$, a geodesic from $q$ to $y$ by [F5]. For $p\in F^{-1}(q)$ define ${\phi }_p:U⟶N,{\phi }_p(y):={\exp }_p((d{F}_p{)}^{-1}{v}_y),$ the endpoint of the unique geodesic lift of ${\gamma }_y$ through $p$ furnished by step 2.1. Then: (i) $F\circ {\phi }_p={\mathrm{id}}_U$: this is step 1.2 applied to $x=p$ and $w=(d{F}_p{)}^{-1}{v}_y$ together with the lift identity $F({\exp }_p(\cdot ))={\exp }_q(d{F}_p(\cdot ))$ of that step; (ii) ${\phi }_p$ is smooth: $y\mapsto v_y$ is smooth because ${\exp }_q$ is a diffeomorphism on $V$, $d{F}_p$ is linear, and ${\exp }_p$ is smooth on $T_{p}N$ by [F4]; (iii) ${\phi }_p$ is injective, since $F\circ {\phi }_p={\mathrm{id}}_U$; so $V_p:={\phi }_p(U)$ is diffeomorphic to $U$ with inverse $F{\mathrm{\mid }}_{V_p}$. Moreover $F^{-1}(U)={⨆}_{p\in F^{-1}(q)}{V}_p$. The inclusion $\supseteq$ is (i). Conversely, let $x\in F^{-1}(U)$ and $y:=F(x)$. The reversed radial geodesic $t\mapsto {\exp }_q((1-t)v_y)$, $t\in [0,1]$, is a geodesic from $y$ to $q$; lift it through $x$ by step 2.1, obtaining a geodesic $c$ with $c(0)=x$, $c(1)=p\in F^{-1}(q)$ and $F\circ c$ contained in $U$. Reversing $c$ gives a geodesic lift of ${\gamma }_y$ through $p$, which is the unique one by step 2.1; hence $x=c(0)={\phi }_p(y)\in V_p$. Finally the $V_p$ are pairwise disjoint. Suppose $x\in V_p\cap V_{p^{\mathrm{\prime }}}$ and put $y:=F(x)$; then $x={\phi }_p(y)$ and $x={\phi }_{p^{\mathrm{\prime }}}(y)$ are the endpoints at time $1$ of geodesic lifts $c$, $c_d$ of ${\gamma }_y$ with $c(0)=p$ and $c_d(0)=p^{\mathrm{\prime }}$. The reversed curves $\bar{c}(t):=c(1-t)$ and ${\bar{c}}_d(t):=c_d(1-t)$, $t\in [0,1]$, are geodesics of $N$ with $\bar{c}(0)={\bar{c}}_d(0)=x$ that both project under $F$ to the reversed radial geodesic $t\mapsto {\gamma }_y(1-t)$ from $y$ to $q$; both are therefore geodesic lifts of one and the same geodesic through the point $x$, so the uniqueness half of step 2.1 applied with $t_0=0$ gives $\bar{c}={\bar{c}}_d$. Evaluating at $t=1$ yields $p=c(0)=\bar{c}(1)={\bar{c}}_d(1)=c_d(0)=p^{\mathrm{\prime }}$, so $x\in V_p\cap V_{p^{\mathrm{\prime }}}$ forces $p=p^{\mathrm{\prime }}$; equivalently, the sets $V_p$ belonging to distinct points $p\mathrm{\ne }{p}^{\mathrm{\prime }}$ of $F^{-1}(q)$ are disjoint.

$F$ is a covering map. [F6, step 3.1, step 3.2] For every $q\in M$ the normal ball $U$ of step 3.2 satisfies: each $V_p={\phi }_p(U)$ is open (by smoothness of ${\phi }_p$ and (i) there), the restriction $F{\mathrm{\mid }}_{V_p}:V_p\to U$ is a homeomorphism (indeed a diffeomorphism, by (i) and (ii) there), and the sets $V_p$, $p\in F^{-1}(q)$, are pairwise disjoint with union $F^{-1}(U)$ (step 3.2). This is exactly the evenly covered condition of [F6], and $F$ is surjective by step 3.1. Hence $F$ is a covering map.

$M$ is complete. [F4, step 2.1, step 3.1] Let $\gamma :I\to M$ be a maximal geodesic of $M$; by step 3.1 and step 2.1 it has a geodesic lift $\tilde{\gamma }:I\to N$, and step 2.1 in fact produces that lift as $\tilde{\gamma }(t)={\exp }_p((t-t_0)w)$ on all of $\mathbb{R}$. Composing with $F$ recovers the maximal geodesic $\gamma$ (both are geodesics with the same initial data, and $\gamma$ is maximal), so $\gamma$ is defined at every real time; hence $I=\mathbb{R}$. Every maximal geodesic of $M$ has domain $\mathbb{R}$, so $M$ is geodesically complete, and [F4] makes $(M,g)$ complete.

Boundary and choice audit. Completeness of $N$ is used exactly twice: in step 1.2 to make the source exponential globally defined, and in step 2.1 to make the geodesic lift exist on the whole interval. The local isometry hypothesis is used for the injective differential in step 2.1, for the open-image step 1.1 and for the geodesic transport of step 1.2. Surjectivity is proved in step 3.1 before it is used in steps 4.1 and 4.2. For $n=0$ both manifolds are discrete and $F$ is a bijection of discrete sets, so the claims are immediate from those two steps; a constant geodesic or the zero vector is covered by steps 1.2 and 2.1 (the lifted geodesic is then constant). Exactly the inherited [A1] is used; no family of geodesics is selected, since each lift is produced from a prescribed initial vector.