Style: spacing between tactic name and arguments

Stream: mathlib4

[Michael Rothgang]

Just to double-check: mathlib style is to put a space between a tactic name and its arguments, right?
(As in: rw [foo], simp [bar], dsimp only [baz].)

[Michael Rothgang]

This came up in #11626; the style guide doesn't mention this explicitly (but mentions other spaces, so I can see how this is confusing).

[Eric Wieser]

In some sense this style is recorded via the notation itself, which pretty-prints with spaces even if you do not write them

[Michael Rothgang]

Volunteers to update the style guide? I can PR a fix to stragglers in mathlib :-)

[Michael Rothgang]

#11714 - quick reviews or a suggestion for other tactics to try welcome.

[Michael Rothgang]

Just searching for e.g. the regex [a-z]\}[a-z] has way too many false positives with notation.

[Eric Wieser]

I think this is probably not worth the time spent to fix manually across Mathlib; the time is arguably better spent in fixing style guides (as you've done!) and planning an autoformatter.

[Michael Rothgang]

I fixed mathlib :see_no_evil: but filed a PR to the style guide as well: https://github.com/leanprover-community/leanprover-community.github.io/pull/457