Fixed a few more suggestions from Vivek and added some detail to the lemma