When playing the Natural Number Game (in Lean), in Advanced Multiplication World Level 2/4, I used the following code. The last three lines seem to cause trouble.
cases a at h,
left,
refl,
cases b at h,
right,
refl,
left,
rw mul_succ at h,
rw add_succ at h,
exfalso,
apply succ_ne_zero (succ a * b + a),
exact h,
This finishes with no goals, but with the error invalid 'begin-end' expression, ',' expected, and so the level doesn't complete. Rewriting the apply using have p := succ_ne_zero _ h yields the same error.
Of course, I can look up a solution here, but what did I do wrong? Thanks.
The problem is a syntax error on the first line: cases a at h is not a valid input to the tactic. When you get the invalid 'begin-end' expression error the syntax is wrong so anything else it says is suspect.
You should use cases a instead; this already replaces a with 0 everywhere in the tactic state.