leanprover-community/NNG4

You have not unlocked the tactic 'generalizing' yet!

Closed this issue · 2 comments

mfornet commented

In the level mul_left_cancel (level 9 | advanced multiplication world) we need to start the proof (as suggested by the hint) with:

induction b with h hd generalizing c

and the game emits the following warning:

You have not unlocked the tactic 'generalizing' yet!
joneugster commented

Thanks for the report! This is indeed already fixed and will be in the live version when updating that to lean v4.6.0 at the end of the month.

  • 👍2
joneugster commented

Should be fixed in the version online, since a few weeks ago. Please reopen if you still experience any issues!

  • 👍1