 Idempotent-ultrafilter star-set lemma

For $A\in \mathcal{U}$ and an idempotent ultrafilter, put $A^{\ast }=\{n\in A:A-n\in \mathcal{U}\}$. Then $A^{\ast }\in \mathcal{U}$, and $A^{\ast }-n\in \mathcal{U}$ for every $n\in A^{\ast }$. For the second assertion, apply idempotence to $A-n$ and intersect its resulting good-translation set with $A-n$. This allows each new finite-sums generator to be chosen from finitely many translation constraints, proving the Idempotent-ultrafilter proof of Hindman's theorem.