I am not aware of built-in facilities for vector calculus at this level of abstraction. There may be ready-made packages around. However, we can roll out a version using pattern replacement rules:

scalarQ[_?NumberQ] := True;
divRules = {myDiv[(s_ /; scalarQ[s])*v_, x_] /; FreeQ[s, x] :> 
    s*myDiv[v, x],
   myDiv[v1_ + v2_, x_] :> myDiv[v1, x] + myDiv[v2, x],
   myDiv[(s_ /; scalarQ[s])*v_, x_] :> 
    s*myDiv[v, x] + myDot[myGrad[s, x], v],
   myDiv[myCross[v1_, v2_], x_] :> 
    myDot[v2, myCurl[v1, x]] - myDot[v1, myCurl[v2, x]]};
renderRules = {myDiv -> Inactive[Div], myDot -> Inactive[Dot], 
   myGrad -> Inactive[Grad], myCross -> Inactive[Cross],
   myCurl -> Inactive[Curl]};
scalarQ[s1] = True;
scalarQ[s2[__]] = True;
expr = s1*v[t, x] + v2[t, x] + s2[t, x]*v3[t, x] + 
   myCross[v4[t, x], v5[t, x]];
expr /. renderRules
myDiv[expr, x] //. divRules /. renderRules

Maybe the identity involving the divergence of a tensor product can be proved by making the algebraic computation of the partial derivatives, assuming T1 = Through[{f1, f2, f3}[x1, x2, x3]] etc.