feat: add Nat.[shiftLeft_or_distrib, shiftLeft_xor_distrib, shiftLeft_and_distrib, testBit_mul_two_pow, testBit_mul_two_pow_gt, testBit_mul_two_pow_le, bitwise_mul_two_pow, shiftLeft_bitwise_distrib]

[luisacicolini]

This PR adds theorems Nat.[shiftLeft_or_distrib, shiftLeft_xor_distrib, shiftLeft_and_distrib, testBit_mul_two_pow, testBit_mul_two_pow_gt, testBit_mul_two_pow_le, bitwise_mul_two_pow, shiftLeft_bitwise_distrib], to prove Nat.shiftLeft_or_distrib by emulating the proof strategy of shiftRight_and_distrib.

In particular, Nat.shiftLeft_or_distrib is necessary to simplify the proofs in #6476.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2421f7f79941853da14346a234aec6df70cf36a1 --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-13 16:50:47)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2421f7f79941853da14346a234aec6df70cf36a1 --onto e9bd9807ef7a983365df9ac55d35040d0b2d5ef2. (2025-01-14 16:40:44)

[luisacicolini]

changelog-library

[luisacicolini]

I am especially skeptical about the testBit_mul_two_pow proof strategy, however, I could not find a better one.

[luisacicolini]

awaiting-review

[luisacicolini]

Thanks a lot @alexkeizer! I am not super confident with calc and suffices, so I'm not really sure I understand it. I'll give it a try for testBit_mul_two_pow_lt as well and push all the changes!