On a certain isomorphism of coends Dear Mathstackexchange,
I am having trouble with understanding a proof in a certain document, I will write it out in detail here instead of referencing to a pdf (as I previously did).
Let $K$ be a simplicial set and X a simplicial object in a tensored and cotensored category $C$ that is enriched over simplicial sets. Let $|X|$ denote geometric realization of a simplicial object, i.e the functor tensor product of $\Delta$ and $X$. Let  $\otimes$ be the tensor in the category. If we have a tensor product of the form $\otimes_\Delta$ or similar, we refer to a functor tensor product, which is a  coend.
It is claimed that the isomorphism $K \otimes |X| \cong (K_\bullet \otimes_\Delta \Delta) \otimes (\Delta^\bullet \otimes_{\Delta^{op}} X_\bullet) \cong_! (\Delta^\bullet \times \Delta^\bullet) \otimes_{\Delta^{op}\times \Delta^{op}} (\amalg_{K_\bullet} X_\bullet)$ holds. I have problem seeing the iso which I marked as $\cong_!$. I suppose that this stems from the fact that the simplicial tensor preserves colimits, but I still don't see it, since we change variance and "juggle around" the terms. Something very explicit on what is done in this isomorphism would be appreciated.
 A: I did only half of the computation; but I went at least through $\cong_!$ :)
Here's the trick: it seems nothing but coend juggling and Yoneda lemma.
$$\begin{align*} 
K\otimes |X|&\cong \left(\int^m \Delta^m\cdot K_m\right)\otimes \left(\int^n \Delta^n\otimes X_n \right )\\
&\cong \int^{m,n}(\underbrace{\underbrace{K_m}_{\bf Set}\cdot\underbrace{\Delta^m}_{\bf sSet}}_{\bf sSet})\otimes (\underbrace{\underbrace{\Delta^n}_{\bf sSet}\otimes X_n}_{\cal M})\\
(1)&\cong \int^{m,n} \big[\left(K_m\cdot \Delta^m \right )\times \Delta^n \big]\otimes X_n\\
(2)&\cong \int^{m,n} \big[ K_m\cdot(\Delta^m\times\Delta^n)\big]\otimes X_n\\
(3)&\cong \int^{m,n}\underbrace{(\Delta^m\times\Delta^n)}_{:=Y^{m,n}_\bullet}\otimes (K_m\cdot X_n)
\end{align*}$$
(3) is in fact what you want to justify.  I hope not to be wrong if I say that it follows from
$$
\left(\coprod_{K_m} Y^{m,n}_\bullet \right )\otimes X_n\cong \coprod_{K_m}\big( Y^{m,n}_\bullet\otimes X_n\big)\cong Y^{m,n}_\bullet\otimes \left(\coprod_{K_m} X_n \right )
$$
(1) follows from the well known isomorphism $(V\otimes W)\boxtimes X\cong V\boxtimes(W\boxtimes X)$
(2) Follows from the fact that products commute with the dot operation, which is a colimit.
Everything seems simply to be commutativity of tensors with (the) colimits (defining the $\bf Set$-tensoring).
