A lifted finite CW equivalence has a contractible group-ring mapping cone

If the original map is not cellular or the chosen basepoint is not a vertex, choose a vertex of $X$, use its image under a based cellular approximation as the target vertex, and transport the previously selected fundamental groups along the basepoint paths. These finite choices do not affect the assertion after the specified coefficient transport. Hence work with the based cellular $f$ in the statement. Form $M$, $j$, $k$ and $r$. By [F1], $r$ and $k$ are inverse up to a deformation fixing $k(Y)$. Since $f=rj$ is an equivalence, $j$ is an equivalence: if $g$ is a homotopy inverse of $f$, then $gr$ is a homotopy inverse of $j$: $grj=gf\simeq 1_X$, while $rjgr=fgr\simeq r$ and the equivalence $r$ detects $jgr\simeq 1_M$.

Apply [F2] to $j(X)\subset M$ to obtain a retraction $r_j$ and homotopy $D^j:1_M\simeq j{r}_j$ fixed on $j(X)$. The standard $k(Y)$ deformation gives $r_k=kr$ and $D^k:1_M\simeq kr$ fixed on $k(Y)$. By [F3] take $r_j,r$ and both homotopies cellular relative to the indicated fixed subcomplexes and their endpoint maps. In particular $r_{j}j=1_X$, $rk=1_Y$, and the selected basepoints $j(x)$ and $k(y)$ stay fixed during the respective homotopies.

Let $\tilde{M}$ be the universal cover of $M$. The prism edge $t\mapsto [x,t]$ from $k(y)$ to $j(x)$ identifies ${\pi }_1(M,j(x))$ with ${\pi }_1(M,k(y))$ by path transport. Since $r$ collapses this edge to the constant path at $y$, the two inclusion isomorphisms identify with $f_{\ast }:\pi \to {\pi }^{\mathrm{\prime }}$ under $r_{\ast }$. Fix a lift of $k(y)$ in $\tilde{M}$, lift that edge to select a lift of $j(x)$, and identify the connected preimages of $k(Y)$ and $j(X)$ with the chosen $\tilde{Y}$ and $\tilde{X}$. They are connected universal covers because $k_{\ast }$ and $j_{\ast }$ are isomorphisms. Under these identifications the common deck ring $\mathbb{Z}[{\pi }_{1}M]$ becomes $R$ via $r_{\ast }$, the source action is precisely the transport through $f_{\ast }$, and the compatible lift of $rj=f$ is $\tilde{r}\tilde{j}=\tilde{f}$.

For $A=j(X)$ or $k(Y)$, write $i_A:A\hookrightarrow M$ and $r_A:M\to A$ for its cellular retraction. Lift $r_A$ so that ${\tilde{r}}_A{\tilde{i}}_A=1_{\tilde{A}}$ at the selected basepoint; lift $D^A:1_M\simeq i_A{r}_A$ starting at $1_{\tilde{M}}$. Since $D^A$ fixes the basepoint in $A$, uniqueness of covering homotopy lifts makes its end exactly ${\tilde{i}}_A{\tilde{r}}_A$. For every deck element $h$, the two maps ${\tilde{D}}^A(T_{h}z,t)$ and $T_h{\tilde{D}}^A(z,t)$ are lifts of the same map and agree at time zero, so they agree for all $t$. Thus the lifted deformation and its cellular prism are equivariant; under the right action they induce $R$-linear chain homotopies $C_{\ast }({\tilde{i}}_A)C_{\ast }({\tilde{r}}_A)\simeq 1_{C_{\ast }(\tilde{M})}$ and $C_{\ast }({\tilde{r}}_A)C_{\ast }({\tilde{i}}_A)=1_{C_{\ast }(\tilde{A})}$. No isolated deck transformation is claimed to be $R$-linear.

Step 3.1 makes each $C_{\ast }(\tilde{j})$ and $C_{\ast }(\tilde{k})$ an $R$-linear chain homotopy equivalence. For $k(Y)$ its retraction is $r$, so $C_{\ast }(\tilde{r})$ is an $R$-linear chain homotopy inverse to $C_{\ast }(\tilde{k})$. Since $C_{\ast }(\tilde{f})=C_{\ast }(\tilde{r})C_{\ast }(\tilde{j})$ by step 2.2, it is an $R$-linear chain homotopy equivalence. An explicit inverse is $C_{\ast }({\tilde{r}}_j)C_{\ast }(\tilde{k})$: both composites reduce to identities using the two homotopies in step 3.1 and functoriality of the induced cellular chain maps.

Apply [F5] to the chain homotopy equivalence in step 4.1. Its cone is contractible with the stated differential. By [F6], both summands in degree $n$ are finite free based right $R$-modules, so the ordered concatenation of their bases is a finite free basis, and the dimensions of $X,Y$ bound the degrees in which the cone is nonzero. Thus the cone is bounded finite free based and contractible. The contraction follows from the two explicit equivariant lifted deformation homotopies in step 3.1 through the cone criterion; no homology-vanishing converse has been used.