Let $M,N$ be transitive models of sufficiently many $\operatorname{ZFC}$ axioms and let $$ \sigma \colon M[G] \prec N[H] $$ be an elementary embedding, where $G$ is $\mathbb P$-generic over $M$ for some forcing $\mathbb P \in M$, $H$ is $\mathbb Q := \sigma(\mathbb P)$-generic over $N$, $\sigma " G \subseteq H$ and $\sigma(G) = H$.
Question. $\sigma \restriction M \colon M \prec N$ ?
I was able to prove the above in a more specific setting and now I'm wondering under which circumstances the general result might fail.
edit: I added the requirement $\sigma(G) = H$ as this is the case that I'm most interested in.
Yes, because $M$ is definable with a parameter which depend on $\Bbb P$ in $M[G]$.
So $N$ is definable by the same formula say $\theta(x)$, with the image of the parameter (which is some $V_\delta$ for $\delta=|\Bbb P|^+$ if my memory serves me right).
Now suppose that $M\models\varphi(x)$, then $M[G]$ satisfies $\theta(x)$ and that the relativization of $\varphi(x)$ to the class defined by $\theta$ holds. Therefore $N[H]$ satisfies that as well, but $\theta$ defines $N$ in $N[H]$, so $N\models\varphi(\sigma(x))$.