use `#check_failure` command to erase errors

[Seasawher]

see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/the.20metaprogramming.20book/near/386542851

There seems to be an intentional error in the code, which will be an obstacle when you try to update Lean version later.

As a way to indicate errors while avoiding them, I suggest the following.

• Import std and use #guard_msgs. Use --# to ensure that they don't remain in markdown.
• Use #check_failure.
• comment out the relevant section.

This PR pointed out where errors can be avoided simply by using #check_failure.I would like to hear your views on where check_failure cannot be used.

Thank you.