Prove the existence (or well-definedness) of the induced connection in tensor bundle Given a connection $\nabla$ on a vector bundle $E$ over a smooth manifold $M$, we know there is a unique extension of $\nabla$ to all tensor bundles of $E$ that satisfies Leibniz rule and contraction. I am going to prove this.
We can first define the connection on the dual space of $E$ using the formula forced by the axioms above. Then the rest is essentially just proving one lemma:
Given two bundles $E$, $F$ on $M$ and connections on $E$ and $F$, both denoted by $\nabla$, then there is a unique connection $\nabla$ on $E\otimes F$ such that 
$$\nabla_X(s_E\otimes s_F)=\nabla_X s_E\otimes s_F+s_E\otimes \nabla_X s_F$$
I tried to invoke the universal property of tensor product as usual, to use bilinearity to prove well-definedness. However this tensor product of sections is not the strict tensor product in linear algebra tense (it takes tensor product pointwise, and it cannot be understood as a tensor product of two $\mathbb R$-vector spaces. It can be tensor product of $C^\infty(M)$ modules though, but $\nabla_X$ is not $C^\infty$ linear). So I get in problem here, and I ask for a conceptual way to show why $\nabla_X$ is a well defined map from the space of sections of $E\otimes F$ to itself. 
 A: It seems to me that people usually include the $\mathbb{R}$-linearity as part of the definition (correct me if I'm wrong); i.e. define $\nabla$ on the simple tensors by the product rule above, and then extend it linearly over $\mathbb{R}$ to the whole space $C^{\infty}(E\otimes F)$.
Actually, due to the fact that $C^{\infty}(E\otimes F)\simeq C^{\infty}(E)\otimes_{C^{\infty}(M)}C^{\infty}(F)$ which OP has mentioned in the comment above, it follows that additivity (i.e.
\begin{align}
\nabla_X(s\otimes t+s'\otimes t')=\nabla_X(s\otimes t)+\nabla_X(s'\otimes t')
\end{align}
which is weaker than $\mathbb{R}$-linearity) is sufficient.
With this in mind, here is an alternative proof, which is essentially a direct computation, though perhaps it may look less elegant.
Let $A\in C^{\infty}(E\otimes F)$. Such $A$ can be expressed as a finite sum of simple tensors, though not uniquely in general. So we want to show that if it can be written in the following two ways
\begin{align}
A=\sum_is_i\otimes t_i=\sum_j\tilde{s}_j\otimes\tilde{t}_j
\end{align}
(the number of summands in these two expressions may be different in general), then
\begin{align}
\nabla_X\left(\sum_is_i\otimes t_i\right)
=\nabla_X\left(\sum_j\tilde{s}_j\otimes\tilde{t}_j\right) & & (*)
\end{align}
Let $(e_{\alpha})$ and $(\epsilon_{\beta})$ be smooth local frames for $E$ and $F$ respectively. Then one can write
\begin{align}
s_i=s_i^{\alpha}e_{\alpha},\qquad
t_j=t_j^{\beta}\epsilon_{\beta},\qquad
\tilde{s}_i=\tilde{s}_i^{\alpha}e_{\alpha},\qquad
\tilde{t}_j=\tilde{t}_j^{\beta}\epsilon_{\beta}
\end{align}
(Einstein summation convention is assumed.) Then we will have
\begin{align}
\sum_is_i\otimes t_i
=\left(\sum_is_i^{\alpha}t_i^{\beta}\right)e_{\alpha}\otimes\epsilon_{\beta},
\qquad
\sum_j\tilde{s}_j\otimes\tilde{t}_j
=\left(\sum_j\tilde{s}_j^{\alpha}\tilde{t}_j^{\beta}\right)e_{\alpha}\otimes\epsilon_{\beta}
\end{align}
Since $\{e_{\alpha}\otimes\epsilon_{\beta}\}$ is a smooth local frame for $E\otimes F$, by uniqueness of local components we must have
\begin{align}
\sum_is_i^{\alpha}t_i^{\beta}=\sum_j\tilde{s}_j^{\alpha}\tilde{t}_j^{\beta} & & (1)
\end{align}
Taking exterior derivative we then have
\begin{align}
\sum_i\left(t_i^{\beta}ds_i^{\alpha}+s_i^{\alpha}dt_i^{\beta}\right)
=\sum_j\left(\tilde{t}_j^{\beta}d\tilde{s}_j^{\alpha}
+\tilde{s}_j^{\alpha}d\tilde{t}_j^{\beta}\right) & & (2)
\end{align}
Now let $\omega_{\alpha}^{\beta}$ and $\theta_{\alpha}^{\beta}$ be the connection 1-forms of $\nabla^E$ and $\nabla^F$ respectively, so that e.g.
\begin{align}
\nabla_X s_i=\left[Xs_i^{\alpha}+s_i^{\beta}\omega_{\beta}^{\alpha} (X)\right]e_{\alpha} & & (3)
\end{align}
and similar identities hold for $\nabla_Xt_i$, $\nabla_X\tilde{s}_j$ and $\nabla_X\tilde{t}_j$. Then we can compute
\begin{align}
&\nabla_X\left(\sum_is_i\otimes t_i\right) \\
%%%
&=\sum_i\left(\nabla_Xs_i\otimes t_i+s_i\otimes\nabla_Xt_i\right) \\
%%%
&=\underbrace{\left(\sum_i\left((Xs_i^{\alpha})t_i^{\beta}
+s_i^{\alpha}(Xt_i^{\beta})\right)\right)}_{=:I}e_{\alpha}\otimes\epsilon_{\beta}
+\underbrace{\left(\sum_is_i^{\gamma}t_i^{\beta}\right)}_{=:II}
\omega_{\gamma}^{\alpha}(X)e_{\alpha}\otimes\epsilon_{\beta}
+\underbrace{\left(\sum_is_i^{\alpha}t_i^{\gamma}\right)}_{=:III}
\theta_{\gamma}^{\beta}(X)e_{\alpha}\otimes\epsilon_{\beta}
\end{align}
where the first step follows by additivity and product rule, while the second step is obtained by substitution of (3) and rearranging the terms.
Now $\nabla_X\left(\sum_j\tilde{s}_j\otimes\tilde{t}_j\right)$ will have the same expression, except that all of the $s_i,t_i$ are replaced by $\tilde{s}_j,\tilde{t}_j$; says
\begin{align}
\nabla_X\left(\sum_j\tilde{s}_j\otimes\tilde{t}_j\right)
=\tilde{I}\cdot e_{\alpha}\otimes\epsilon_{\beta}
+\tilde{II}\cdot \omega_{\gamma}^{\alpha}(X)e_{\alpha}\otimes\epsilon_{\beta}
+\tilde{III}\cdot \theta_{\gamma}^{\beta}(X)e_{\alpha}\otimes\epsilon_{\beta}
\end{align}
Then:

*

*By (2), we have $I=\tilde{I}$.

*By (1), we have $II=\tilde{II}$ and $III=\tilde{III}$.

Hence, (*) holds as desired.
A: Here one should invoke the universal property for balanced maps:
view $\mathcal{C}^{\infty}(E)$ as left $\mathcal{C}^{\infty}(M)$ module, and $\mathcal{C}^{\infty}(F)$ as right $\mathcal{C}^{\infty}(M)$ (which we of course can, since everything is commutative).
Check that for your formula $\nabla((f \cdot s_E) \otimes s_F) = \nabla (s_E \otimes (s_F \cdot f))$ and bi-additivity hold, so that by the universal property we get a map of abelian groups: $$\mathcal{C}^{\infty}(E \otimes F) =\mathcal{C}^{\infty}(E) \otimes_{\mathcal{C}^{\infty}(M)} \mathcal{C}^{\infty}(F) \to \mathcal{C}^{\infty} (\wedge^1 M \otimes (E \otimes F)).$$Here we use the fact that for a commutative ring universality with respect to bilinear maps and with respect to balanced maps yields isomorphic objects (see, for instance, here).
Then one checks by hand that actually the map is $\mathbb{R}$-linear and Leibniz rule holds, thus we have a connection. 
