(masked) trunc (lshr X, ShiftC) --> (masked) lshr (trunc X), C
Narrowing the shift should be better for analysis and can lead to follow-on transforms as shown.
Attempt at the general proof in Alive2:
https://alive2.llvm.org/ce/z/tRnnSF
Here are a couple of the specific tests:
https://alive2.llvm.org/ce/z/bCnTp-
I think this is only part of the check.
https://alive2.llvm.org/ce/z/59fb7i => https://alive2.llvm.org/ce/z/s_G7u7