linter commandStart does not like @[to_app (attr := reassoc)

Stream: mathlib4

[Joël Riou]

In #25971, it was found that the commandStart linter does not like the syntax @[to_app (attr := reassoc) (it suggests @[to_app (attr:=reassoc)), while @[reassoc (attr := simp)] is used throughout the category theory files.

[Aaron Liu]

sounds like we need some whitespace in docs#CategoryTheory.to_app

[Calle Sönne]

I can fix this, or are you already doing it @Aaron Liu ?

[Joël Riou]

Thansk! I am trying to do it right now.

[Aaron Liu]

just change the ":=" to " := " it's not that hard

[Joël Riou]

Yes, it was not too hard: https://github.com/leanprover-community/mathlib4/pull/25971/commits/8771d68b8adbe83f330142d1b9b977c83d02a8f1
Thanks!