[Merged by Bors] - chore: miscellaneous linter whitespace fixes

[grunweg]

Extracted from #30658. Found by adomani's extension of the commandStart linter to proof bodies.

---

[github-actions]

PR summary 3af1c0aa0e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+-+- coe_mk

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

@YaelDillies @Ruben-VandeVelde Would one of you like to review this one?

[YaelDillies]

Easy!

maintainer merge

[ADedecker]

This one is more subtle I think, there was clear intent to align the =>. I think it's okay to change it, but IMO this should be allowed by whatever tooling we use.

[grunweg]

I agree with the intent. I'm sceptical about manual alignment, though - as this often becomes stale.
In this case, the proofs are also similar, but not too parallel, so this wasn't worth it to me.

I'm not sure how easy or difficult manual alignment is to detect. Manually disabling the linter seems like a good enough band-aid for now.

[ADedecker]

These ones are also debatable IMO. I like a bit of flexibility in sticking together things n+1 in a complicated expression. But I won't fight for it.

[grunweg]

I understand this, abstractly! I think, however, that doing so consistently in a library like mathlib is very hard to impossible, and would much rather have a consistent and enforceable rule. (It's not trivial to make the commandStart linter allow this. Maybe the autoformatter will, but we won't know that for a while.)

[ADedecker]

Thanks! You can ignore my comments, they are just things I wanted to nuance.

bors d+

[mathlib-bors]

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[grunweg]

Thanks for the careful review. I agree both places you flagged could be discussed carefully in the abstract. In this case, I think both changes are fine, so let me go ahead with the one that's easier to automate (namely, making the linter happy).
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step