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

awk 'length > 100' measures bytes in many locales, so Lean files full of Unicode (⟶, ≫, ⟦⟧, subscripts) report dozens of false 'long lines'. 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", or run awk under a UTF-8 locale with gawk. For a long term-mode have : T := f (fun ... ↦ by ...) a b, it is cleaner to hoist the lambda into its own have h (x y ...) : ... := by ... than to fight the indentation.