Extra help for 0 * m = m

[Timmmm]

I got a bit stuck on this level. Probably missing something obvious but you might want to add a "show more help" for it. It doesn't seem like there is any way to get the solution if you are stuck at all?

[Timmmm]

Ah I figured it out. There were a couple of minor footguns in the way:

1. I thought "maybe you solve this with induction", but I tried induction m by d hd and nothing happened. I dunno if that is valid syntax or something, but I took the "nothing" response to mean something like "you can't do that". Of course I didn't realise it's actually with for about 15 minutes. Could this show an error message instead?

2. I was slightly thrown off the induction scent by the description saying that we want to solve the mul_comm goal by induction, sort of slightly implying that you don't need induction for the 0 * m = m goal.

I would:

1. If you can, show an error message for induction m by d hd. Even if it's a very hacky regex hint induction\s+\w+\s+by "did you mean induction with?"
2. Either add a show more help that says "you need to use induction here", or just put in the description something like "note, you can use induction to prove inductive goals".

Fantastic site by the way - I've read a few Lean tutorials and it all seemed pretty incomprehensible until I found this site.

[joneugster]

It's unfortunate that parsing errors like induction m by d hd are sometimes handled pretty randomly in Lean. Also, the game is currently on a 6 month old Lean, so hopefully once we manage to update, some of these will be handled in a more robust way (as Lean itself constantly improves)

2. could be a PR to the natural number game: https://github.com/leanprover-community/nng4. This repo here only does the engine running the games