Let $M$ and $N$ be topological spaces.
Let $\operatorname{Sh}(M)$ denote the presentable $\infty$-category of space-valued sheaves on $M$.
It seems to me that the equivalence
$$\operatorname{Sh}(M) \otimes \operatorname{Sh}(N) = \operatorname{Sh}(M \times N)$$
where $\otimes$ is the standard symmetric monoidal structure of $\operatorname{Pr^L}$, the $\infty$-category of presentable categories with left adjoints, is well-known.
However, I cannot find a proof in the literature.
My question is if there is a standard reference for this statement? Or if there is a "simple proof" of it by assuming some well-known results?
By the way, I believe that I was once told that it's in Lurie but I've failed to find it in either Higher Topos Theory or Higher Algebra.



Taking the category of sheaves is symmetric monoidal
1. Provided at least one of $M$ and $N$ is locally compact, the $\infty$-topos $\mathrm{Sh}(M \times N)$ is the product of $\mathrm{Sh}(M)$ and $\mathrm{Sh}(N)$ in $\mathrm{RTop}$. This is HTT 7.3.1.11.
2. Products in $\mathrm{RTop}$ can be computed as tensor products in $\mathrm{Pr^L}$. This is HA Example 4.8.1.19.


HA doesn't include a complete proof of the latter, but the case where one of the factors is of the form $\mathrm{Sh}(M)$ is essentially HTT 7.3.3.9, up to the matter of identifying $\mathrm{Sh}(M; \mathrm{Sh}(N))$ with the tensor product $\mathrm{Sh}(M) \otimes \mathrm{Sh}(N)$, for which HA 4.8.1.17 should be useful.


