[proofplan]
We prove both identities in a local gauge, where induced connections are written as ordinary derivatives plus the infinitesimal representation of the local connection one-form. The tensor identity follows by differentiating the [tensor product](/page/Tensor%20Product) representation, which gives the infinitesimal action as the sum of the two actions on the two factors. The dual identity follows similarly from the dual representation, whose infinitesimal action is the negative transpose action; this cancellation is exactly what makes the derivative of the scalar pairing split into the two covariant derivative terms. Since the identities are tensorial and hold in every local trivialization, they glue to global identities.
[/proofplan]
[step:Write the induced connections in a local gauge]
Let $\rho_V:G\to GL(V)$ and $\rho_W:G\to GL(W)$ denote the representations defining the associated vector bundles $E=P\times_G V$ and $F=P\times_G W$. Let $\mathfrak{g}:=T_eG$ denote the Lie algebra of $G$, where $e\in G$ is the identity element. Let
\begin{align*}
\omega \in \Omega^1(P;\mathfrak{g})
\end{align*}
denote the principal connection one-form on $P$, and let $\mathfrak{X}(U):=\Gamma(TU)$ denote the space of smooth vector fields on an [open set](/page/Open%20Set) $U\subset M$. Let $U \subset M$ be an open set admitting a smooth local section
\begin{align*}
\sigma: U \to P.
\end{align*}
Define the local connection one-form
\begin{align*}
A := \sigma^*\omega \in \Omega^1(U;\mathfrak{g}).
\end{align*}
The section $\sigma$ determines local trivializations
\begin{align*}
E|_U &\cong U \times V
\end{align*}
and
\begin{align*}
F|_U &\cong U \times W.
\end{align*}
Let
\begin{align*}
u:U \to V
\end{align*}
and
\begin{align*}
v:U \to W
\end{align*}
be the smooth maps representing $s|_U$ and $t|_U$ in these trivializations.
By the local formula in the definition of the induced connection on an associated vector bundle, using the convention that the local expression is ordinary differentiation plus the infinitesimal representation of $A(X)$, for a smooth vector field $X \in \mathfrak{X}(U)$ the induced covariant derivatives are represented by
\begin{align*}
\nabla_X^E s = X(u) + \rho_{V,*}(A(X))u
\end{align*}
and
\begin{align*}
\nabla_X^F t = X(v) + \rho_{W,*}(A(X))v,
\end{align*}
where $\rho_{V,*}:\mathfrak{g}\to\mathfrak{gl}(V)$ and $\rho_{W,*}:\mathfrak{g}\to\mathfrak{gl}(W)$ are the differentials of the representations at the identity element of $G$.
[/step]
[step:Differentiate the tensor product representation]
Let
\begin{align*}
\rho_{V \otimes W}:G \to GL(V \otimes W)
\end{align*}
be the tensor product representation defined by
\begin{align*}
\rho_{V \otimes W}(g)(a \otimes b) := \rho_V(g)a \otimes \rho_W(g)b
\end{align*}
for $g \in G$, $a \in V$, and $b \in W$. Let $I_V:V\to V$ and $I_W:W\to W$ denote the identity maps on $V$ and $W$, respectively. We claim that for every $\xi \in \mathfrak{g}$,
\begin{align*}
\rho_{V \otimes W,*}(\xi) = \rho_{V,*}(\xi)\otimes I_W + I_V \otimes \rho_{W,*}(\xi).
\end{align*}
Indeed, for $a \in V$ and $b \in W$, differentiating the curve
\begin{align*}
r \mapsto \rho_V(\exp(r\xi))a \otimes \rho_W(\exp(r\xi))b
\end{align*}
at $r=0$ gives
\begin{align*}
\rho_{V \otimes W,*}(\xi)(a \otimes b) = \rho_{V,*}(\xi)a \otimes b + a \otimes \rho_{W,*}(\xi)b.
\end{align*}
Since pure tensors span $V \otimes W$, the displayed operator identity follows.
[/step]
[step:Apply the local formula to the tensor product section]
In the local trivialization of $E \otimes F$ induced by $\sigma$ and the representation $\rho_{V \otimes W}$, the section $(s \otimes t)|_U$ is represented by the smooth map
\begin{align*}
u \otimes v:U \to V \otimes W.
\end{align*}
For $X \in \mathfrak{X}(U)$, the induced connection gives
\begin{align*}
\nabla_X^{E \otimes F}(s \otimes t) = X(u \otimes v) + \rho_{V \otimes W,*}(A(X))(u \otimes v).
\end{align*}
Using the ordinary product rule for the smooth map $u \otimes v$ and the infinitesimal tensor product identity from the previous step, we obtain
\begin{align*}
\nabla_X^{E \otimes F}(s \otimes t) = X(u)\otimes v + u\otimes X(v) + \rho_{V,*}(A(X))u\otimes v + u\otimes \rho_{W,*}(A(X))v.
\end{align*}
Grouping the $V$-factor terms and the $W$-factor terms gives
\begin{align*}
\nabla_X^{E \otimes F}(s \otimes t) = \bigl(X(u)+\rho_{V,*}(A(X))u\bigr)\otimes v + u\otimes \bigl(X(v)+\rho_{W,*}(A(X))v\bigr).
\end{align*}
By the local formulas for $\nabla^E$ and $\nabla^F$, this is
\begin{align*}
\nabla_X^{E \otimes F}(s \otimes t) = (\nabla_X^E s)\otimes t + s\otimes(\nabla_X^F t).
\end{align*}
[guided]
The point of the local calculation is to reduce the covariant derivative to a formula in vector spaces. In the gauge determined by $\sigma:U\to P$, the section $s$ is represented by a map $u:U\to V$, the section $t$ is represented by a map $v:U\to W$, and the tensor product section $s\otimes t$ is represented by
\begin{align*}
u\otimes v:U\to V\otimes W.
\end{align*}
The induced connection on $E\otimes F$ is not just the ordinary derivative of $u\otimes v$; it also includes the infinitesimal action of the local connection form $A=\sigma^*\omega$. Thus, for every vector field $X\in\mathfrak{X}(U)$,
\begin{align*}
\nabla_X^{E\otimes F}(s\otimes t)=X(u\otimes v)+\rho_{V\otimes W,*}(A(X))(u\otimes v).
\end{align*}
Now we compute each term. The ordinary derivative satisfies the usual product rule for the bilinear map $V\times W\to V\otimes W$, so
\begin{align*}
X(u\otimes v)=X(u)\otimes v+u\otimes X(v).
\end{align*}
The connection term is controlled by the differentiated tensor product representation. For $\xi\in\mathfrak g$, the identity
\begin{align*}
\rho_{V\otimes W,*}(\xi)=\rho_{V,*}(\xi)\otimes I_W+I_V\otimes\rho_{W,*}(\xi)
\end{align*}
gives, with $\xi=A(X)$,
\begin{align*}
\rho_{V\otimes W,*}(A(X))(u\otimes v)=\rho_{V,*}(A(X))u\otimes v+u\otimes\rho_{W,*}(A(X))v.
\end{align*}
Substituting both formulas into the local expression for the covariant derivative yields
\begin{align*}
\nabla_X^{E\otimes F}(s\otimes t)=X(u)\otimes v+u\otimes X(v)+\rho_{V,*}(A(X))u\otimes v+u\otimes\rho_{W,*}(A(X))v.
\end{align*}
We now group the terms according to which tensor factor they differentiate:
\begin{align*}
\nabla_X^{E\otimes F}(s\otimes t)=\bigl(X(u)+\rho_{V,*}(A(X))u\bigr)\otimes v+u\otimes\bigl(X(v)+\rho_{W,*}(A(X))v\bigr).
\end{align*}
The first parenthesis is exactly the local representative of $\nabla_X^E s$, and the second parenthesis is exactly the local representative of $\nabla_X^F t$. Therefore
\begin{align*}
\nabla_X^{E\otimes F}(s\otimes t)=(\nabla_X^E s)\otimes t+s\otimes(\nabla_X^F t).
\end{align*}
Since $X$ was arbitrary, this proves the tensor Leibniz identity on $U$ as an equality of $E\otimes F$-valued one-forms.
[/guided]
[/step]
[step:Differentiate the dual representation and compute the pairing]
Let
\begin{align*}
\rho_V^*:G\to GL(V^*)
\end{align*}
be the dual representation defined by
\begin{align*}
(\rho_V^*(g)\beta)(a):=\beta(\rho_V(g^{-1})a)
\end{align*}
for $g\in G$, $\beta\in V^*$, and $a\in V$. Let
\begin{align*}
\beta:U\to V^*
\end{align*}
be the smooth map representing $\alpha|_U$ in the dual trivialization.
For $\xi\in\mathfrak g$, differentiating
\begin{align*}
r\mapsto \rho_V^*(\exp(r\xi))\beta
\end{align*}
at $r=0$ gives
\begin{align*}
\bigl((\rho_V^*)_*(\xi)\beta\bigr)(a)=-\beta(\rho_{V,*}(\xi)a).
\end{align*}
Hence the local formula for the induced dual connection is
\begin{align*}
(\nabla_X^{E^*}\alpha)(s)=X(\beta)(u)-\beta(\rho_{V,*}(A(X))u).
\end{align*}
On the other hand,
\begin{align*}
\alpha(\nabla_X^E s)=\beta\bigl(X(u)+\rho_{V,*}(A(X))u\bigr).
\end{align*}
Adding these two expressions cancels the infinitesimal connection terms:
\begin{align*}
(\nabla_X^{E^*}\alpha)(s)+\alpha(\nabla_X^E s)=X(\beta)(u)+\beta(X(u)).
\end{align*}
The right-hand side is the ordinary derivative of the scalar function
\begin{align*}
\alpha(s):U\to\mathbb R
\end{align*}
represented by $x\mapsto \beta(x)(u(x))$. Therefore
\begin{align*}
(\nabla_X^{E^*}\alpha)(s)+\alpha(\nabla_X^E s)=d(\alpha(s))(X).
\end{align*}
Since $X$ was arbitrary, the one-form identity
\begin{align*}
d(\alpha(s))=(\nabla^{E^*}\alpha)(s)+\alpha(\nabla^E s)
\end{align*}
holds on $U$.
[guided]
The dual identity is the same local calculation, but with one important sign change. In the trivialization determined by $\sigma:U\to P$, the section $s$ is represented by $u:U\to V$, and the dual section $\alpha$ is represented by a smooth map
\begin{align*}
\beta:U\to V^*.
\end{align*}
The scalar function $\alpha(s):U\to\mathbb R$ is represented by the map $x\mapsto \beta(x)(u(x))$.
The dual representation is defined by
\begin{align*}
(\rho_V^*(g)\beta)(a):=\beta(\rho_V(g^{-1})a)
\end{align*}
for $g\in G$, $\beta\in V^*$, and $a\in V$. To compute its infinitesimal action, fix $\xi\in\mathfrak g$ and differentiate the curve $r\mapsto \rho_V^*(\exp(r\xi))\beta$ at $r=0$. Since $\exp(-r\xi)$ is the inverse of $\exp(r\xi)$, we obtain
\begin{align*}
\bigl((\rho_V^*)_*(\xi)\beta\bigr)(a)=-\beta(\rho_{V,*}(\xi)a).
\end{align*}
This negative sign is the mechanism that cancels the connection term from the derivative of $s$.
Using the local induced connection formula with $\xi=A(X)$, the dual covariant derivative satisfies
\begin{align*}
(\nabla_X^{E^*}\alpha)(s)=X(\beta)(u)-\beta(\rho_{V,*}(A(X))u).
\end{align*}
The original bundle connection gives
\begin{align*}
\alpha(\nabla_X^E s)=\beta\bigl(X(u)+\rho_{V,*}(A(X))u\bigr).
\end{align*}
Adding these two expressions, the terms containing $\rho_{V,*}(A(X))u$ cancel:
\begin{align*}
(\nabla_X^{E^*}\alpha)(s)+\alpha(\nabla_X^E s)=X(\beta)(u)+\beta(X(u)).
\end{align*}
The right-hand side is exactly the ordinary derivative in the direction $X$ of the scalar function $x\mapsto \beta(x)(u(x))$. Therefore
\begin{align*}
(\nabla_X^{E^*}\alpha)(s)+\alpha(\nabla_X^E s)=d(\alpha(s))(X).
\end{align*}
Since this holds for every $X\in\mathfrak X(U)$, it proves
\begin{align*}
d(\alpha(s))=(\nabla^{E^*}\alpha)(s)+\alpha(\nabla^E s)
\end{align*}
on $U$ as an equality of real-valued one-forms.
[/guided]
[/step]
[step:Glue the local identities to obtain the global identities]
The open set $U$ and the local section $\sigma:U\to P$ were arbitrary. Both sides of the tensor identity are globally defined smooth one-forms on $M$ with values in $E\otimes F$, and both sides of the dual identity are globally defined smooth real-valued one-forms on $M$. On every such trivializing open set, the preceding steps prove equality after applying the local bundle trivializations determined by $\sigma$.
Because a local trivialization is a fibrewise linear isomorphism, equality of the local representatives implies equality of the underlying bundle-valued one-forms over that open set. To make the overlap notation precise, let $U_i\subset M$ and $U_j\subset M$ be two trivializing open sets with smooth local sections
\begin{align*}
\sigma_i:U_i\to P
\end{align*}
and
\begin{align*}
\sigma_j:U_j\to P.
\end{align*}
Define the local connection one-forms
\begin{align*}
A_i:=\sigma_i^*\omega\in\Omega^1(U_i;\mathfrak g)
\end{align*}
and
\begin{align*}
A_j:=\sigma_j^*\omega\in\Omega^1(U_j;\mathfrak g).
\end{align*}
On an overlap $U_i\cap U_j$, let $g_{ij}:U_i\cap U_j\to G$ be the smooth gauge transformation determined by $\sigma_j=\sigma_i g_{ij}$. By the gauge transformation law for connection one-forms, the corresponding local connection forms satisfy
\begin{align*}
A_j=\operatorname{Ad}_{g_{ij}^{-1}}A_i+g_{ij}^{-1}dg_{ij}.
\end{align*}
Under this change of gauge, if $u_i:U_i\to V$ is the local representative of $s$ in the gauge $\sigma_i$, then the representative in the gauge $\sigma_j$ is obtained by applying $\rho_V(g_{ij}^{-1})$ pointwise; the same statement holds with $\rho_W$, $\rho_{V\otimes W}$, and $\rho_V^*$ for $t$, $s\otimes t$, and $\alpha$. Substituting these transformation rules together with the displayed transformation law for $A_i$ and $A_j$ into the local formula for the induced connection shows that the local covariant derivatives transform by the same transition functions as the underlying associated bundles. Therefore the two local expressions computed above agree on overlaps as representatives of the same globally defined bundle-valued one-forms. They therefore define global equalities of smooth one-forms with values in the indicated bundles:
\begin{align*}
\nabla^{E \otimes F}(s \otimes t) = (\nabla^E s)\otimes t+s\otimes(\nabla^F t)
\end{align*}
and
\begin{align*}
d(\alpha(s))=(\nabla^{E^*}\alpha)(s)+\alpha(\nabla^E s).
\end{align*}
This proves both assertions.
[/step]
