Lurie characterizes the symmetric monoidal structure on $\mathsf{Sp}$ by a universal property (HA.4.8.2.19): it is uniquely determined up to a contractible space of choices by the property that $S^0$ is the unit and $\wedge$ commutes with homotopy colimits in both variables.

I think on first glance this sounds like one of those formal things that doesn't help you 'compute' anything, but I claim that (i) you can get all the computational mileage out of this that you usually get from model categories of spectra and (ii) if you like, you can easily show that your favorite symmetric monoidal model category of spectra models this symmetric monoidal structure.

We'll start with (ii) since that's what you asked about, and it's easier. Suppose you have a model category $\mathbf{M}$ which models spectra (which is something else that can be checked easily from universal properties by its relationship to some model for $\mathsf{Spaces}$, for example). Suppose further that it's a symmetric monoidal model category. Then the underlying $\infty$-category $\mathsf{M}[W^{-1}] \cong \mathsf{Sp}$ inherits a symmetric monoidal structure. To compare it with the 'universal' one, one needs to check that the tensor product commutes with homotopy colimits and that the unit is weakly equivalent to the sphere spectrum. The unit requirement is just always satisfied (otherwise what sort of spectra are you using??) and the homotopy colimit requirement is also always satisfied, because part of the definition of being a symmetric monoidal model category is that $\otimes$ be a left Quillen bifunctor- and that forces the tensor product to commute with homotopy colimits in both variables.

Now let's talk about (i). What does it even mean to 'understand' the smash product of spectra? Well, usually the way a spectrum is handed to us is as a sequence of (say, pointed) spaces $(X_k)$ and maps $\Sigma X_k \to X_{k+1}$. Every model ever includes at least that much data, often with all sorts of extra requirements and structure. But in any case, this data presents a spectrum $X = \mathrm{hocolim}_k \Sigma^{-k}\Sigma^{\infty}X_k$. So, from the universal property we learn that $$ X \wedge Y = \underset{j,k}{\mathrm{hocolim}}\, \Sigma^{-j-k}\left( \Sigma^{\infty}X_j \wedge \Sigma^{\infty}Y_k\right). $$ So now we'd better figure out how to compute $\Sigma^{\infty}A \wedge \Sigma^{\infty} B$ for pointed spaces $A$ and $B$. It's possible to argue very abstractly that $\Sigma^{\infty}$ must be symmetric monoidal, using the methods in HA.4.8.2, but you can also argue as follows: first reduce to the unpointed case, so we want to compute $\Sigma^{\infty}_+A \wedge \Sigma^{\infty}_+B$. But $A$ and $B$ are homotopy colimits of constant diagrams shaped like $A$ and $B$, respectively. And $\Sigma^{\infty}_+$ commutes with homotopy colimits. A little string of equivalences and the fact that $\Sigma^{\infty}_+(*) = S^0$ is the unit gives the result.

Excellent, so just from nonsense we learn that $\Sigma^{\infty}$ is symmetric monoidal. Moving back to our original formula we learn that a 'concrete' computation for the smash product is:

$$X \wedge Y = \underset{j,k}{\mathrm{hocolim}}\, \Sigma^{-j-k}\left( \Sigma^{\infty}X_j \wedge \Sigma^{\infty}Y_k\right) = \underset{j,k}{\mathrm{hocolim}}\, \Sigma^{-j-k}\left( \Sigma^{\infty}(X_j \wedge Y_k)\right).\quad (1)$$

If you like, then at this point you could pick your favorite cofinal copy of $\mathbb{N}$ inside $\mathbb{N} \times \mathbb{N}$ and present this smash product as a sequence of spaces with maps from the suspension of one to the next.

This way of thinking about the smash product is the very original one, going back to Boardman and Adams. Of course they ran into all sorts of technical issues verifying all the properties they wanted out of a symmetric monoidal structure. What happened to those? Well, when dealing with a symmetric monoidal structure one would like (a) properties and (b) the ability to 'compute' what the thing does. The original approach was to begin with (b) and then work hard to verify (a). In the present situation, one begins with (a) using various levels of sophistication and then deduces (b). Of course, lots of technical work went into producing the symmetric monoidal $\infty$-category $\mathsf{Sp}$! But the work pays off: you get a much stronger theorem and a more flexible theory.

Let me go into a bit more detail about comparing with, say, the formula for the smash product one finds for orthogonal spectra. I claim that it is a particular model-categorical presentation of precisely the formula (1). To justify that, I'm going to compare the two formulae directly. So I'll need to review a bit about orthogonal spectra. Recall that an **orthogonal spectrum** consists of a sequence of pointed spaces $X_n$ equipped with $O(n)$-actions together with compatible, $O(n)\times O(m)$-equivariant, based maps $X_n \wedge S^m \to X_{n+m}$. Given an orthogonal spectrum, one would like to know how to describe the corresponding object in $\mathsf{Sp}$ and how to understand smash products.

We'll take the $\infty$-category $\mathsf{Spaces}$ as 'understood' and the functor $\Sigma^{\infty}$ as also understood. Then an orthogonal spectrum $(X_k)$ presents an object of $\mathsf{Sp}$ by the formula $$X = \underset{\mathbb{N}}{\mathrm{hocolim}}\, \Sigma^{-k}\Sigma^{\infty}X_k$$ Of course, we ignored the orthogonal group action. Luckily, here's a fun fact:

**Fun fact.** Let $\mathsf{Orth}$ denote the $\infty$-category of real inner product spaces and isometric embeddings. Then the inclusion $\mathbb{N} \to \mathsf{Orth}$ is homotopy final.

It follows that we may compute the homotopy colimit either over $\mathsf{Orth}$ or over $\mathbb{N}$. That's important, because the formula for the smash product of orthogonal spectra is really trying to be a formula for a homotopy colimit over $\mathsf{Orth} \times \mathsf{Orth}$. I won't bother typesetting the formula here (see page 5 of Schwede's book, for example) but unless I'm mistaken one arrives at this formula as follows:

- Take the formula in (1) and replace the homotopy colimit over $\mathbb{N} \times \mathbb{N}$ by a homotopy colimit over $\mathsf{Orth} \times \mathsf{Orth}$.
- To compute that homotopy colimit, we are free to first left Kan extend along $\oplus: \mathsf{Orth} \times \mathsf{Orth} \to \mathsf{Orth}$.
- Stare at the pointwise formula for the left Kan extension evaluated at $\mathbb{R}^n$, and you become interested in a homotopy colimit along all pairs $p+q = n$ together with actions of $O(p) \times O(q)$ etc.
- Now suspend everything n times, erase the $\Sigma^{\infty}$'s, and use one of the standard formulas for computing a homotopy colimit as an ordinary colimit in some model category, and you should get (with cofibrancy conditions if you want the right homotopy type) the previously mentioned formula in the linked book.

The same thing works in symmetric spectra, except that the claim about finality is false. Instead, one uses a cofibrancy condition that allows a lemma of Bökstedt to apply so you can replace $\mathbb{N}$ with the category of finite sets and injections.

the $E_\infty$-structure, i.e. provide all required associators, commutators, twistors and higher coherences between different products. Even stating it precisely isn't simple, thus a very abstract approach is required. The classical theories encode $E_\infty$-action in explicit geometric objects like actions of orthogonal or symmetric groups, so remaining structure is commutative "on the nose". $\endgroup$