[proofplan] A homotopy equivalence $f: X \to Y$ comes with a homotopy inverse $g: Y \to X$, but the defining homotopies $f \circ g \simeq \operatorname{id}_Y$ and $g \circ f \simeq \operatorname{id}_X$ are free homotopies — they move basepoints. Applying the change-of-basepoint lemma to each of these homotopies converts the composite on fundamental groups into the post-composition by a change-of-basepoint isomorphism. From $g_* \circ f_* = u'_\#$ (an isomorphism) we extract injectivity of $f_*$ and surjectivity of $g_*$ at one basepoint; from the symmetric identity $f_* \circ g_* = u_\#$ applied at the shifted basepoint we extract the other two halves. Combining these bijectivity statements with the correct basepoint bookkeeping shows $f_*$ is an isomorphism. [/proofplan]

[step:Fix a homotopy inverse and the two free homotopies] Since $f: X \to Y$ is a homotopy equivalence, by definition there exist a continuous map $g: Y \to X$ and continuous homotopies \begin{align*} H: Y \times I &\to Y, & H(y, 0) &= f(g(y)), & H(y, 1) &= y, \\ H': X \times I &\to X, & H'(x, 0) &= g(f(x)), & H'(x, 1) &= x, \end{align*} so $f \circ g \simeq_{H} \operatorname{id}_Y$ and $g \circ f \simeq_{H'} \operatorname{id}_X$. Fix the basepoint $x_0 \in X$ and write \begin{align*} y_0 := f(x_0), \qquad x_1 := g(y_0) = g(f(x_0)), \qquad y_1 := f(x_1) = f(g(f(x_0))). \end{align*} Define the two tracking paths recording how the basepoint drifts under $H'$ and $H$: \begin{align*} u': I &\to X & u'(t) &:= H'(x_0, t), & u'(0) &= x_1, \ u'(1) = x_0, \\ u: I &\to Y & u(t) &:= H(y_0, t), & u(0) &= y_1, \ u(1) = y_0. \end{align*} Both $u'$ and $u$ are continuous (restrictions of continuous homotopies). The induced maps on fundamental groups and the three change-of-basepoint isomorphisms we will use are: \begin{align*} f_*: \pi_1(X, x_0) &\to \pi_1(Y, y_0), & g_*: \pi_1(Y, y_0) &\to \pi_1(X, x_1), \\ f_*^{x_1}: \pi_1(X, x_1) &\to \pi_1(Y, y_1), & u'_\#: \pi_1(X, x_1) &\to \pi_1(X, x_0), \\ u_\#: \pi_1(Y, y_1) &\to \pi_1(Y, y_0). & & \end{align*} The superscript on $f_*^{x_1}$ records that we take the map induced by $f$ at the basepoint $x_1$; the subscript-free $f_*$ always means the induced map at $x_0$. By the [change-of-basepoint isomorphism theorem](/theorems/???), $u'_\#$ and $u_\#$ are group isomorphisms (a path induces an isomorphism of fundamental groups between its endpoints). [/step]

[step:Apply the change-of-basepoint lemma to $H'$ to show $g_* \circ f_* = u'_\#$]The map $H': X \times I \to X$ is a homotopy from $g \circ f$ to $\operatorname{id}_X$, and the path $H'(x_0, \cdot) = u'$ runs from $(g \circ f)(x_0) = x_1$ to $\operatorname{id}_X(x_0) = x_0$. Apply the [Homotopic Maps and Base-change theorem](/theorems/1881) with source $X$, target $X$, maps $g \circ f$ (in the role of $f$ in that theorem) and $\operatorname{id}_X$ (in the role of $g$), homotopy $H'$, basepoint $x_0$, and tracking path $u'$. The theorem yields the identity \begin{align*} (\operatorname{id}_X)_* = u'_\# \circ (g \circ f)_*: \pi_1(X, x_0) \to \pi_1(X, x_0). \end{align*} Since $(\operatorname{id}_X)_* = \operatorname{id}_{\pi_1(X, x_0)}$ by the [functoriality of $\pi_1$ at identities](/theorems/???), and since $(g \circ f)_* = g_* \circ f_*$ by the [functoriality of $\pi_1$ under composition](/theorems/???) — applied to the composition $X \xrightarrow{f} Y \xrightarrow{g} X$ at basepoint $x_0$ — we obtain \begin{align*} \operatorname{id}_{\pi_1(X, x_0)} = u'_\# \circ g_* \circ f_*. \end{align*} Composing on the left by the inverse of $u'_\#$ (which exists because $u'_\#$ is an isomorphism) gives \begin{align*} g_* \circ f_* = (u'_\#)^{-1}: \pi_1(X, x_0) \to \pi_1(X, x_1). \end{align*} This is a composition of an isomorphism with $f_*$ on one side and $g_*$ on the other.[/step]

[guided]The conclusion we are extracting from $H'$ is one piece of the bijectivity argument. We want to use that $g \circ f \simeq \operatorname{id}_X$ to conclude something about $f_*$ and $g_*$. The temptation is to say "apply $\pi_1$ to both sides and get $g_* \circ f_* = \operatorname{id}$". This is **wrong** because $\pi_1$ is only functorial with respect to *based* maps and *based* homotopies; our homotopy $H'$ moves the basepoint, as recorded in the path $u'$. The [Homotopic Maps and Base-change theorem](/theorems/1881) is precisely the correction: when the homotopy moves the basepoint along a path $u'$, the two induced maps differ by the change-of-basepoint isomorphism $u'_\#$. We verify the hypotheses of that theorem: we need two maps with the same source and target, and a homotopy between them. Here the source is $X$, the target is $X$, the maps are $g \circ f$ and $\operatorname{id}_X$, and the homotopy is $H'$. The path $u'$ is automatically the track of the basepoint, by definition $u'(t) = H'(x_0, t)$. All hypotheses are met. From $(u'_\#) \circ (g_* \circ f_*) = \operatorname{id}$ we do not yet know that $g_* \circ f_*$ is an isomorphism — only that it is a right inverse to $u'_\#$ (in fact $(u'_\#)^{-1}$). But since $u'_\#$ is itself an isomorphism, its right inverse is its two-sided inverse, and so $g_* \circ f_* = (u'_\#)^{-1}$ is an isomorphism. Why does this give $f_*$ injective and $g_*$ surjective? Because $(g_*) \circ (f_*)$ is a bijection: the composite is injective, forcing $f_*$ to be injective; the composite is surjective, forcing $g_*$ to be surjective.[/guided]

[step:Extract injectivity of $f_*$ and surjectivity of $g_*$ from the composite identity] By the previous step, $g_* \circ f_* = (u'_\#)^{-1}$ is an isomorphism of groups. In particular it is both injective and surjective. If a composition $h \circ k$ is injective then $k$ is injective, and if $h \circ k$ is surjective then $h$ is surjective (by the standard set-theoretic argument). Applying these to $h = g_*$ and $k = f_*$: \begin{align*} f_*: \pi_1(X, x_0) &\to \pi_1(Y, y_0) \text{ is injective,} \\ g_*: \pi_1(Y, y_0) &\to \pi_1(X, x_1) \text{ is surjective.} \end{align*} [/step]

[step:Apply the change-of-basepoint lemma to $H$ to show $f_*^{x_1} \circ g_* = u_\#$] Symmetrically, $H$ is a homotopy from $f \circ g$ to $\operatorname{id}_Y$ and the tracking path at the basepoint $y_0$ is $u(t) = H(y_0, t)$, running from $f(g(y_0)) = y_1$ to $y_0$. Apply the [Homotopic Maps and Base-change theorem](/theorems/1881) with source $Y$, target $Y$, maps $f \circ g$ and $\operatorname{id}_Y$, homotopy $H$, basepoint $y_0$, and tracking path $u$: \begin{align*} (\operatorname{id}_Y)_* = u_\# \circ (f \circ g)_*: \pi_1(Y, y_0) \to \pi_1(Y, y_0). \end{align*} Functoriality at identities gives $(\operatorname{id}_Y)_* = \operatorname{id}_{\pi_1(Y, y_0)}$; functoriality on $Y \xrightarrow{g} X \xrightarrow{f} Y$ at basepoint $y_0$ gives $(f \circ g)_* = f_*^{x_1} \circ g_*$, where $f_*^{x_1}$ is required because $g$ sends $y_0$ to $x_1$, so the subsequent application of $f_*$ must use $x_1$ as source basepoint. Therefore \begin{align*} \operatorname{id}_{\pi_1(Y, y_0)} = u_\# \circ f_*^{x_1} \circ g_*, \end{align*} and composing with $(u_\#)^{-1}$ on the left, \begin{align*} f_*^{x_1} \circ g_* = (u_\#)^{-1}: \pi_1(Y, y_0) \to \pi_1(Y, y_1). \end{align*} As before, this composition is an isomorphism. Applying the "injective composite $\Rightarrow$ right factor injective" and "surjective composite $\Rightarrow$ left factor surjective" principles with $h = f_*^{x_1}$ and $k = g_*$: \begin{align*} g_*: \pi_1(Y, y_0) &\to \pi_1(X, x_1) \text{ is injective,} \\ f_*^{x_1}: \pi_1(X, x_1) &\to \pi_1(Y, y_1) \text{ is surjective.} \end{align*} [/step]

[step:Combine the four conclusions to show $f_*$ is an isomorphism]From the two previous steps we have, at their respective basepoints, \begin{align*} f_*: \pi_1(X, x_0) &\to \pi_1(Y, y_0) \text{ is injective,} \\ g_*: \pi_1(Y, y_0) &\to \pi_1(X, x_1) \text{ is both injective and surjective.} \end{align*} In particular $g_*: \pi_1(Y, y_0) \to \pi_1(X, x_1)$ is an isomorphism. Returning to the identity $g_* \circ f_* = (u'_\#)^{-1}$ of Step 2, both $g_*$ and $(u'_\#)^{-1}$ are isomorphisms, so \begin{align*} f_* = (g_*)^{-1} \circ (u'_\#)^{-1}: \pi_1(X, x_0) \to \pi_1(Y, y_0) \end{align*} is the composition of two isomorphisms, hence itself an isomorphism. This establishes the claim.[/step]

[guided]We have four facts — $f_*$ injective, $g_*$ injective, $g_*$ surjective, $f_*^{x_1}$ surjective — and we want $f_*$ to be an isomorphism. The data for $f_*$ alone only gives injectivity; the surjectivity must come from elsewhere. The cleanest route is: once we know $g_*: \pi_1(Y, y_0) \to \pi_1(X, x_1)$ is bijective, we can left-invert the composite identity. From $g_* \circ f_* = (u'_\#)^{-1}$, composing on the left by $(g_*)^{-1}$ gives $f_* = (g_*)^{-1} \circ (u'_\#)^{-1}$. Since $(g_*)^{-1}$ and $(u'_\#)^{-1}$ are both isomorphisms, their composition is an isomorphism. A purely cardinality-based argument (that $f_*$ is injective plus $|\pi_1(X, x_0)| = |\pi_1(Y, y_0)|$ implies bijective) would require finiteness, which is not assumed. The composition-of-isomorphisms argument above works in full generality. Why did we need to introduce the shifted basepoint $x_1$ and the induced map $f_*^{x_1}$? Because the second homotopy $H$ lives in $Y$, so when we unwind $(f \circ g)_*$ using functoriality of $\pi_1$, the $g$ part lands us at $x_1 = g(y_0)$, not $x_0$. The induced map $f_*$ at $x_0$ would land in $\pi_1(Y, y_0)$, but the $f$ appearing after $g$ starts from $x_1$, so we need $f_*^{x_1}: \pi_1(X, x_1) \to \pi_1(Y, f(x_1)) = \pi_1(Y, y_1)$. This basepoint bookkeeping is the only subtle feature of the proof and is the reason the lemma of Step 2 is applied twice with different data rather than used symmetrically.[/guided]