Why these two definitions of induced representations are equivalent? Let $F$, $G$ and $H$ be respectively a field, a finite group and a subgroup of $G$.

Problem. For a representation $(\sigma, W)$ of $H$, define an $F$-vector space $$\widetilde W=\{f\colon G\to W\mid f(hg)=\sigma(h)f(g),h\in H,g\in G\},$$ and the action of $G$ on $\widetilde W$ is given by $(g'f)(g)=f(gg')$. Then $\widetilde W$ is isomorphic to $F[G]\otimes_{F[H]}W$ (as $G$-representations, or in other words, as $F[G]$-modules).

In my algebra lecture, the induced representation of $W$ from$H$ to $G$ is defined as the $F[G]$-module $\mathrm{Ind}_H^GW:=F[G]\otimes_{F[H]}W$, and this problem says that these two definitions are equivalent. However, although tried, I have no idea how to prove it. What I think may be helpful is a proposition which is stated as follows (Here $\mathrm{Res}_H^GV$ is the restriction of $V$ to $H$)

Let $V$ be a representation of $G$ and $W$ be a subrepresentation of $\mathrm{Res}_H^GV$. Then $V\cong\mathrm{Ind}_H^GW$ if and only if $V$ is generated by $W$ as an $F[G]$-module and $\dim_FV=[G:H]\dim_FW$.

Yet I do not know how to identify $W$ with an $F[H]$-submodule of $\mathrm{Res}_H^G\widetilde W$, let alone how to verify other conditions in this proposition. So I would like to ask if it is correct to prove it in this way, or there is any easier or more straightforward proof?
Thanks in advance...
 A: It's fine that you've found a solution to your problem (I haven't checked it myself, so I don't know whether it's correct). Here's however a high-level solution for those interested in abstract nonsense. 
One of the points of the induced representation is to have the following (natural) isomorphism : $Hom_G(\rho, \mathrm{Ind}_H^G\pi) \cong Hom_H(\rho_{\mid H}, \pi)$ (where I use the map $ K\to GL(V)$ to denote the representation rather than $V$), where $\rho_{\mid H}$ denotes the restriction of $\rho$ to $H$, and where $Hom_K$ is the set of $K$-morphisms between the representations. You can check that this holds in the two presentations you gave. 
Once you prove this, then the fact that they're naturally isomorphic follows from general category-theoretic principles: indeed let $\mathbf{Rep}_K$ denote the category of $F$-representations of $K$ for a finite group $K$.
Then we have a clear functor $\mathrm{Res}: \mathbf{Rep}_G \to \mathbf{Rep}_H$ defined on objects by $\rho \mapsto \rho_{\mid H}$ (the definition on arrows is clear); and the induced representation yields a functor $\mathrm{Ind}_H^G: \mathbf{Rep}_H\to \mathbf{Rep}_G$ defined on objects by $\pi \mapsto \mathrm{Ind}_H^G \pi$ and on arrows you can either use your proof of the aforementioned isomorphism to define it (or you can define it the only possible way, for instance if we're using the definition with maps $G\to W$ : if $f : (\pi,W) \to (\pi', W')$, then $\mathrm{Ind}_H^Gf : \mathrm{Ind}_H^G \pi \to \mathrm{Ind}_H^G \pi'$ can be defined by $\mathrm{Ind}_H^Gf (g) = f\circ g$).
In any case we get a nice functor and the aforementioned isomorphism is just a way of saying that  $\mathrm{Res} \dashv \mathrm{Ind}_H^G$ (they're adjoint). But this is the case for any presentation of the induced representation; and adjoints are unique up to natural isomorphism. Therefore, any presentation of the induced representation (that satisfies the isomorphism in question) is naturally isomorphic to, say, the ones with maps $G\to W$. 
A: It seems that I have worked out an answer on my own, thanks to Cameron Williams. 
Let $T$ be a set of representatives of right $H$-cosets of $G$. For each $g\in T$, denote $W_g:=\{f\in\widetilde W\mid f|_{G\setminus Hg}=0\}$. Then we have


*

*$\dim_F\widetilde W=[G\colon H]\dim_FW$. Indeed, each $W_g$ is an $F$-vector space and $W_1$ is an $F[H]$-module. Moreover, 
\begin{align}
\begin{matrix}
\varphi\colon W\to W_1\\
w\mapsto\sigma(\cdot)w
\end{matrix}\quad
\text{and}\quad
\begin{matrix}
\psi\colon W_1\to W\\
f\mapsto f(1)
\end{matrix}
\end{align}
are $F[H]$-homomophisms (for $g\in G\setminus H$, $\sigma(g)w$ is defined to be $0$). While for each $w\in W$ and $f\in W_1$, it follows that $\psi\circ\varphi(w)=\psi(\sigma(\cdot)w)=w$ and $\varphi\circ\psi(f)=\varphi(f(1))=\sigma(\cdot)f(1)=f$ (note that $f|_{G\setminus H}=0$). Thus $\varphi$ is isomorphic. Hence $W\cong W_1$ (as $F[H]$-modules) and then $W_1\cong W_g$ (as $F$-spaces, $\forall g\in T$) and $\widetilde W=\bigoplus_{g\in T}W_g$ entails that
$$\dim_F\widetilde W=|T|\dim_FW_1=[G\colon H]\dim_FW.$$

*$W\hookrightarrow\mathrm{Res}_H^G\widetilde W$. This has been shown in the foregoing deduction: $W\cong W_1\hookrightarrow\mathrm{Res}_H^G\widetilde W$ (as $F[H]$-modules).

*$\widetilde W$ is generated by $W$ as an $F[G]$-module. For each $g\in G$, consider $gW_1$ and we have $\forall g'\in G$, $\forall f\in W_1$, $(gf)(g')=f(g'g)$, while $g'g\in H$ iff $g'\in Hg^{-1}$. Thus $$gW_1=\{f\in\widetilde W\mid f|_{G\setminus Hg^{-1}}=0\}=W_{g^{-1}},$$ and therefore
$$\widetilde W=\bigoplus_{g\in T}W_g=\sum_{g\in G}gW_1=\langle W_1\rangle_{F[G]}\cong \langle W\rangle_{F[G]}.$$
In all, it follows that $\widetilde W\cong\mathrm{Ind}_H^GW$.
