Maybe it's not something they would "typically miss", but, from proof by existence, it's something they sometimes miss.

It does speak to the benefits of using lean in that you don't need to be clever about the different examples you test.