exact? finds levels own theorem, allowing progress on some levels

[SeseMueller]

When running a level, the exact? tactic is able to find the levels own theorem (which we are trying to prove) as a solution. While writing out the solution as the tactic suggests is correctly flagged as not allowed, the level allows progress, as the exact? has (technically) closed the goal.

Thus, there is a simple way to play through a lean4game:

1. Start playing until you unlock exact
2. Go into editor mode
3. Type exact?
4. Move to next level

Note that this only works on some levels and not on others; I can't find a pattern for that because I don't have good insight into the inner workings of the lean4game.

This doesn't look intended, but a learning user will most likely not know exact?, making this a probably useless edge case.

[TentativeConvert]

This is related to https://github.com/leanprover-community/lean4game/issues/299. The plan is that in future versions of lean4game, enabling exact will no longer automatically enable exact?, see https://github.com/leanprover-community/lean4game/pull/304#issuecomment-2708478515. That should solve this issue.