mathlib

686d005a - chore(*): fix some "line too long" lint errors by rewriting proofs/statements (#5958)