The Stacks project

Weakly proregular => QC({R/I^n}) = D_{comp}(R, I)

Tags: Added new tags

Also made some unimportant mostly invisible changes

Finish the proof

Decided to prove the lemma that

Rlim(M_n \otimes_R K_t) = Rlim(M_n \otimes_{K_n} K_t)

via an explicit comparison of the systems

(K_t) <----> (K_n \otimes_R K_t)

over the varying dgas K_n. On the one hand, you could claim that this
makes the proof "easier" as you only need to check some explicit
computations with complexes, but on the other hand this make the proof
harder to understand as it isn't just deduced from some general
principle... The reason for my choice is that I was having trouble
formulating a beautiful general principle underlying what is going on
here... Dear imaginary reader, maybe you can help?

Finished the proof

Thanks to Bhargav Bhatt for explaining how to get the unboubnded version
working like so.