Yes, everyone is aware that the statement needs to be checked. No one has suggested otherwise. It goes without saying. The "magic" of lean is that (in princi

Yes, everyone is aware that the statement needs to be checked. No one has suggested otherwise. It goes without saying. The "magic" of lean is that (in principle, assuming lean is sound and the proof is verified) that is all you have to check by hand. That is a big deal.