In John Rognes' Galois theory monograph he constructs something called the Hopf-cobar complex for a coalgebra object $H$ (in spectra) and a comodule algebra $X$. It is, intuitively, the object whose totalization computes the (global sections of the structure sheaf of the...) quotient of $Spec(X)$ under the action of $Spec(H)$, if $X$ is a commutative ring spectrum. In degree $n$ it looks like $X\wedge H\wedge\ldots H$, with $n$ copies of $H$. The coface maps are given by either the coaction of $H$ on $X$, the diagonal map of $H$, or the unit map of $H$. Codegeneracies are given by either applying the counit of $H$ or the multiplication of $H$. This can be thought of as an explicit construction for the "cotensor product" of $X$ and $\mathbb{S}$ as $H$-comodules. This can in fact be made quite explicit if one works in a suitable framework for coalgebraic structure (e.g. this).
On the other hand, if $X$ is a commutative ring spectrum, there is something called the Amitsur complex for $X$. In degree $n$ this has the form of $X\wedge X\wedge\ldots\wedge X$, $n+1$-copies of $X$. The coface maps here are given by using the unit of $X$, and the codegeneracies are given by the multiplication on $X$. This is not really given as any kind of tensor product, but rather as the effect of iterating a monad (the one given by tensoring with $X$) on $\mathbb{S}$ over and over again and considering the resulting cosimplicial resolution.
In Proposition 12.1.8 of the aforementioned monograph (available here), Rognes proves that if we have an equivalence $X\wedge X\to X\wedge H$ given by $$X\wedge X\overset{1\wedge\Delta}\to X\wedge X\wedge H\overset{\mu\wedge 1}\to X\wedge H,$$ we can iterate this at each level to produce a cosimplicial equivalence between the two cosimplicial objects I described above (see Definition 12.1.7 op. cit.). He remarks that a diagram chase is necessary to show that this map is in fact cosimplicial, and moreover that it uses strict coassociativity and counitality of $H$.
My question is the following: can one deduce the above equivalence in the setting of a quasicategories when one does not have recourse to a diagram chase, especially not one requiring strict commutativity of diagrams? It would seem that doing this in this setting would require having a deeper understanding of what those two cosimplicial objects are.
