I want to prove the Künneth formula with $\mathbb R$ coefficients using the Leray spectral sequence.
Let $f: X \times Y \to Y$ the projection map. Then we get a Leray spectral sequence $E^{p,q}_r \Rightarrow E^{p,q}_\infty$ where $$E_2^{p,q}= H^p(Y,R^qf_* \mathbb R), ~~~~~~~E^{p,q}_\infty=gr^p_F H^{p+q}(X\times Y,\mathbb R).$$
Further, the presheaf $R^qf_* \mathbb R$ is given by $U\mapsto H^q(f^{-1}(U), \mathbb R)$. Thus for $U$ contractible $$R^qf_* \mathbb R(U)= H^q(X\times U, \mathbb R) = H^q(X, \mathbb R).$$ In particular this is a locally constant sheaf. Then
$$E_2^{p,q} =H^p(Y,R^qf_* \mathbb R)= H^p(Y,H^q(X,\mathbb R)) \\=H^p(Y,\mathbb R) \otimes H^q(X,\mathbb R) ,$$ where in the last equlity I used the universal coefficient theorem.
I also have that $$H^{p+q}(X\times Y, \mathbb R)= \bigoplus_{p+q=k} E^{p,q}_\infty$$
So if $E^{p,q}_2=E^{p,q}_\infty$, the Künneth formula follows.
But how do I show the last part? Are there any mistakes in the above?
The projection $pr_1:X\times Y\rightarrow X$ induces a map of fibrations from $X\rightarrow X\times Y\xrightarrow{pr_2} Y$ to $X\xrightarrow{=}X\rightarrow\ast$, which in particular is an isomorphism on the fibre. Clearly the spectral sequence for $X\xrightarrow{=}X\rightarrow\ast$ collapses, with all differentials trivial. Naturality of the LS spectral sequence then allows you to use the previous map of fibrations to show that all the differentials of the spectral sequence for $X\rightarrow X\times Y\xrightarrow{pr_2} Y$ are trivial. Thus the sequence collapses at $E_2$ and we have $E_2^{p,q}\cong E_\infty^{p,q}$, as required.