Add missing explicit description of derived completion

We tried to do as much as possible with the extended alternating Cech
complex, because it is technically easier to work with, but putting this
in will perhaps help convince the reader that derived completion is in
some sense a completion. Also, we'll use it in the next commit.
Rf_* commutes with derived limits

Not sure why this wasn't yet in the Stacks project!
Thanks to Bhargav Bhatt for private communication.
Rf_* commutes with derived completion

This clarifies some of the issues that happen when you consider the
derived pushforward of a derived complete complex. See also the next
commit.
Derived completion of pseudo-coherent complex over Noetherian ring
Unfinished remark on formal formal functions theorem

This commit tries to explain something that was explained to me by
Preygel and Halpern-Leistner, but I fear I didn't understand...