Checking Mathlib's 100-column limit: awk length counts bytes, not characters

In Lean files full of unicode (⟪⟫, ∑, ᵢ, ⊗), awk 'length > 100' reports far too many long lines, because in a C/POSIX locale it counts UTF-8 bytes. Count characters instead, e.g. python3 -c "for i,l in enumerate(open(f).read().split('\n'),1): print(i,len(l)) if len(l)>100 else None". When splitting long statements, break after * or := and indent the continuation 2 more spaces than the head of the expression. In calc first steps, keep the relation on the continuation line. Rerun lake env lean afterwards, since a break inside fun j => needs the body indented under it.