bors merge

I'm not really sure this is a good use of:

• Your time
• The reviewers time
• Other contributors who have merge conflicts to solve after this PR
• CI time

vs investing in a formatting script and using it in CI.

But since you already made the change, let's just put it in.

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style

Thanks for the review and reminding me of this perspective. You have already successfully installed this voice in my head; I did in fact think about this :-)

• on using my time, the initial changes were fully automatic
• my next step, instead of hand-fixing these, would have been to add an extra auto-fixable linter to lint-style.py and use that for the replacements instead (basically, incorporating fix-line-break.py into the other script)
  In fact, this is still possible and should in the order of 15 minutes to implement; I'll do this in my next burst of Lean time.

Given I won't outdo Mario's future auto-formatter, I'm not convinced trying to develop one myself is the right way to go.
(An auto-fixable Python style linter is fine though; did you mean this?)

#13419 does some more replacements, but in a fully automated way.