1

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.

Benjamin Wang
  • 226
  • 1
  • 9

1 Answers1

2

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.

Mario Carneiro
  • 1,548
  • 1
  • 18
  • 32