@AaronMazel-Gee Gaitsgory-Rozenblyum is not a good source. The appendices of that book rely on extremely difficult unproven combinatorial lemmas
It's maybe possible that Johnson-Freyd and Scheimbauer have proven some of them, but not enough to give you what Gaitsgory-Rozenblyum assert in the appendix
@FrankScience I can see two ways of proving that. One is via rational homotopy theory (use the fact that the homotopy groups of $H\mathbb{Q}\otimes_{\mathbb{S}}H\mathbb{Q}$ are given by $\mathrm{colim}_n H_{*-n}(K(\mathbb{Q},n); \mathbb{Q})$ to deduce that they are concentrated in degree 0)
The other, and maybe more natural, is to show that $H\mathbb{Q}$ is $\mathbb{S}$ with all primes inverted, since all positive homotopy groups of $\mathbb{S}$ are torsion
In particular, $-\otimes_{\mathbb{S}}H\mathbb{Q}$ is a smashing localization
