More stuff on model theory

Stream: mathlib4

[Tony Beta Lambda]

I'm trying to add more model theory stuff to mathlib, and I think quantifier elimination is a good place to start. I've proved a bunch of basic results here: https://github.com/tonyxty/mathlib4/tree/master, and a provisional proof of the substructure test can be found on the qe branch: https://github.com/tonyxty/mathlib4/tree/qe.

The plan is to prove quantifier elimination for DLO, RCF, and ACF, and hopefully improve the overall design of this part of the library. If someone is working in a similar direction perhaps we can work together.

I'm also interested in adding other classical results to it. Things that came to mind include o-minimality, Morley rank, and quasi-finite fields.

[Chris Hughes]

I should draw your attention to #6617 and #6468 if you hadn't seen them already.

[Tony Beta Lambda]

Thanks! That actually covers a large portion of what I originally planned to do, with a different approach.