chore: clean imports

[felixpernegger]

This PR removes all redundant imports (keeps imports makred --shake etc), and sorts all alphabetically. Reduces imports by about 10%.

Done with vibecoded script here.

I think it would be a good practice to run this automatically once a month or so. Right now it is still pretty quick, like 30min on my laptop.

[felixpernegger]

!bench

[leanprover-radar]

Benchmark results for eab0bc8 against 9d42aaa are in. No significant results found. @felixpernegger

• ✅ build//instructions: -19.9G (-1.02%)

Medium changes (4✅)

• ✅ build/module/Cslib.Computability.Automata.Transducers.Transducer//instructions: -1.8G (-59.28%)
• ✅ build/module/Cslib.Foundations.Syntax.HasAlphaEquiv//instructions: -1.8G (-59.71%)
• ✅ build/module/Cslib.Foundations.Syntax.HasSubstitution//instructions: -1.9G (-60.71%)
• ✅ build/module/Cslib.Foundations.Syntax.HasWellFormed//instructions: -1.8G (-61.57%)

Small changes (8✅)

• ✅ build/module/Cslib.Algorithms.Lean.TimeM//instructions: -1.1G (-19.17%)
• ✅ build/module/Cslib.Foundations.Data.OmegaSequence.Defs//instructions: -844.1M (-19.31%)
• ✅ build/module/Cslib.Foundations.Data.Set.Saturation//instructions: -485.2M (-13.94%)
• ✅ build/module/Cslib.Foundations.Relation.Attr//instructions: -933.6M (-19.88%) (reduced significance based on absolute threshold)
• ✅ build/module/Cslib.Foundations.Relation.Defs//instructions: -1.1G (-24.25%)
• ✅ build/module/Cslib.Foundations.Relation.Restriction//instructions: -507.6M (-14.40%)
• ✅ build/module/Cslib.Languages.CombinatoryLogic.Defs//instructions: -1.0G (-16.15%)
• and 1 hidden

[felixpernegger]

!bench

[leanprover-radar]

Benchmark results for 9a35cbc against 9d42aaa are in. No significant results found. @felixpernegger

• 🟥 build//instructions: +1.9G (+0.10%)

No significant changes detected.

[felixpernegger]

There difference between the two benches comes from whether including init or not.

[chenson2018]

TLDR: I'd be open to adding periodic CI for this, but would prefer it use the new shake like Mathlib does.

More detailed version:

• It does not surprise me that Cslib.Init makes such a huge difference, but this is essential: it serves the same purpose of Mathlib.Init in ensuring that syntax linters (probably the slow part), common tactics etc. are present in every file
• If you look at our CI, you'll see commented out where we previously ran shake on every commit, as Mathlib once did. I'd really prefer to get back to this, but there is an issue of some pending bugs in the new shake I believe. So we can't rely on it as something automatic for every commit yet, but periodic shake PRs would be fine. (Performance is also an issue for Mathlib, but we're tiny in comparison so I think it'd be fine)
• So with this under consideration, I'd much prefer a PR based on shake to an AI-generated Python script.

[felixpernegger]

TLDR: I'd be open to adding periodic CI for this, but would prefer it use the new shake like Mathlib does.

More detailed version:

* It does not surprise me that `Cslib.Init` makes such a huge difference, but this is essential: it serves the same purpose of `Mathlib.Init` in ensuring that syntax linters (probably the slow part), common tactics etc. are present in every file

* If you look at our CI, you'll see commented out where we previously ran `shake` on every commit, as Mathlib once did. I'd really prefer to get back to this, but there is an issue of some pending bugs in the new `shake` I believe. So we can't rely on it as something automatic for every commit yet, but periodic `shake` PRs would be fine. (Performance is also an issue for Mathlib, but we're tiny in comparison so I think it'd be fine)

* So with this under consideration, I'd much prefer a PR based on `shake` to an AI-generated Python script.

I agree shake will eventually definitely be better, but looking at the mathlib PRs with shake, it isnt stable yet. What the AI script is definitely doing though, is getting to some import status, where one can no longer remove any import which isnt Init or marked to be kept.

[felixpernegger]

Is this still mergable as a one-off-thing maybe (since it is reducing imports after all) or do you prefer this to be closed?