Theorem on formal functions: Let $f:X\to Y$ be a projective morphism between noetherian schemes, $\mathcal{F}\in\textrm{Coh}(X)$, and $y\in Y$. Then the natural map $R^if_*(\mathcal{F})_y^\wedge\to\varprojlim H^i(X_n, \mathcal{F}_n)$ is an isomorphism for all $i\ge 0$. Here $X_n=X\times_Y \mathcal{O}_y/m_y^n$ and $\mathcal{F}_n$ is the pullback to $X_n$.
If I specialize to $i=0$ and don't take the limit, the map is $\varphi:f_*(\mathcal{F})\otimes \mathcal{O}_y/m_y\to f'_*(\mathcal{F}_1)$, where $f': X_1\to \text{Spec }\mathcal{O}_y/m_y$ is the base change. When I think about $\varphi$ with the rough analogy like integration along fiber, it seems that $\varphi$ itself might be an isomorphism. Thus, it would be enlightening to see a counterexample of $\varphi$ being an isomorphism. Additionally, a counterexample of the theorem when $f$ is not proper would be instructive too.
I tried a few simple examples like $\mathbb{A}^3\to \mathbb{A}^2$, $\mathbb{P}^1\times \mathbb{A}^1\to\mathbb{A}^1$, $\mathbb{A}^1-\{0\}\to\mathbb{A}^1$ (with structure sheaves) and each case $\varphi$ turned out to be an isomorphism.
Even some (flat) families that limit to a reducible or non-reduced fiber induce an isomorphism. I tried $Y=\text{Spec }k[t]$ with $X\subset\mathbb{P}_Y^2$ defined by $x_0x_1-tx_2^2=0$, as well as $X\subset\mathbb{P}_Y^1$ defined by $x_0^2-tx_1^2=0$. Special fibers are two lines and a double point respectively, and both sides of $\varphi$ well detected them.
