Let $\lambda$ be a large enough regular cardinal, $\mathbb{P}\in M\prec H_\lambda$, with $M$ countable and $\mathbb{P}$ proper. Let $G$ be $\mathbb P$-generic over the ground model $V$. Let $\pi:M\cong \bar M$ be the Mostwoski collapse. Write $\bar{\mathbb{P}}=\pi(\mathbb{P})$, $\bar G=\pi''G$. Does it follow that
$$
\overline{M[G]}=\bar{M}[\bar G]?
$$
Here, $M[G]=\{x_G:x\in M\}$, where $x_G$ is the interpretation of $x$ according to $G$, in the usual sense, and $\overline{M[G]}$ is the Mostowski collapse of $M[G]$. The RHS makes sense because $\bar G$ is $\bar{\mathbb P}$-generic over $\bar M$, by elementarity.
I've tried lifting $\pi$ to an isomorphism $M[G]\to \bar M[\bar G]$. This would be enough, because $\bar M[\bar G]$ is transitive. The natural definition would be $\dot x_G\mapsto (\pi(\dot x))_{\bar G}$, where $\dot x\in M$. But, one needs to verify that this is well defined:
Let $\dot x,\dot y\in M$ with $\dot x_G=\dot y_G$. By the Truth Lemma, there is some $p\in G$ with $p\Vdash \dot x=\dot y$. If $p$ were to belong to $M$; then we would be done because we can apply $\pi$ to the statement $M\models (p\Vdash \dot x=\dot y)$, but this need not be the case. One can say
$$
H_\lambda \models \exists q\in \mathbb{P}(q\Vdash \dot x=\dot y)
$$
and so there is some $q\in M$ with $q\Vdash \dot x=\dot y$, but $q$ might not be in $G$. Properness seems highly relevant here, since we want an object in $M\cap G$, but I haven't been able to produce it.
If $p\in G$ and $p\Vdash \dot x=\dot y$, then
$$
D:=\{q\le p:q\Vdash M\cap \dot G\neq\emptyset\}\in V
$$
is dense below $p$ because $\mathbb{P}$ is proper. Therefore, $G\cap D\neq\emptyset$ by genericity, say $q\in G\cap D$. Then $q\Vdash M\cap \dot G\neq \emptyset$, so there is some $r\in M\cap G$. But now we don't necessarily know that $r\Vdash \dot x =\dot y$.
Best Answer
In general, $\overline{M[G]}\neq \bar M[\bar G]$. The problem is that while $G$ meets any dense $D\subseteq\mathbb P$ with $D\in M$, $G$ is not necessarily $M$-generic in the sense that $G$ meets $D$ inside $M$, even if $\mathbb P$ is proper.
Suppose for example that $\mathbb P=\mathrm{Add}(\omega_1, 1)$ is the canonical $\sigma$-closed forcing to force a new subset of $\omega_1$. Let $\alpha=M\cap\omega_1$ and note that this is a countable ordinal. Now consider the condition $p:\alpha\rightarrow 2$ that is constant with value $0$ and suppose $p\in G$. Intuitively, "$p$ makes sure that there is only $M$-trivial information in $G\cap M$".
Proof: Let $H=\{q\in\mathrm{Add}(\omega_1, 1)\mid q$ is constant with value $0\}$. Then $p\in G$ ensures that $G\cap M$ is exactly $H\cap M$ and hence $\bar G=\pi[G\cap M]=\pi[H\cap M]$. However, $H\in M$ and thus $\pi[H\cap M]=\pi(H)\in\bar M$ so that $\bar M=\bar M[\bar G]$. On the other hand $G\in M[G]\setminus M$ implies $\overline{M[G]}\neq \bar M$.$\square$
This problem can easily be mitigated for proper forcing if one assumes that there is an $(M,\mathbb P)$-generic condition $p\in G$. In this case $G\cap M\cap D\neq\emptyset$ for any dense $D\subseteq \mathbb P$ with $D\in M$ and your attempt in the question goes through: For any $\dot x, \dot y\in M^\mathbb P$ the set $$D=\{p\in\mathbb P\mid p\Vdash\dot x=\dot y\vee p\Vdash\dot x\neq\dot y\}$$ is dense and in $M$. Hence there is $p\in M\cap G$ deciding whether $\dot x=\dot y$. As indeed $\dot x_G=\dot y_G$, we must have $p\Vdash \dot x=\dot y$.