lint(tactic/*): break long lines (#8973)
For code lines, the fix was often simple, just break that damn line.
For strings, you shouldn't break a line inside one as this will be a visible change to the tactic's output. When nothing else can be done, I used the trick of breaking the string into two appended strings. "A B" becomes "A" ++ " B", and that's line-breakable.
