Incorrect. The statement in Lean can itself be wrong. Moreover, they could be exploiting a kernel bug in Lean, of which we had one published literally a week ago.