It's embarrassing, I've never learned to do this on the command line.
I have a directory full of images:
image0001.png
image0002.png
image0003.png
...
And I would like a one-liner to rename them to (say).
0001.png
0002.png
0003.png
...
How do I do this?