cannot apply succ_inj in succ_mul

[bombless]

its in the panel on the right, so my guess is it's a bug that the execution report error as "unknown identifier 'succ_inj'"

[user202729]

The panel could probably be improved (I think at the moment it actually lists everything that you have already unlocked?), but then you don't need that for this level anyway.

[bombless]

that's true, but that can also be a feature. just that you don't want to confuse the user

[joneugster]

Same as leanprover-community/lean4game#187