Import requirements for `Mathlib.Data.List.Basic`

Stream: mathlib4

[Kim Morrison]

It seems the imports for Mathlib.Data.List.Basic are rather heavy. Can we get rid of some?

Here's a whole bunch of general order theory which surely isn't need:

2024-03-19-Mathlib.Data.List.Basic.pdf

[Kim Morrison]

Much better:

after.pdf

[Kim Morrison]

#11497

[Yaël Dillies]

Glad to see you are doing exactly what I thought was needed

[Kim Morrison]

Not my usual MO. :-)