In proving the formal function theorem, Grothendieck uses a rather technical lemma in EGA 0-III.13:

**Lemma:** Let $\mathcal{F}_n$ be an inverse system of sheaves on a space $X$ with surjective transition maps such that there is a basis on which the $\mathcal{F}_n$ all have no cohomology, and such that $H^\bullet(X, \mathcal{F}_n)$ satisfies the ML condition for each index. Then the natural map
$$H^\bullet(X, \mathcal{F}) \to \varprojlim H^\bullet(X, \mathcal{F}_n)$$ is an isomorphism.

This is used to compare cohomology of the formal completion of a sheaf along a closed subscheme $Y$ with the limit of the pull-backs to the nilpotent thickenings $Y_n$. (The statement in EGA is actually a bit stronger, but in practice the sheaves are all quasi-coherent and at least for the application I have in mind, this suffices.)

I found the proof in EGA hard to digest: it uses the Godement resolution of a sheaf, flasqueness, as well as a result on inverse limits of complexes. Is there a cleaner, more natural approach to this result (e.g. using a spectral sequence possibly involving the derived functors of the inverse limit)?

Edit: OK, I just realized something: in the case where $X$ is separated (which is what matters for the fft), and the $\mathcal{F}_n$ are quasi-coherent, this is clear because we can just use a fixed Cech resolution (with respect to some affine cover) and then use the result in EGA on inverse limits of complexes. I'm still curious why the general result should be true though.

Edit 2 (and 3): Actually, my reasoning in the previous edit was incomplete. While it is then clear that, if the $\mathcal{F}_n$ are quasicoherent and $X$ separated, we have $H^\bullet(\mathfrak{A}, \mathcal{F}) = \varprojlim H^\bullet(\mathfrak{A}, \mathcal{F}_n)$, one should check that this is true for derived functor cohomology as well. But for this it suffices to show that the Cech cohomology is zero on any affine (for then one can "bootstrap" via the Cech-to-derived-functor spectral sequence as in EGA III.1 to see that derived functor cohomology of $\mathcal{F}$ is zero on any open affine, hence a Cech resolution by affines is sufficient), and this we have just checked. So formal arguments do handle the case of quasi-coherent sheaves. Sorry for the repeated edits!