Commit 2022-11-23 13:44 aa2a7259

feat: port Data.List.Lex (#672) mathlib3 SHA: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3 Porting notes:

1. There was a mathport "failed to parenthesize" error, but it was easily worked around, see the first commit for details.
2. I had to use aux declarations when constructing things recursively inside the field of a structure. I asked about this on Zulip and also here, but so far there doesn't seem to be a better way. In any case, it compiles so it should be fine. Otherwise, this port was very smooth.
3. Because of the aux where (which is really let rec aux) this caused the defLemma linter to fire, which is being handled in [lean4#1866](https://github.com/leanprover/lean4/pull/1866), so for now we just add these declarations to nolints.json; see Zulip