remove import Mathlib.Tactic

[kbuzzard]

import Mathlib.Tactic pulls in a huge amount of mathlib (there are many domain-specific tactics).

Before this PR:

buzzard@brutus:~/lean-projects/NNG4$ lake clean
buzzard@brutus:~/lean-projects/NNG4$ lake build
...
[109/2085] Building Mathlib.Tactic.Widget.SelectInsertParamsClass
[110/2085] Building Mathlib.Tactic.Variable
[111/2085] Building Mathlib.Tactic.UnsetOption
[112/2085] Building Mathlib.Tactic.TypeCheck
[113/2085] Building Mathlib.Tactic.Trace
[114/2085] Building Mathlib.Util.WhatsNew
...

After this PR you can build the entire project without even downloading mathlib cache very quickly:

buzzard@brutus:~/lean-projects/NNG4$ lake clean
buzzard@brutus:~/lean-projects/NNG4$ lake build
 ...
[349/352] Building Game.Levels.AdvMultiplication.L10mul_right_eq_self
[350/352] Building Game.Levels.AdvMultiplication
[351/352] Building Game
stdout:
i18n: file created at /media/buzzard/ExternalSSD1TB/lean-projects/NNG4/.i18n/en/Game.pot
buzzard@brutus:~/lean-projects/NNG4$  

One possible downside was that I tried this approach with NNG3 and I remember someone complaining that they wanted to use fancy tactics to solve levels but the fancy tactics weren't imported. However if someone has a genuine need for a tactic which is now no longer available then we could just make a new PR adding the import of that particular tactic, which is unlikely to be e.g. a bespoke Witt vector tactic which imports 1000 algebra files from mathlib.

I have no feeling about whether this makes any practical difference to e.g. space requirements for the game, but if it does then it looks like a pretty simple fix.

[kbuzzard]

Let's take the bull by the horns and merge this.