Production-worthy formatter for lean4.

Right now it copes with important open source libraries on the model of clang-format's configuration, which is a real trick given the partial elaboration you need (with backtracking). But that works.

mathlib4 is the final boss, I don't currently even have a plan without per-directory quirks files which is probably a nonstarter.