Why is $ U \otimes \operatorname{Ind}(W) = \operatorname{Ind}(\operatorname{Res}(U) \otimes W)$?

I take it $H \leq G$. These reps are not equal, but they are isomorphic. It will be more natural to prove that $ (W \otimes U|_H) \uparrow^G \cong (W \uparrow ^G) \otimes U $, but this is equivalent as $A\otimes B \cong B \otimes A$ for modules over group algebras.

We want a module map $kG \otimes_H (W \otimes U|_H) \to (kG\otimes_H W) \otimes U$. Take $\beta: x\otimes (w \otimes u) \mapsto (x\otimes w) \otimes x u $. This is easily verified to be a module map (and well-defined: there is an issue because of the $\otimes_H$).

Now define $\alpha : (kG\otimes_H W) \otimes U \to kG \otimes_H (W \otimes U|_H)$ by $(x \otimes w) \otimes u \mapsto x \otimes ( w \otimes x^{-1} u )$. This is inverse to $\beta$, and is well-defined and a module map: thus the two modules are isomorphic.

Surprisingly, all this generalises to arbitrary Hopf algebras (even non-cocommutative ones). The maps are slightly more messy to write down though.

Here is a proof ${\rm Ind}_H^G(V\otimes{\rm Res}_H^GW)\cong({\rm Ind}_H^GV)\otimes W$ are isomorphic using the categorial version of Frobenius reciprocity (that $\rm Ind$, $\rm Res$ are adjoint functors), as well as three other lemmas:

Lemma I. If $\hom_G(A,U)\cong\hom_G(B,U)$ for all $U\in{\rm Rep}(G)$ then $A\cong B$.

Lemma II (Frobenius reciprocity). $\hom_G({\rm Ind}_H^GA,B)\cong\hom_H(A,{\rm Res}_H^GB)$.

Lemma III (currying). $\hom_H(A\otimes B,C)\cong\hom_H(A,B^*\otimes C)$.

Lemma IV. $({\rm Res}_H^GA)^*\cong{\rm Res}_H^G(A^*)$ and $({\rm Res}_H^GA)\otimes({\rm Res}_H^GB)\cong{\rm Res}_H^G(A\otimes B)$.

We employ the last three lemmas to verify the hypothesis of the first lemma: for all $U\in{\rm Rep}(G)$,

$$\begin{array}{llll} & \hom_G({\rm Ind}_H^G(V\otimes{\rm Res}_H^GW),U) & \cong & \hom_H(V\otimes{\rm Res}_H^GW,{\rm Res}_H^GU) \\ \cong & \hom_H(V,({\rm Res}_H^GW)^*\otimes{\rm Res}_H^GU) & \cong & \hom_H(V,{\rm Res}_H^G(W^*\otimes U)) \\ \cong & \hom_G({\rm Ind}_H^GV,W^*\otimes U) & \cong & \hom_G(({\rm Ind}_H^GV)\otimes W,U). \end{array}$$

Hence ${\rm Ind}_H^G(V\otimes{\rm Res}_H^GW)\cong({\rm Ind}_H^GV)\otimes W.$

In fact the functors ${\rm Ind}_H^G(-\otimes{\rm Res}_H^G-)$ and $({\rm Ind}_H^G-)\otimes-:{\rm Rep}(H)\times{\rm Rep}(G)\to{\rm Rep}(G)$ should be naturally isomorphic (via a canonical isomorphism mt_ gave). All of the isomorphisms in the above calculation are natural, but I am not sure how to successfully upgrade Lemma I to talk about naturality.