This is essentially impossible to review in the traditional way, so the question is whether we trust your script or not. I'd say yes (the fact that it builds is proof enough that it works at least to reduce some imports) so I think we should merge this as quickly as possible (running the tool again to fix the conflicts), but it would be better that at least two people agree on this, so
maintainer merge

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

This PR was not actually written by my script, unfortunately. It was a few phases of looking at the output, moving some things to global noshakes, some to local noshakes, and accepting the rest, then cleanup and reformatting of the result, then doing a second and third pass to ensure a minimal diff and checking that things still compile.

The script is able to produce a passable approximation of this PR, but it works best when there are few changes needed and most of the noshakes are already in place; when you run it cold like this it makes a lot of mistakes (because it missed some dependency it wasn't aware of) and makes more mistakes trying to fix its other mistakes, and this requires manual cleanup.

Let me correct myself, then. The question is whether we trust script + Mario. My answer is yes, because in the end it builds and it reduces imports. Maybe in a slightly non-optimal way if Mario screwed up somewhere, but in any case it's a big improvement.

Going forward it might be worth teaching people (mainly maintainers) how to use noshake.json, because it's grown large enough that it is reasonable to expect it to need to be edited on a regular basis.

In short:

• ignoreAll is for files which intentionally have unnecessary imports. Files which are import-only are automatically considered as being in this group, so really the only mathlib file we have in this category is Mathlib.Mathport.Syntax.
• ignoreImport is for files which should be treated as used when importing into another file. This is when there is some property of the file itself which means that downstream users will depend on it without having any direct constant-to-constant dependency. That is, tactics and notation files, and files whose main purpose is to add or declare an attribute.
• ignore is for individual imports in individual files. This is used when there is some unusual use of a constant which is compile-time only, like double-backtick names, Qq expressions, attribute [foo] bar, as well as check-only commands like #guard and example.

I've pushed fixes for the tests, which might warrant additional scrutiny since additional imports there imply some usability loss (to remember to import things otherwise the tactic has degraded behavior).

✌️ digama0 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Could you please merge master and shake it again? I'm surprised that imports of Data.Set.Defs didn't change: it compiles with

import Std.Classes.SetNotation
import Mathlib.Init.Set
import Mathlib.Tactic.Attr.Core
import Mathlib.Tactic.Simps.Basic
import Mathlib.Order.Notation
import Mathlib.Util.CompileInductive
import Mathlib.Data.SProd
import Mathlib.Data.Subtype

(I removed Mathlib.Order.Basic, then fixed compile).

(I hadn't actually done the re-shaking from the last merge yet. I can't shake it until it compiles successfully. Seems I have to merge again and restart the process...)

AAH it conflicted again, I literally can't get this out the door fast enough

bors merge p=10

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style