Drinfeld's lemma measures the failure of the K\"unneth formula for the \'etale fundamental group of schemes in characteristic $p>0$ in terms of equivariance data under partial Frobenius morphisms. In this note, we promote Drinfeld's lemma to a K\"unneth type equivalence of derived categories of constructible Weil sheaves with $\bar F_\ell$-coefficients or $\bar Q_\ell$-coefficients for $\ell\not = p$.