[BalinKing]

See my other comment—LangRust.lean is the same way.

EDIT: Just skimmed Completeness.lean, and it looks similar—at a glance, even the 3+-line proofs are very short and look a lot like boilerplate.

[trissim]

Interesting that you're using em dashes in your comments. Those require Alt+0151 or copy-paste. Glass houses.

[dwb]

And Option-Shift-Hyphen in macOS, which is easy if you know it. And a press and hold on a hyphen on iOS, which is discoverable, even.