[proofplan] The strategy proceeds in two stages. First, we equip the tangent space $T_p M$ with the pulled-back metric $\tilde g := \exp_p^* g$. Under $K \leq 0$, no Jacobi field vanishing at $0 \in T_p M$ vanishes anywhere else (by [Non-Positive Curvature Implies No Conjugate Points](/theorems/2738)), so $d(\exp_p)_v$ is a linear isomorphism for every $v \in T_p M$ — i.e., $\exp_p$ is a local diffeomorphism, and $\tilde g$ is a smooth Riemannian metric on $T_p M$. Second, we show $\exp_p : (T_p M, \tilde g) \to (M, g)$ is a local isometry by construction, and the radial-line geodesics through $0 \in T_p M$ are geodesics of $\tilde g$ defined on all of $\mathbb{R}$ (Gauss' lemma plus the geodesic correspondence under local isometries). Hence $(T_p M, \tilde g)$ is geodesically complete at $0$, and by [Hopf–Rinow Theorem](/theorems/2726), $(T_p M, \tilde g)$ is complete. The [Local Isometry onto Complete Domain](/theorems/2736) (sketch corollary of [Local Isometry from Complete Manifold is a Covering Map](/theorems/2735)) then forces $\exp_p$ to be a covering map onto $(M, g)$. [/proofplan]

[step:Verify $\exp_p$ is defined on all of $T_p M$ and has full-rank differential everywhere]Let $(M, g)$ be the complete connected Riemannian manifold with $K \leq 0$ on every two-plane in $TM$, and fix $p \in M$. By the [Hopf–Rinow Theorem](/theorems/2726), completeness of $(M, g)$ is equivalent to geodesic completeness, so the exponential map \begin{align*} \exp_p : T_p M \to M \end{align*} is defined on all of $T_p M$. We claim $d(\exp_p)_v : T_v(T_p M) \to T_{\exp_p(v)} M$ is a linear isomorphism for every $v \in T_p M$. Identify $T_v(T_p M) \cong T_p M$ via the canonical identification of a vector space with its tangent space at any point (the translation isomorphism $T_p M \to T_v(T_p M)$, $w \mapsto \frac{d}{ds}\big|_{s=0}(v + sw)$). Both $T_v(T_p M)$ and $T_{\exp_p(v)}M$ have dimension $n$, so it suffices to show $d(\exp_p)_v$ is injective. Fix $w \in T_p M$ with $d(\exp_p)_v(w) = 0$. Define the geodesic \begin{align*} \gamma : \mathbb{R} &\to M, \\ t &\mapsto \exp_p(tv), \end{align*} which has $\gamma(0) = p$, $\dot\gamma(0) = v$, and is defined on all of $\mathbb{R}$ by completeness. By [Jacobi Fields via the Exponential Map](/theorems/2717), the field \begin{align*} J : \mathbb{R} &\to TM, \\ t &\mapsto J(t) := d(\exp_p)_{tv}(tw) \end{align*} is a Jacobi field along $\gamma$ with $J(0) = 0$ and $J'(0) := \nabla_t J(0) = w$. At $t = 1$: \begin{align*} J(1) = d(\exp_p)_v(w) = 0. \end{align*} Hence $J$ vanishes at $t = 0$ and at $t = 1$. By [Non-Positive Curvature Implies No Conjugate Points](/theorems/2738) applied to $\gamma$ on $(M, g)$ — whose hypotheses are $K \leq 0$ along $\gamma$, given by the chapter hypothesis — no non-trivial Jacobi field vanishing at one point can vanish at any other point on $\gamma$. Therefore $J \equiv 0$, which gives $w = J'(0) = 0$. This proves $d(\exp_p)_v$ is injective, hence bijective, hence an isomorphism. Therefore $\exp_p : T_p M \to M$ is a local diffeomorphism at every $v \in T_p M$.[/step]

[guided]We are using two pieces of information about $(M, g)$ separately. **Completeness of $(M, g)$** gives us $\exp_p$ defined on all of $T_p M$, via the equivalence of metric and geodesic completeness in the [Hopf–Rinow Theorem](/theorems/2726). **Non-positive curvature** will give us injectivity of $d(\exp_p)_v$ at every $v$ — without this, the exponential map could fold over itself at conjugate points, and the differential could degenerate. Without completeness we would have no global map; without non-positive curvature, no global immersion. Let $(M, g)$ be the complete connected Riemannian manifold with $K \leq 0$ on every two-plane in $TM$, and fix $p \in M$. Hopf–Rinow tells us metric completeness is equivalent to geodesic completeness, so every geodesic extends for all time, and the exponential map \begin{align*} \exp_p : T_p M \to M \end{align*} is defined on all of $T_p M$. This handles the "global domain" question. We now turn to the differential. **Goal:** show $d(\exp_p)_v : T_v(T_p M) \to T_{\exp_p(v)} M$ is a linear isomorphism for every $v \in T_p M$. We first identify the source. The tangent space to a vector space at any point is canonically the vector space itself: the translation isomorphism $T_p M \to T_v(T_p M)$, $w \mapsto \frac{d}{ds}\big|_{s=0}(v + sw)$, gives $T_v(T_p M) \cong T_p M$. Both source and target then have dimension $n$, so by the rank-nullity theorem it suffices to prove injectivity. **The strategy: turn the kernel of $d(\exp_p)_v$ into a vanishing Jacobi field.** Why Jacobi fields? Because the standard formula $J(t) = d(\exp_p)_{tv}(tw)$ packages exactly the differential of $\exp_p$ along the radial direction into a Jacobi field — and Jacobi fields are where curvature acts. So a kernel element $w$ becomes a Jacobi field with two zeros, and non-positive curvature forbids that. Fix $w \in T_p M$ with $d(\exp_p)_v(w) = 0$. Define the radial geodesic \begin{align*} \gamma : \mathbb{R} &\to M, \\ t &\mapsto \exp_p(tv), \end{align*} which has $\gamma(0) = p$ and $\dot\gamma(0) = v$, and is defined on all of $\mathbb{R}$ by completeness. The Jacobi field we want is the one arising from the variation $f(t, s) := \exp_p(t(v + sw))$ — a variation of $\gamma$ through nearby radial geodesics. Differentiating in $s$ at $s = 0$ and applying [Jacobi Fields via the Exponential Map](/theorems/2717) yields \begin{align*} J : \mathbb{R} &\to TM, \\ t &\mapsto J(t) := d(\exp_p)_{tv}(tw), \end{align*} a Jacobi field along $\gamma$ with $J(0) = 0$ (the variation fixes $p$) and $J'(0) := \nabla_t J(0) = w$. The kernel hypothesis $d(\exp_p)_v(w) = 0$ at the parameter $t = 1$ becomes \begin{align*} J(1) = d(\exp_p)_v(w) = 0. \end{align*} So $J$ vanishes at both $t = 0$ and $t = 1$ — two zeros of a Jacobi field along the same geodesic. **This is exactly a conjugate-point statement.** We now invoke [Non-Positive Curvature Implies No Conjugate Points](/theorems/2738) on the geodesic $\gamma$. Its hypotheses require sectional curvature $\leq 0$ along $\gamma$, which holds because the chapter-wide hypothesis is $K \leq 0$ everywhere on $M$ — so in particular $K \leq 0$ on every two-plane along $\gamma$. The conclusion: no non-trivial Jacobi field vanishing at one point of $\gamma$ can vanish at any other point. Since $J$ vanishes at $t = 0$ and $t = 1$, the contrapositive forces $J \equiv 0$. Then \begin{align*} w = J'(0) = \nabla_t J(0) = 0. \end{align*} This proves $d(\exp_p)_v$ is injective. Combined with the dimension argument, $d(\exp_p)_v$ is a linear isomorphism for every $v \in T_p M$. By the inverse function theorem, $\exp_p : T_p M \to M$ is therefore a local diffeomorphism at every point — exactly the conclusion we needed for Step 2's pullback construction.[/guided]

[step:Define the pulled-back metric $\tilde g := \exp_p^* g$ on $T_p M$] Since $\exp_p : T_p M \to M$ is a local diffeomorphism at every point, the pullback metric \begin{align*} \tilde g := \exp_p^* g \end{align*} is well-defined: for $v \in T_p M$ and $X, Y \in T_v(T_p M)$, \begin{align*} \tilde g_v(X, Y) := g_{\exp_p(v)}(d(\exp_p)_v X, d(\exp_p)_v Y). \end{align*} Because $d(\exp_p)_v$ is an isomorphism, $\tilde g_v$ is a positive-definite symmetric bilinear form on $T_v(T_p M)$. Smoothness of $\exp_p$ and $g$ gives smoothness of $\tilde g$ in $v$. Hence $(T_p M, \tilde g)$ is a smooth Riemannian manifold (using the canonical smooth structure on $T_p M$ as a finite-dimensional vector space). By construction, \begin{align*} \exp_p : (T_p M, \tilde g) \to (M, g) \end{align*} is a local isometry: at every $v \in T_p M$, $d(\exp_p)_v$ pulls $g$ to $\tilde g$ pointwise. [/step]

[step:Show that radial straight lines in $T_p M$ are geodesics of $\tilde g$ defined on all of $\mathbb{R}$] Let $u \in T_p M \setminus \{0\}$. Define the radial line \begin{align*} \sigma_u : \mathbb{R} &\to T_p M, \\ t &\mapsto t u. \end{align*} We claim $\sigma_u$ is a geodesic of $(T_p M, \tilde g)$, defined on all of $\mathbb{R}$. By construction, $\exp_p \circ \sigma_u (t) = \exp_p(tu)$ is a geodesic of $(M, g)$ (the radial geodesic from $p$ with initial velocity $u$), defined on all of $\mathbb{R}$ by completeness of $(M, g)$. Since $\exp_p : (T_p M, \tilde g) \to (M, g)$ is a local isometry and local isometries pull geodesics back to geodesics — the pullback of the Levi-Civita connection equals the Levi-Civita connection of the pullback metric, by the uniqueness of Levi-Civita — the curve $\sigma_u$ is a geodesic of $\tilde g$ at every $t$ where $\exp_p \circ \sigma_u$ is locally a geodesic, which is everywhere. We make this explicit. Let $\widetilde\nabla$ denote the Levi-Civita connection of $\tilde g$, and $\nabla$ that of $g$. For any vector field $X$ on $T_p M$ and $Y \in \mathfrak{X}(T_p M)$, the pullback connection satisfies $d(\exp_p)(\widetilde\nabla_X Y) = \nabla_{d(\exp_p)X}(d(\exp_p) Y)$ in the sense of $\exp_p$-related vector fields, which is well-defined locally because $\exp_p$ is a local diffeomorphism. Both connections are torsion-free and metric-compatible (with respect to $\tilde g$ and $g$ respectively), and the pullback inherits both properties. By uniqueness of the Levi-Civita connection of $\tilde g$, the pullback connection is $\widetilde\nabla$ itself. Therefore for the curve $\sigma_u$ in $T_p M$ and the curve $\beta := \exp_p \circ \sigma_u$ in $M$: \begin{align*} d(\exp_p)_{\sigma_u(t)}(\widetilde\nabla_t \dot\sigma_u(t)) = \nabla_t \dot\beta(t). \end{align*} Since $\beta$ is a geodesic of $g$, $\nabla_t \dot\beta = 0$, and since $d(\exp_p)_{\sigma_u(t)}$ is injective, $\widetilde\nabla_t \dot\sigma_u = 0$. Hence $\sigma_u$ is a geodesic of $\tilde g$. Moreover, the maximal domain of $\sigma_u$ as a geodesic of $\tilde g$ is at least the maximal domain of $\beta = \exp_p \circ \sigma_u$ as a geodesic of $g$ — which by completeness of $(M, g)$ is all of $\mathbb{R}$. In particular, every radial line through the origin $0 \in T_p M$ is a $\tilde g$-geodesic defined on all of $\mathbb{R}$, so $\widetilde{\exp}_0 : T_0(T_p M) \cong T_p M \to T_p M$ is defined on all of $T_p M$, and $\widetilde{\exp}_0(u) = \sigma_u(1) = u$ — i.e., $\widetilde{\exp}_0$ is the identity map on $T_p M \cong T_0(T_p M)$. [/step]

[step:Conclude $(T_p M, \tilde g)$ is complete]By the previous step, the exponential map $\widetilde{\exp}_0$ of $(T_p M, \tilde g)$ at $0$ is defined on all of $T_0(T_p M) \cong T_p M$. By the [Hopf–Rinow Theorem](/theorems/2726), the equivalence of conditions $(3) \implies (5)$, since $\widetilde{\exp}_0$ is defined on all of $T_0(T_p M)$ and $(T_p M, \tilde g)$ is connected (it is path-connected as a vector space), the metric space $(T_p M, \tilde g)$ is metrically complete. The connectedness hypothesis of Hopf–Rinow is satisfied: $T_p M$ is a connected smooth manifold (being a vector space, hence path-connected). The other standing hypotheses are also met: $\tilde g$ is a smooth Riemannian metric (Step 2), and we work on the connected manifold $(T_p M, \tilde g)$. Hence $(T_p M, \tilde g)$ is a complete Riemannian manifold.[/step]

[guided]The completeness of $(T_p M, \tilde g)$ comes specifically from "$\exp_q$ is defined on all of $T_q M$ for some $q$" — condition $(3)$ in our [Hopf–Rinow Theorem](/theorems/2726) — applied at $q = 0 \in T_p M$. We do not need completeness at every basepoint, just at one; Hopf-Rinow then gives metric completeness for the whole space. Why is $\widetilde{\exp}_0$ defined on all of $T_p M$? Because every radial line $t \mapsto tu$ from $0$ in $T_p M$ is a $\tilde g$-geodesic (by construction, since $\exp_p$ is a local isometry mapping it to a $g$-geodesic) and is defined on all of $\mathbb{R}$ (since $(M, g)$ is complete, the corresponding $g$-geodesic in $M$ is defined on all of $\mathbb{R}$). The push-forward of the maximal domain in $T_p M$ matches the maximal domain in $M$ because the local isometry pushes geodesics to geodesics injectively in the parametrisation. A subtle point: one might worry that a $\tilde g$-geodesic could escape to infinity faster than its $g$-image, but the local isometry property says $\tilde g$-arclength equals $g$-arclength along any pair of corresponding curves, so the parametrisation matches and the maximal domains coincide.[/guided]

[step:Apply the local-isometry covering theorem to conclude $\exp_p$ is a covering map] We have established: - $\exp_p : (T_p M, \tilde g) \to (M, g)$ is a smooth local isometry (Step 2), - $(T_p M, \tilde g)$ is complete (Step 4), - $(M, g)$ is connected (chapter hypothesis on $M$). By [Local Isometry onto Complete Domain](/theorems/2736), every local isometry $f : (M', g') \to (N, h)$ with $M'$ complete and $N$ connected is a covering map of $N$. Applying this with $M' = T_p M$, $g' = \tilde g$, $N = M$, $h = g$, $f = \exp_p$: \begin{align*} \exp_p : T_p M \to M \quad \text{is a covering map.} \end{align*} In particular, $\exp_p$ is surjective (covering maps onto connected spaces are surjective). [/step]

[step:Deduce the simply connected case]If $M$ is simply connected, every covering map $\exp_p : T_p M \to M$ is a homeomorphism — and being a smooth local diffeomorphism, it is a diffeomorphism. Concretely: a covering map of a simply connected base from a connected total space is a homeomorphism, since the universal property of universal covers shows $T_p M \to M$ has the same number of sheets as $\pi_1(M) = \{1\}$ has elements, namely one. (Alternatively, the connected total space $T_p M$ of a covering of the simply connected $M$ must equal $M$ as a covering, hence $\exp_p$ is bijective; its smoothness and full-rank differential then make it a diffeomorphism.) Thus $\exp_p : T_p M \to M$ is a diffeomorphism, and $T_p M \cong \mathbb{R}^n$ as a smooth manifold (any choice of basis gives a linear isomorphism, hence a diffeomorphism of smooth manifolds), so \begin{align*} M \cong T_p M \cong \mathbb{R}^n \end{align*} as smooth manifolds.[/step]

[guided]We have $\exp_p : T_p M \to M$ a covering map (Step 5), and we now add the assumption that $M$ is simply connected. The strategy has two pieces: first promote the covering map to a homeomorphism using simple connectivity, then identify $T_p M$ with $\mathbb{R}^n$. **Piece 1: a connected covering of a simply connected base is a homeomorphism.** Why? The number of sheets of a connected covering equals the index $[\pi_1(M) : (\exp_p)_* \pi_1(T_p M)]$, which divides $|\pi_1(M)|$. Since $\pi_1(M) = \{1\}$ by hypothesis, the index is $1$ — the covering has exactly one sheet, i.e., it is a bijection. (Equivalently: $T_p M$, being a vector space, is connected and simply connected; $M$ is simply connected; both are connected covers of $M$, hence isomorphic as covers, so $\exp_p$ is the trivial single-sheeted cover.) We apply this here. The total space $T_p M$ is a vector space, hence path-connected and simply connected. The base $M$ is connected (chapter hypothesis) and simply connected (case hypothesis). So $\exp_p$ has one sheet and is bijective. A bijective covering map is a homeomorphism. Combined with the fact that $\exp_p$ is a smooth local diffeomorphism (Step 1), bijectivity upgrades it to a global diffeomorphism: a smooth bijection with everywhere-invertible differential is a diffeomorphism by the inverse function theorem applied at each point. **Piece 2: $T_p M \cong \mathbb{R}^n$ as a smooth manifold.** This is standard but worth spelling out. Pick any basis $e_1, \dots, e_n$ of $T_p M$ and define the linear isomorphism \begin{align*} \Phi : \mathbb{R}^n &\to T_p M, \\ (x_1, \dots, x_n) &\mapsto \sum_{i=1}^n x_i e_i. \end{align*} $\Phi$ is a linear bijection between finite-dimensional vector spaces; both $\Phi$ and $\Phi^{-1}$ are linear maps and hence smooth in the canonical smooth structures, so $\Phi$ is a diffeomorphism. **Combining the pieces.** Composing the diffeomorphism $\exp_p : T_p M \to M$ with $\Phi$: \begin{align*} \exp_p \circ \Phi : \mathbb{R}^n \to M \end{align*} is a composition of two diffeomorphisms, hence a diffeomorphism. Therefore \begin{align*} M \cong T_p M \cong \mathbb{R}^n \end{align*} as smooth manifolds, which is the desired conclusion. **The full Hadamard–Cartan picture.** Complete simply-connected manifolds with $K \leq 0$ are diffeomorphic to $\mathbb{R}^n$, and in particular have contractible topology. In the non-simply-connected case Step 5 still gives that $\exp_p$ is a covering map, so the universal cover $\widetilde M$ of $M$ is diffeomorphic to $\mathbb{R}^n$, and $M = \widetilde M / \pi_1(M)$ is the quotient by a group of deck transformations acting freely and properly discontinuously on $\mathbb{R}^n$ — the standard structure for non-positively curved manifolds.[/guided]