Restriction of injective group modules is injective

For a finite set $S$ of right cosets $gH$, let $P_S$ be the subgroup of $\mathbb{Z}[G]$ supported on their union. It is a right $\mathbb{Z}[H]$-submodule and a direct summand, by projection on those cosets. Choose representatives for these finitely many nonempty cosets. They identify $P_S$ with a finite direct sum of copies of $\mathbb{Z}[H]$. Thus for a monomorphism $A\hookrightarrow B$, the map $P_S\otimes A\to P_S\otimes B$ is a finite direct sum of that monomorphism, hence is injective. For $S=\mathrm{\varnothing }$ both tensors are zero. Finite choice is a theorem of ZF.

An element of $\mathbb{Z}[G]\otimes A$ is a finite sum of tensors and hence comes from some $P_S\otimes A$. If its image in $\mathbb{Z}[G]\otimes B$ is zero, projecting the latter tensor to $P_S\otimes B$ shows that its representing element has zero image there. Step 1.1 makes it zero already in $P_S\otimes A$. This proves induction preserves monomorphisms, without choosing representatives for any infinite family of cosets.

Given an $H$-map $A\to \mathrm{Res}I$ and an $H$-monomorphism $A\hookrightarrow B$, transpose by F2 to a $G$-map $\mathrm{Ind}A\to I$. Extend over the monomorphism $\mathrm{Ind}A\hookrightarrow \mathrm{Ind}B$ by F3, and transpose back. Naturality of the adjunction ensures the resulting $B\to \mathrm{Res}I$ extends the given map. Hence restriction preserves injectives. Restriction preserves exactness because it changes no groups or maps, so the resolution assertion follows degree by degree. Zero modules and $H=G$ or $H=1$ are included.