We develop algorithms to prove peephole optimzations correct in a bitwidth-generic fashion, and apply it to hacker's delight, rewrites mined from InstCombine, and challenging problems from program deobfuscation. We explain the core ideas of the algorithm, as well as the implementation, evaluation, and proofs which we performed in the Lean proof assistant. Finally, we demo the interface to the end-user, which provides a command (bv_automata) to prove theorems about bitvector rewrites that are universally quantified over the bitwidth. We hope to use our algorithm to simplify the many thousands of lines of proof in the Lean bitvector standard library, and more broadly, hope to provide effective proof automation for bitvector predicates that quantify over bitwidth.