data.list.defs mathlib4#803

Stream: mathlib4

[Scott Morrison]

It looks like this PR may be ready to go. If someone (@Kevin Buzzard?) has read through it carefully, it would be great to have that said so I can merge it without reading it myself. :-)

[Arien Malec]

I think the things that want checking are mostly the naming decisions & decisions about #aligns & it's quite possible that there's code there that really should be aligned differently. I think @Yury G. Kudryashov took a look at this previously as well.

[Kevin Buzzard]

Unfortunately I have not read through it carefully and I already used up all of my lean time for today :-( (unless I get to the bottom of this list of 10 other jobs which is unlikely)