[Merged by Bors] - chore(Tactic/TypeStar): reduce imports

[eric-wieser]

I noticed that this doesn't actually use Std or in fact any of its other imports.

The downstream fallout is pretty small because Mathlib.Tactic.Basic imports Std anyway, so this only impacts files not downstream of that.

---

[grunweg]

Does what it says, and there seems to be support for and no resistance against this particular change on zulip.

Thank you for making this change.

[adomani]

Thanks!

I see that there are additions to shake. Should there also be some deletions, from the no longer imported Std?

[eric-wieser]

I just ran shake --update; I assume this auto-removes ignore instructions that no longer do anything?

[adomani]

This is a question for @digama0. I suspect that an unused import should have an entry in shake and removing an unused import should therefore imply a removal in shake.

Anyway, this is certainly not an issue with this PR!

maintainer merge

[digama0]

I just ran shake --update; I assume this auto-removes ignore instructions that no longer do anything?

It auto-removes entries from ignore but not ignoreImport or ignoreAll. This one might have been on those other lists.

[eric-wieser]

Can we leave the shake-reconfiguration to a follow-up?

[adomani]

Yes, I think that it does not make much sense to edit these noshake files manually.

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by adomani.

[Vierkantor]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style