Does the derivation follow a sort of Leibniz's Rule for a tensor product?
$ \displaystyle \frac {\partial} {\partial t} \left ( A_t \otimes B_t \right) \overset ? = \frac {\partial A_t} {\partial t} \otimes B_t + A_t \otimes \frac {\partial B_t} {\partial t}$
Why am I asking that? Because if it was true, then the solution of the Schrodinger equation in operator form:
$$ i \hbar \frac \partial {\partial t} U(t) = H \ U(t)$$
for any Hamiltonian in the form $H = H_o \otimes \mathbb I_s + \mathbb I_o \otimes H_s$ would admit a factorized solution $U(t) = U_o(t) \otimes U_s(t)$, where $U_{o,s}(t)$ solves $\displaystyle i \hbar \frac \partial {\partial t} U_{o, s}(t) = H_{o, s}U_{o, s}(t)$.
Proof. $ \displaystyle { i \hbar \frac {\partial} {\partial t} U(t) = \\ {i \hbar \frac {\partial U_o(t)} {\partial t} \otimes U_s(t) + U_o(t) \otimes i \hbar \frac {\partial U_s(t)} {\partial t} =} \\ {H_oU_o(t) \otimes U_s(t) + U_o(t) \otimes H_sU_s(t) =} \\ {\left ( H_o \otimes \mathbb I_s \right )\left (U_o(t) \otimes U_s(t) \right ) + \left (\mathbb I_o \otimes H_s \right ) \left ( U_o(t) \otimes U_s(t)\right )=} \\ {\left ( H_o \otimes \mathbb I_s + \mathbb I_o \otimes H_s \right ) \left ( U_o(t) \otimes U_s(t)\right )=} \\ H \ U(t)} $
As peek-a-boo said in the comments, this product rule is true and follows along the same lines as the usual product rule. In this particular case one can also apply the usual product rule (for products of operators). Just note that $$ A_t\otimes B_t=(A_t\otimes I)(I\otimes B_t) $$ and the maps $X\mapsto X\otimes I$, $Y\mapsto I\otimes Y$ are bounded linear maps. Thus \begin{align*} \frac{d}{dt}(A_t\otimes B_t)&=\frac{d}{dt}(A_t\otimes I)(I\otimes B_t)\\ &=(\dot A_t\otimes I)(I\otimes B_t)+(A_t\otimes I)(I\otimes \dot B_t)\\ &=\dot A_t\otimes B_t+A_t\otimes \dot B_t. \end{align*}