mathlib

16776539 - chore(*): long lines (#6939)

chore(*): long lines (#6939) Except for URLs, references to books, and `src/tactic/*`, this should be very close to the last of our long lines. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>