Let $M$ be a ctm of $ZFC$, and let $P$ be the poset $\prod_{n<\omega}^{\text{fin}} \text{Coll}(\omega,\aleph_n)$ as computed within $M$.
Let $G$ be $P$-generic over $M$. Let $G^{<n}\times G^{\ge n}$ be the image of $G$ under the natural isomorphism $P\cong P^{<n}\times P^{\ge n}$
Let $X=\bigcup_{n<\omega} \mathcal{P}(\omega)\cap M[G^{< n}]$.
I'd like to show that $X\neq \mathcal{P}(\omega)\cap M[G]$, i.e. there is some subset of $\omega$ in the big generic extension which is not added in any of the smaller ones. I'm puzzled because this forcing adds surjections $\omega\to\aleph_n^M$, so I don't know how to get reals into the mix.
Any hints on how to get started?
First of all, you really shouldn't be puzzled about how you can get reals! Reals are really easy to build from other data. For instance, given a map $\omega\to\omega_n^M$, you can get a real by composing it with any map $\omega_n^M\to 2$. Basically, the thing to keep in mind is that $M[G]$ doesn't just have $G$ added--it also has lots of other sets which can be "built" from $G$ or which encode the data of $G$ in different ways. A real is just a countable sequence of yes/no choices, and such countable sequences can be encoded inside other objects in tons of ways.
Now, you want a real that is not in $M[G^{<n}]$ for any $n$. Intuitively, this means the real cannot be constructed from finitely many of the surjections $\omega\to\omega_n^M$ which $G$ gives you, but instead can only be constructed if you really have all of them (or at least infinitely many of them). So, how could you define a real that uses data from all of the surjections $\omega\to\omega_n^M$ at once?