Cleaning up error messages with the new string gaps feature

Stream: mathlib4

[Kyle Miller]

I've gone through mathlib looking for error messages that span multiple lines and cleaned them up using the "string gap" escape sequence feature that's now in Lean. #9193

This feature lets us write

    logError m!"\
      After careful consideration, tactic \
      cannot apply{indentD e}\n\
      due to some reason or another."

rather than something like

    logError m!"After careful consideration, tactic {
      ""}cannot apply{indentD e
      }\ndue to some reason or another."

This sort of cleanup has already been done in std4#480

[Kyle Miller]

I'm mentioning this here mostly as a PSA for metaprogrammers -- no need to be clever with {...} anymore!

[Eric Wieser]

The red boxes in the snippet raise that we should probably upstream our lean4 pygments highlighter so that Zulip has access to it

[Eric Wieser]

(possibly after rewriting it to use the fixes that have been made upstream to the lean3 one in the meantime; for instance, https://github.com/pygments/pygments/pull/2614)

[Eric Wieser]

Done in https://github.com/pygments/pygments/pull/2618