Computation of a homotopy colimit of pro-spectra Suppose $E\simeq\text{hocolim}_iE_i$ is a filtered homotopy colimit. Suppose $X=\{X_j\}_j$ is a pro-space (assume some finiteness conditions on the spaces or spectra if you have to...for example, assume $X_i$ are simplicial sets with finitely many simplicies in each degree). Is it true that in the $\infty$-category of pro-spectra, we have $\text{hocolim}^{pro}_i\{E_i\wedge X_j\}_j\simeq \{\text{hocolim}_i(E_i\wedge X_j)\}_j$? More generally, is it true that if $E_i$ are pro-spectra with some mild finiteness condition and all indexed by the same cofiltered diagram, then I can compute their homotopy colimit degreewise?
 A: This is not true, unfortunately. Here's an example.
Let $E_i$ be the directed system
$$
\DeclareMathOperator{\hocolim}{hocolim}
\DeclareMathOperator{\holim}{holim}
S^0 \to S^0 \vee S^1 \to S^0 \vee S^1 \vee S^2 \to \dots
$$
of wedge inclusions, and let $X_j$ be the inverse system
$$
S^0 \leftarrow S^0 \vee S^1 \leftarrow S^0 \vee S^1 \vee S^2 \leftarrow \dots
$$
of projections. Both are systems of objects of finite type, and both the homotopy limit and homotopy colimit are also of finite type.
We also have a natural isomorphism
$$
Map(E_i \wedge X_j, F) \cong \bigoplus_{k=0}^i \bigoplus_{l = 0}^j Map(S^{i+j}, F).
$$
Let $F$ be any spectrum, viewed as a constant pro-object. Then we can show that the two spectra you describe are different by calculating homotopy classes of maps out to $F$:
$$
\begin{align*}
Map_{pro}(\{\hocolim_i(E_i\wedge X_j)\}_j, F) &= \hocolim_j \holim_i Map(E_i \wedge X_j, F)\\
Map_{pro}(\hocolim^{pro}_i\{E_i\wedge X_j\}_j, F) &= \holim_i \hocolim_j Map(E_i \wedge X_j, F)
\end{align*}
$$
Thus, we have isomorphisms
$$
\begin{align*}
[\{\hocolim_i(E_i\wedge X_j)\}_j, F]_{pro} &= \bigoplus_l \prod_k  \pi_{k+l}(F)\\
[\hocolim^{pro}_i\{E_i\wedge X_j\}_j, F]_{pro} &= \prod_k \bigoplus_l \pi_{k+l}(F)
\end{align*}
$$
In particular, the natural map from the top to the bottom is not an isomorphism unless the homotopy groups of $F$ are zero above a certain degree.
As you can see, finiteness properties on the $E_i$ or $X_j$ don't buy you what you need. If you are taking a hocolim over a finite diagram instead (pushouts, finite wedges, things built from those by finitely many steps), then the fact that the category of pro-spectra is stable allows you to move the homotopy colimit inside the inverse system.
