Interior product and exterior product I have seen around the internet that this should hold:
$$\iota_X(\alpha\wedge\beta)=\iota_X\alpha\wedge\beta+(-1)^k\alpha\wedge\iota_X\beta,$$
where $X$ is a vector field, $\alpha$ a $k$-form, $\beta$ an $\ell$-form, $\iota_X$ is the interior product (i.e. $\iota_X\alpha(v_1,\dotsc,v_{k-1})=\alpha(X,v_1,\dotsc,v_{k-1})$), and $\wedge$ is the exterior product. Now I define the exterior product as:
$$\alpha\wedge\beta(v_1,\dotsc,v_k,v_{k+1},\dotsc,v_{k+\ell})=\sum_{\sigma\in S_{k+\ell}}\operatorname{sgn}\sigma\alpha(v_{\sigma(1)},\dotsc,v_{\sigma(k)})\beta(v_{\sigma(k+1)},\dotsc,v_{\sigma(k+\ell)}),$$
where some others define it with a coefficient in front of it involving factorials of $\ell$ and $k$. I tried all I could to prove the above identity. I reduced it to proving the case $\alpha=df$. And I'm simply stuck on that case. No matter what, there are sign problems. So could you help me figure this out? Are there coefficients missing with my definition of wedge btw?
 A: If we let brackets denote unnormalized antisymmetrization to match your wedge convention, then in index notation we have (choosing a basis $e_{i_k}$ with $e_1 = X$)
$$\begin{align*}
\iota_X (\alpha \wedge \beta)_{i_2 \ldots i_{k+l}} &= \alpha_{[i_1 \ldots i_{k}} \beta_{i_{k+1} \ldots i_{k+l}]}.
\end{align*}$$
Now let us expand just the $i_1$ in the antisymmetrization:
$$\begin{align*}
\iota_X (\alpha \wedge \beta)_{i_2 \ldots i_{k+l}} 
&= \alpha_{i_1 [i_2\ldots i_{k}} \beta_{i_{k+1} \ldots i_{k+l}]} \\
&- \alpha_{[i_2|i_1|i_3\ldots i_{k}} \beta_{i_{k+1} \ldots i_{k+l}]} \\
&+ \alpha_{[i_2 i_3|i_1|i_4\ldots i_{k}} \beta_{i_{k+1} \ldots i_{k+l}]} \\
&\;\vdots\\
&+(-1)^k \alpha_{[i_2 i_3 i_4\ldots i_{k+1}} \beta_{|i_1 |i_{k+2} \ldots i_{k+l}]} \\
&-(-1)^k \alpha_{[i_2 i_3 i_4\ldots i_{k+1}} \beta_{i_{k+2}|i_1 |i_{k+3} \ldots i_{k+l}]}\\
&\;\vdots
\end{align*}$$
Now separating this in to two sums, note that by shifting $i_1$ to the first slot of whichever form it appears in we eliminate the alternating signs, leaving us with 
$$ \iota_X (\alpha \wedge \beta)_{i_2 \ldots i_{k+l}} = k\alpha_{i_1 [i_2 \ldots i_k} \beta_{i_{k+1}\ldots i_{k+l}]} + l(-1)^k \alpha_{[i_2 \ldots i_{k+1}} \beta_{|i_1|i_{k+2} \ldots i_{k+l}]}\\
= k(\iota_X \alpha)_{[i_2 \ldots i_k} \beta_{i_{k+1}\ldots i_{k+l}]} + l(-1)^k \alpha_{[i_2 \ldots i_{k+1}} (\iota_X \beta)_{i_{k+2} \ldots i_{k+l}]} $$
and so it seems the correct formula for your definition of the wedge product is in fact
$$ \iota_X (\alpha \wedge \beta) = k(\iota_X \alpha) \wedge \beta + l(-1)^k \alpha \wedge (\iota_X \beta).$$
A: $\DeclareMathOperator{sgn}{sgn}$
For the sake of practice I've done normed version. Normalization means that I use factorials and sum over all permutations in definition of wedge product, i.e.:
$$(\alpha\wedge\beta)(v_1,\dots,v_{k+l})=\frac{(k+l)!}{k!l!}\sum_{\sigma\in S_{k+l}}\sgn(\sigma)\alpha(v_{\sigma(1)},\dots,v_{\sigma(k)})\beta(v_{\sigma(k+1)},\dots,v_{\sigma(k+l)})$$
So we fix base and use Ricci calculus. This means that we can work only with coefficients.
Given coefficients $\alpha_{[i_1\dots i_k]}$ and $\beta_{[j_{1}\dots j_{l}]}$ of covariant tensors $\alpha$ and $\beta,$ the coefficients of wedge product are given by formula
$$(\alpha\wedge\beta)_{i_1\dots i_{k+l}}=(\alpha\wedge\beta)_{[i_1\dots i_{k+l}]}=\frac{(k+l)!}{k!l!}\alpha_{[i_1\dots i_k}\beta_{i_{k+1}\dots i_{k+l}]}.$$
Given coefficients $\omega_{[i_1\dots i_s]}$ of covariant tensor $\omega$ and coefficients $X^i$ of contravariant one tensor (i.e. vector) $X,$ the coefficients of interior product are given by formula
$$(\iota_X\omega)_{[i_1\dots i_{s-1}]}=X^i\omega_{[ii_1\dots i_{s-1}]}.$$
In order to prove
$$\iota_X(\alpha\wedge\beta)=\overbrace{\iota_X\alpha\wedge\beta}^{(1)}+\overbrace{(-1)^k\alpha\wedge\iota_X\beta}^{(2)}\hspace{20pt}(\star)$$
we will compare coefficients on left and right hand side of $(\star)$
LHS:
$$[\iota_X(\alpha\wedge\beta)]_{[i_1\dots i_{k+l-1}]}=X^i(\alpha\wedge\beta)_{[ii_1\dots i_{k+l-1}]}=\frac{(k+l)!}{k!l!}X^i\alpha_{[ii_1\dots i_{k-1}}\beta_{i_k\dots i_{k+l-1}]}$$
RHS (1):
$$[(\iota_X\alpha)\wedge\beta]_{[i_1\dots i_{k+l-1}]}=\frac{(k+l-1)!}{(k-1)!l!}(\iota_X\alpha)_{[i_1\dots i_{k-1}}\beta_{i_k\dots i_{k+l-1}]}=\frac{(k+l-1)!}{(k-1)!l!}X^i\alpha_{[ii_1\dots i_{k-1}}\beta_{i_k\dots i_{k+l-1}]}.$$
RHS (2):
$$(-1)^k[\alpha\wedge(\iota_X\beta)]_{[i_1\dots i_{k+l-1}]}=(-1)^k\frac{(k+l-1)!}{k!(l-1)!}\alpha_{[i_1\dots i_k}(\iota_X\beta)_{i_{k+1}\dots i_{k+l-1}]}=(-1)^k\frac{(k+l-1)!}{k!(l-1)!}\alpha_{[i_1\dots i_k}X^i\beta_{ii_{k+1}\dots i_{k+l-1}]}=(-1)^k\frac{(k+l-1)!}{k!(l-1)!}X^i\alpha_{[i_1\dots i_k}\beta_{ii_{k+1}\dots i_{k+l-1}]}=(-1)^k\frac{(k+l-1)!}{k!(l-1)!}X^i(-1)^k \alpha_{[ii_1\dots i_{k-1}}\beta_{i_k\dots i_{k+l-1}]}=\frac{(k+l-1)!}{k!(l-1)!}X^i\alpha_{[ii_1\dots i_{k-1}}\beta_{i_k\dots i_{k+l-1}]}$$
Adding factorials from RHS (1) and RHS (2) we get
$$\frac{(k+l-1)!}{(k-1)!l!}+\frac{(k+l-1)!}{k!(l-1)!}=\frac{(k+l-1)!k}{k!l!}+\frac{(k+l-1)!l}{k!l!}=\frac{(k+l-1)!(k+l)}{k!l!}=\frac{(k+l)!}{k!l!}.$$
What finishes the proof.
