Natural Number Game: add_sq ends with error?

Stream: new members

[apnorton]

I'm trying to go through the natural number game to get a bit of exposure to Lean, but I'm getting a bit stuck on Power World 9/10 (add_sq) --- it seems the prover wants to just "stop" part-way through, but it does not let me navigate to the end of the problem.

My (start of) a proof is this:

repeat rw [pow_two]
repeat rw [mul_add]
repeat rw [add_mul]
rw [mul_comm ba ]

...and when I view this in the terminal view, it says "Level completed with warnings :performing_arts:" and won't let me go forward. In the typewrite view, it just shows me this (screenshot below):
image.png

[apnorton]

(i.e. there's no "next line" to enter further text, but the level is also not complete)

If anyone could point me in the right direction/help me understand what I'm doing wrong, I'd be very appreciative. :)

[Kevin Buzzard]

There's no such thing as ba so rw [mul_comm ba ] should be some kind of error but for whatever reason it's just giving you something incomprehensible. Do you mean mul_comm b a?

[apnorton]

Ahhh! That's exactly what I meant. I think the lack of any error message confused me; e.g.:
image.png

[apnorton]

Correcting it so I have mul_comm b a brought it back to a state I could work with, and I could proceed. :) Ty so much!

[apnorton]

:o and I just realized you're the person who made the game! Thank you also for making this, because it's been a lot of fun and informative :)