The space of theorems that are "very routine and not requiring any ideas" is actually pretty interesting. In particular, compilers do quite a lot of theorem-proving of the "these functions are equivalent" variety, and it's way more elaborate than most people imagine.