feat: move to the module system

[chenson2018]

Closes #172. This PR moves CSLib to the module system, mostly following Mathlib's pattern of using @[expose] public section liberally for the simplest transition. This removes a few uses of private that conflicted:

• LTS.noε
• the HasTau instance in Cslib.Computability.Automata.EpsilonNA.Basic
• grind lemmas about ReductionSystem
• FinFun.fromFun

I also think it might be less confusing if we move some meta sections to their own files, but will leave this for a future PR.

[chenson2018]

For the moment I have moved lake exe mk_all --check --module into its own step, because lean-action does not yet have a parameter for this. (I can make a PR for this later, but don't want it to hold up this one)

[chenson2018]

I have also removed the shake step, as my understanding is that this is not yet compatible with the module system. (Though I think we can still encourage people to use #min_imports until the replacement is in effect.)