diff --git a/Cache/Requests.lean b/Cache/Requests.lean
index 207d358bdc2df..ec8da2439e229 100644
--- a/Cache/Requests.lean
+++ b/Cache/Requests.lean
@@ -47,8 +47,8 @@ def mkGetConfigContent (hashMap : IO.HashMap) : IO String := do
 
     -- Note we append a '.part' to the filenames here,
     -- which `downloadFiles` then removes when the download is successful.
-    pure $ acc ++ s!"url = {← mkFileURL fileName none}\n-o {
-      (IO.CACHEDIR / (fileName ++ ".part")).toString.quote}\n"
+    pure $ acc ++ s!"url = {← mkFileURL fileName none}\n\
+      -o {(IO.CACHEDIR / (fileName ++ ".part")).toString.quote}\n"
 
 /-- Calls `curl` to download a single file from the server to `CACHEDIR` (`.cache`) -/
 def downloadFile (hash : UInt64) : IO Bool := do
diff --git a/ImportGraph/Main.lean b/ImportGraph/Main.lean
index 98a1db984f125..0b86f35143303 100644
--- a/ImportGraph/Main.lean
+++ b/ImportGraph/Main.lean
@@ -78,9 +78,9 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
 /-- Setting up command line options and help text for `lake exe graph`. -/
 def graph : Cmd := `[Cli|
   graph VIA importGraphCLI; ["0.0.1"]
-  "Generate representations of a Lean import graph." ++
-  "By default generates the import graph up to `Mathlib`." ++
-  "If you are working in a downstream project, use `lake exe graph --to MyProject`."
+  "Generate representations of a Lean import graph. \
+   By default generates the import graph up to `Mathlib`. \
+   If you are working in a downstream project, use `lake exe graph --to MyProject`."
 
   FLAGS:
     reduce;               "Remove transitively redundant edges."
@@ -90,11 +90,11 @@ def graph : Cmd := `[Cli|
     "include-deps";       "Include used files from other projects (e.g. lake packages)"
 
   ARGS:
-    ...outputs : String;  "Filename(s) for the output. " ++
-      "If none are specified, generates `import_graph.dot`. " ++
-      "Automatically chooses the format based on the file extension. " ++
-      "Currently `.dot` is supported, " ++
-      "and if you have `graphviz` installed then any supported output format is allowed."
+    ...outputs : String;  "Filename(s) for the output. \
+      If none are specified, generates `import_graph.dot`. \
+      Automatically chooses the format based on the file extension. \
+      Currently `.dot` is supported, \
+      and if you have `graphviz` installed then any supported output format is allowed."
 ]
 
 /-- `lake exe graph` -/
diff --git a/Mathlib/Data/Matrix/Notation.lean b/Mathlib/Data/Matrix/Notation.lean
index 7a1eaef0a01b3..13f2a3527df5b 100644
--- a/Mathlib/Data/Matrix/Notation.lean
+++ b/Mathlib/Data/Matrix/Notation.lean
@@ -103,9 +103,9 @@ macro_rules
     let n := if h : 0 < m then rows[0].size else 0
     let rowVecs ← rows.mapM fun row : Array Term => do
       unless row.size = n do
-        Macro.throwErrorAt (mkNullNode row)
-          s!"Rows must be of equal length; this row has {row.size} items, the previous rows {"
-          "}have {n}"
+        Macro.throwErrorAt (mkNullNode row) s!"\
+          Rows must be of equal length; this row has {row.size} items, \
+          the previous rows have {n}"
       `(![$row,*])
     `(@Matrix.of (Fin $(quote m)) (Fin $(quote n)) _ ![$rowVecs,*])
   | `(!![$[;%$semicolons]*]) => do
diff --git a/Mathlib/Data/PNat/Xgcd.lean b/Mathlib/Data/PNat/Xgcd.lean
index 047a251db8206..c43183d9b8b21 100644
--- a/Mathlib/Data/PNat/Xgcd.lean
+++ b/Mathlib/Data/PNat/Xgcd.lean
@@ -70,9 +70,9 @@ instance : SizeOf XgcdType :=
  reflects the matrix/vector interpretation as above. -/
 instance : Repr XgcdType where
   reprPrec
-  | g, _ => s!"[[[ {repr (g.wp + 1)}, {(repr g.x)} ], [" ++
-            s!"{repr g.y}, {repr (g.zp + 1)}]], [" ++
-            s!"{repr (g.ap + 1)}, {repr (g.bp + 1)}]]"
+  | g, _ => s!"[[[{repr (g.wp + 1)}, {repr g.x}], \
+                 [{repr g.y}, {repr (g.zp + 1)}]], \
+                [{repr (g.ap + 1)}, {repr (g.bp + 1)}]]"
 
 /-- Another `mk` using ℕ and ℕ+ -/
 def mk' (w : ℕ+) (x : ℕ) (y : ℕ) (z : ℕ+) (a : ℕ+) (b : ℕ+) : XgcdType :=
diff --git a/Mathlib/Lean/Expr/Basic.lean b/Mathlib/Lean/Expr/Basic.lean
index 68cbeaf94e739..eaab712e9ff82 100644
--- a/Mathlib/Lean/Expr/Basic.lean
+++ b/Mathlib/Lean/Expr/Basic.lean
@@ -422,8 +422,8 @@ def reduceProjStruct? (e : Expr) : MetaM (Option Expr) := do
     if hs : sidx < sfields.size then
       return some (sfields[sidx]'hs)
     else
-      throwError m!"ill-formed expression, {cname} is the {pinfo.i + 1}-th projection function {
-          ""}but {sarg} does not have enough arguments"
+      throwError m!"ill-formed expression, {cname} is the {pinfo.i + 1}-th projection function \
+        but {sarg} does not have enough arguments"
   else
     return none
 
diff --git a/Mathlib/Mathport/Notation.lean b/Mathlib/Mathport/Notation.lean
index 9afa98330f8b6..86f6e6b78a12e 100644
--- a/Mathlib/Mathport/Notation.lean
+++ b/Mathlib/Mathport/Notation.lean
@@ -590,13 +590,14 @@ elab (name := notation3) doc:(docComment)? attrs?:(Parser.Term.attributes)? attr
         elabCommand <|
           ← `(command| attribute [$attrKind delab $(mkIdent key)] $(Lean.mkIdent delabName))
     else
-      logWarning s!"Was not able to generate a pretty printer for this notation.{
-        ""} If you do not expect it to be pretty printable, then you can use{
-        ""} `notation3 (prettyPrint := false)`.{
-        ""} If the notation expansion refers to section variables, be sure to do `local notation3`.{
-        ""} Otherwise, you might be able to adjust the notation expansion to make it matchable;{
-        ""} pretty printing relies on deriving an expression matcher from the expansion.{
-        ""} (Use `set_option trace.notation3 true` to get some debug information.)"
+      logWarning s!"\
+        Was not able to generate a pretty printer for this notation. \
+        If you do not expect it to be pretty printable, then you can use \
+        `notation3 (prettyPrint := false)`. \
+        If the notation expansion refers to section variables, be sure to do `local notation3`. \
+        Otherwise, you might be able to adjust the notation expansion to make it matchable; \
+        pretty printing relies on deriving an expression matcher from the expansion. \
+        (Use `set_option trace.notation3 true` to get some debug information.)"
 
 initialize Std.Linter.UnreachableTactic.addIgnoreTacticKind ``«notation3»
 
diff --git a/Mathlib/Mathport/Rename.lean b/Mathlib/Mathport/Rename.lean
index 14c2ce5471dc1..c87acc945db71 100644
--- a/Mathlib/Mathport/Rename.lean
+++ b/Mathlib/Mathport/Rename.lean
@@ -160,17 +160,17 @@ def suspiciousLean3Name (s : String) : Bool := Id.run do
         let note := "(add `set_option align.precheck false` to suppress this message)"
         let inner := match ← try some <$> resolveGlobalConstWithInfos id4 catch _ => pure none with
         | none => m!""
-        | some cs => m!" Did you mean:\n\n{
-            ("\n":MessageData).joinSep (cs.map fun c' => m!"  #align {id3} {c'}")
-          }\n\n#align inputs have to be fully qualified.{""
-          } (Double check the lean 3 name too, we can't check that!)"
+        | some cs => m!" Did you mean:\n\n\
+              {("\n":MessageData).joinSep (cs.map fun c' => m!"  #align {id3} {c'}")}\n\n\
+            #align inputs have to be fully qualified. \
+            (Double check the lean 3 name too, we can't check that!)"
         throwErrorAt id4 "Declaration {c} not found.{inner}\n{note}"
       if Linter.getLinterValue linter.uppercaseLean3 (← getOptions) then
         if id3.getId.anyS suspiciousLean3Name then
-          Linter.logLint linter.uppercaseLean3 id3 $
-            "Lean 3 names are usually lowercase. This might be a typo.\n" ++
-            "If the Lean 3 name is correct, then above this line, add:\n" ++
-            "set_option linter.uppercaseLean3 false in\n"
+          Linter.logLint linter.uppercaseLean3 id3
+            "Lean 3 names are usually lowercase. This might be a typo.\n\
+             If the Lean 3 name is correct, then above this line, add:\n\
+             set_option linter.uppercaseLean3 false in\n"
     withRef id3 <| ensureUnused id3.getId
     liftCoreM <| addNameAlignment id3.getId id4.getId
   | _ => throwUnsupportedSyntax
diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
index 8f0d99b868349..450fd905a4a82 100644
--- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
+++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
@@ -243,11 +243,11 @@ def borelToRefl (e : Expr) (i : FVarId) : TacticM Unit := do
     liftMetaTactic fun m => return [← subst m i]
   catch _ =>
     let et ← synthInstance (← mkAppOptM ``TopologicalSpace #[e])
-    throwError
-      (m!"`‹TopologicalSpace {e}› := {et}" ++ MessageData.ofFormat Format.line ++
-        m!"depends on" ++ MessageData.ofFormat Format.line ++
-        m!"{Expr.fvar i} : MeasurableSpace {e}`" ++ MessageData.ofFormat Format.line ++
-        "so `borelize` isn't avaliable")
+    throwError m!"\
+      `‹TopologicalSpace {e}› := {et}\n\
+      depends on\n\
+      {Expr.fvar i} : MeasurableSpace {e}`\n\
+      so `borelize` isn't avaliable"
   evalTactic <| ← `(tactic|
     refine_lift
       letI : MeasurableSpace $te := borel $te
diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index c6a66c311a9ba..425ea805c77c8 100644
--- a/Mathlib/Tactic/Cases.lean
+++ b/Mathlib/Tactic/Cases.lean
@@ -75,11 +75,11 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.casesTarget,+)
       let mut s ← getFVarSetToGeneralize targets forbidden
       for v in genArgs do
         if forbidden.contains v then
-          throwError "variable cannot be generalized {""
-            }because target depends on it{indentExpr (mkFVar v)}"
+          throwError "variable cannot be generalized \
+            because target depends on it{indentExpr (mkFVar v)}"
         if s.contains v then
-          throwError "unnecessary 'generalizing' argument, {""
-            }variable '{mkFVar v}' is generalized automatically"
+          throwError "unnecessary 'generalizing' argument, \
+            variable '{mkFVar v}' is generalized automatically"
         s := s.insert v
       let (fvarIds, g) ← g.revert (← sortFVarIds s.toArray)
       g.withContext do
diff --git a/Mathlib/Tactic/CategoryTheory/Coherence.lean b/Mathlib/Tactic/CategoryTheory/Coherence.lean
index 2458843d8c4ec..ffa3d3e9dea24 100644
--- a/Mathlib/Tactic/CategoryTheory/Coherence.lean
+++ b/Mathlib/Tactic/CategoryTheory/Coherence.lean
@@ -329,8 +329,8 @@ def coherence_loop (maxSteps := 37) : TacticM Unit :=
     -- Otherwise, rearrange so we have a maximal prefix of each side
     -- that is built out of unitors and associators:
     evalTactic (← `(tactic| liftable_prefixes)) <|>
-      exception' ("Something went wrong in the `coherence` tactic: " ++
-        "is the target an equation in a monoidal category?")
+      exception' "Something went wrong in the `coherence` tactic: \
+        is the target an equation in a monoidal category?"
     -- The goal should now look like `f₀ ≫ f₁ = g₀ ≫ g₁`,
     liftMetaTactic MVarId.congrCore
     -- and now we have two goals `f₀ = g₀` and `f₁ = g₁`.
diff --git a/Mathlib/Tactic/CategoryTheory/Elementwise.lean b/Mathlib/Tactic/CategoryTheory/Elementwise.lean
index c892dac0de665..e9920aa866288 100644
--- a/Mathlib/Tactic/CategoryTheory/Elementwise.lean
+++ b/Mathlib/Tactic/CategoryTheory/Elementwise.lean
@@ -84,9 +84,9 @@ def elementwiseExpr (src : Name) (type pf : Expr) (simpSides := true) :
       -- First simplify using elementwise-specific lemmas
       let mut eqPf' ← simpType (simpOnlyNames elementwiseThms (config := { decide := false })) eqPf
       if (← inferType eqPf') == .const ``True [] then
-        throwError "elementwise lemma for {src} is trivial after applying ConcreteCategory {""
-          }lemmas, which can be caused by how applications are unfolded. {""
-          }Using elementwise is unnecessary."
+        throwError "elementwise lemma for {src} is trivial after applying ConcreteCategory \
+          lemmas, which can be caused by how applications are unfolded. \
+          Using elementwise is unnecessary."
       if simpSides then
         let ctx := { ← Simp.Context.mkDefault with config.decide := false }
         let (ty', eqPf'') ← simpEq (fun e => return (← simp e ctx).1) (← inferType eqPf') eqPf'
@@ -94,9 +94,9 @@ def elementwiseExpr (src : Name) (type pf : Expr) (simpSides := true) :
         forallTelescope ty' fun _ ty' => do
           if let some (_, lhs, rhs) := ty'.eq? then
             if ← Std.Tactic.Lint.isSimpEq lhs rhs then
-              throwError "applying simp to both sides reduces elementwise lemma for {src} {""
-                }to the trivial equality {ty'}. {""
-                }Either add `nosimp` or remove the `elementwise` attribute."
+              throwError "applying simp to both sides reduces elementwise lemma for {src} \
+                to the trivial equality {ty'}. \
+                Either add `nosimp` or remove the `elementwise` attribute."
         eqPf' ← mkExpectedTypeHint eqPf'' ty'
       if let some (w, instConcr) := instConcr? then
         return (← Meta.mkLambdaFVars (fvars.push instConcr) eqPf', w)
diff --git a/Mathlib/Tactic/Change.lean b/Mathlib/Tactic/Change.lean
index 982f37e4084b7..a14ddb334200d 100644
--- a/Mathlib/Tactic/Change.lean
+++ b/Mathlib/Tactic/Change.lean
@@ -39,8 +39,9 @@ elab_rules : tactic
     | some sop => do
       let tgt ← getMainTarget
       let ex ← withRef sop <| elabTermEnsuringType sop (← inferType tgt)
-      if !(← isDefEq ex tgt) then throwErrorAt sop "The term{indentD ex}\nis not defeq to the goal:{
-        indentD tgt}"
+      if !(← isDefEq ex tgt) then throwErrorAt sop "\
+        The term{indentD ex}\n\
+        is not defeq to the goal:{indentD tgt}"
       instantiateMVars ex
   let dstx ← delabToRefinableSyntax expr
   addSuggestion tk (← `(tactic| change $dstx)) (origSpan? := stx)
diff --git a/Mathlib/Tactic/ComputeDegree.lean b/Mathlib/Tactic/ComputeDegree.lean
index 1044c6b9db4df..a731eec11f844 100644
--- a/Mathlib/Tactic/ComputeDegree.lean
+++ b/Mathlib/Tactic/ComputeDegree.lean
@@ -445,11 +445,10 @@ elab_rules : tactic | `(tactic| compute_degree $[!%$bang]?) => focus <| withMain
     | _ => none
   let twoH := twoHeadsArgs gt
   match twoH with
-    | (_, .anonymous, _) => throwError
-        (m!"'compute_degree' inapplicable. The goal{indentD gt}\nis expected to be '≤' or '='.")
-    | (.anonymous, _, _) => throwError
-        (m!"'compute_degree' inapplicable. The LHS must be an application of {
-          ""}'natDegree', 'degree', or 'coeff'.")
+    | (_, .anonymous, _) => throwError m!"'compute_degree' inapplicable. \
+        The goal{indentD gt}\nis expected to be '≤' or '='."
+    | (.anonymous, _, _) => throwError m!"'compute_degree' inapplicable. \
+        The LHS must be an application of 'natDegree', 'degree', or 'coeff'."
     | _ =>
       let lem := dispatchLemma twoH
       trace[Tactic.compute_degree] f!"'compute_degree' first applies lemma '{lem.getString}'"
diff --git a/Mathlib/Tactic/Core.lean b/Mathlib/Tactic/Core.lean
index d0b89a09f5755..79d349fad19e7 100644
--- a/Mathlib/Tactic/Core.lean
+++ b/Mathlib/Tactic/Core.lean
@@ -251,8 +251,8 @@ def getPackageDir (pkg : String) : IO System.FilePath := do
   let root? ← sp.findM? fun p =>
     (p / pkg).isDir <||> ((p / pkg).withExtension "lean").pathExists
   if let some root := root? then return root
-  throw <| IO.userError s!"Could not find {pkg} directory. {
-    ""}Make sure the LEAN_SRC_PATH environment variable is set correctly."
+  throw <| IO.userError s!"Could not find {pkg} directory. \
+    Make sure the LEAN_SRC_PATH environment variable is set correctly."
 
 /-- Returns the mathlib root directory. -/
 def getMathlibDir := getPackageDir "Mathlib"
diff --git a/Mathlib/Tactic/DeriveFintype.lean b/Mathlib/Tactic/DeriveFintype.lean
index 2790a2cc19194..d475463b92670 100644
--- a/Mathlib/Tactic/DeriveFintype.lean
+++ b/Mathlib/Tactic/DeriveFintype.lean
@@ -133,8 +133,8 @@ def mkFintypeEnum (declName : Name) : CommandElabM Unit := do
           type := listType
           value := enumList }
       setProtected enumListName
-      addDocString enumListName s!"A list enumerating every element of the type, {
-        ""}which are all zero-argument constructors. (Generated by the `Fintype` deriving handler.)"
+      addDocString enumListName s!"A list enumerating every element of the type, \
+        which are all zero-argument constructors. (Generated by the `Fintype` deriving handler.)"
     do -- Prove that this list is in `toCtorIdx` order
       trace[Elab.Deriving.fintype] "proving {toCtorThmName}"
       let goalStx ← `(term| ∀ (x : $(← Term.exprToSyntax <| mkConst declName levels)),
diff --git a/Mathlib/Tactic/Eqns.lean b/Mathlib/Tactic/Eqns.lean
index e3c1808672c4b..e8ea5e7a6dc19 100644
--- a/Mathlib/Tactic/Eqns.lean
+++ b/Mathlib/Tactic/Eqns.lean
@@ -38,8 +38,8 @@ initialize eqnsAttribute : NameMapExtension (Array Name) ←
     add   := fun
     | declName, `(attr| eqns $[$names]*) => do
       if let some _ := Meta.eqnsExt.getState (← getEnv) |>.map.find? declName then
-        throwError "There already exist stored eqns for '{declName}' registering new equations{
-            "\n"}will not have the desired effect."
+        throwError "There already exist stored eqns for '{declName}'; registering new equations \
+          will not have the desired effect."
       names.mapM resolveGlobalConstNoOverloadWithInfo
     | _, _ => Lean.Elab.throwUnsupportedSyntax }
 
diff --git a/Mathlib/Tactic/FinCases.lean b/Mathlib/Tactic/FinCases.lean
index f7324d4da07f1..c28b00169668f 100644
--- a/Mathlib/Tactic/FinCases.lean
+++ b/Mathlib/Tactic/FinCases.lean
@@ -30,8 +30,8 @@ def getMemType {m : Type → Type} [Monad m] [MonadError m] (e : Expr) : m (Opti
     | (``List, #[α])     => return α
     | (``Multiset, #[α]) => return α
     | (``Finset, #[α])   => return α
-    | _ => throwError ("Hypothesis must be of type `x ∈ (A : List α)`, `x ∈ (A : Finset α)`,"
-        ++ " or `x ∈ (A : Multiset α)`")
+    | _ => throwError "Hypothesis must be of type `x ∈ (A : List α)`, `x ∈ (A : Finset α)`, \
+                       or `x ∈ (A : Multiset α)`"
   | _ => return none
 
 /--
diff --git a/Mathlib/Tactic/GCongr/Core.lean b/Mathlib/Tactic/GCongr/Core.lean
index 0caf2fc67f3bf..c15ad39a29fef 100644
--- a/Mathlib/Tactic/GCongr/Core.lean
+++ b/Mathlib/Tactic/GCongr/Core.lean
@@ -155,9 +155,9 @@ initialize registerBuiltinAttribute {
   add := fun decl _ kind ↦ MetaM.run' do
     let declTy := (← getConstInfo decl).type
     withReducible <| forallTelescopeReducing declTy fun xs targetTy => do
-    let fail := throwError
-      "@[gcongr] attribute only applies to lemmas proving {
-      ""}x₁ ~₁ x₁' → ... xₙ ~ₙ xₙ' → f x₁ ... xₙ ∼ f x₁' ... xₙ', got {declTy}"
+    let fail := throwError "\
+      @[gcongr] attribute only applies to lemmas proving \
+      x₁ ~₁ x₁' → ... xₙ ~ₙ xₙ' → f x₁ ... xₙ ∼ f x₁' ... xₙ', got {declTy}"
     -- verify that conclusion of the lemma is of the form `rel (head x₁ ... xₙ) (head y₁ ... yₙ)`
     let .app (.app rel lhs) rhs ← whnf targetTy | fail
     let some relName := rel.getAppFn.constName? | fail
@@ -404,8 +404,8 @@ partial def _root_.Lean.MVarId.gcongr
   let some (sErr, e) := ex?
     -- B. If there is a template, and there was no `@[gcongr]` lemma which matched the template,
     -- fail.
-    | throwError "gcongr failed, no @[gcongr] lemma applies for the template portion {""
-        }{template} and the relation {rel}"
+    | throwError "gcongr failed, no @[gcongr] lemma applies for the template portion \
+        {template} and the relation {rel}"
   -- B. If there is a template, and there was a `@[gcongr]` lemma which matched the template, but
   -- it was not possible to `apply` that lemma, then report the error message from `apply`-ing that
   -- lemma.
@@ -512,5 +512,5 @@ elab_rules : tactic
     | unsolvedGoalStates => do
       let unsolvedGoals ← @List.mapM MetaM _ _ _ MVarId.getType unsolvedGoalStates
       let g := Lean.MessageData.joinSep (unsolvedGoals.map Lean.MessageData.ofExpr) Format.line
-      throwError "rel failed, cannot prove goal by 'substituting' the listed relationships. {""
-        }The steps which could not be automatically justified were: \n{g}"
+      throwError "rel failed, cannot prove goal by 'substituting' the listed relationships. \
+        The steps which could not be automatically justified were:\n{g}"
diff --git a/Mathlib/Tactic/LibrarySearch.lean b/Mathlib/Tactic/LibrarySearch.lean
index 5b53531bb0ec7..3a99072021bb0 100644
--- a/Mathlib/Tactic/LibrarySearch.lean
+++ b/Mathlib/Tactic/LibrarySearch.lean
@@ -275,8 +275,8 @@ elab_rules : tactic | `(tactic| apply? $[using $[$required],*]?) => do
   exact? (← getRef) required false
 
 elab tk:"library_search" : tactic => do
-  logWarning ("`library_search` has been renamed to `apply?`" ++
-    " (or `exact?` if you only want solutions closing the goal)")
+  logWarning "`library_search` has been renamed to `apply?` \
+    (or `exact?` if you only want solutions closing the goal)"
   exact? tk none false
 
 open Elab Term in
diff --git a/Mathlib/Tactic/MoveAdd.lean b/Mathlib/Tactic/MoveAdd.lean
index 99e38ea26f949..b160937169965 100644
--- a/Mathlib/Tactic/MoveAdd.lean
+++ b/Mathlib/Tactic/MoveAdd.lean
@@ -388,8 +388,9 @@ def unifyMovements (data : Array (Expr × Bool × Syntax)) (tgt : Expr) :
   let atoms := (ops.map Prod.fst).flatten.toList.filter (!isBVar ·)
   -- `instr` are the unified user-provided terms, `neverMatched` are non-unified ones
   let (instr, neverMatched) ← pairUp data.toList atoms
-  let dbgMsg := #[m!"Matching of input variables:\n* pre-match:  {
-    data.map (Prod.snd ∘ Prod.snd)}\n* post-match: {instr}",
+  let dbgMsg := #[m!"Matching of input variables:\n\
+    * pre-match:  {data.map (Prod.snd ∘ Prod.snd)}\n\
+    * post-match: {instr}",
     m!"\nMaximum number of iterations: {ops.size}"]
   -- if there are `neverMatched` terms, return the parsed terms and the syntax
   let errMsg := neverMatched.map fun (t, a, stx) => (if a then m!"← {t}" else m!"{t}", stx)
diff --git a/Mathlib/Tactic/Nontriviality/Core.lean b/Mathlib/Tactic/Nontriviality/Core.lean
index 0d6a1fadbed47..b1fed972e004c 100644
--- a/Mathlib/Tactic/Nontriviality/Core.lean
+++ b/Mathlib/Tactic/Nontriviality/Core.lean
@@ -109,8 +109,8 @@ syntax (name := nontriviality) "nontriviality" (ppSpace colGt term)?
       if let some (α, _) := tgt.eq? then return α
       if let some (α, _) := tgt.app4? ``LE.le then return α
       if let some (α, _) := tgt.app4? ``LT.lt then return α
-      throwError "The goal is not an (in)equality, so you'll need to specify the desired {""
-        }`Nontrivial α` instance by invoking `nontriviality α`.")
+      throwError "The goal is not an (in)equality, so you'll need to specify the desired \
+        `Nontrivial α` instance by invoking `nontriviality α`.")
     let .sort u ← whnf (← inferType α) | unreachable!
     let some v := u.dec | throwError "not a type{indentExpr α}"
     let α : Q(Type v) := α
diff --git a/Mathlib/Tactic/ProxyType.lean b/Mathlib/Tactic/ProxyType.lean
index 3051eda2efa32..5aca18d189eee 100644
--- a/Mathlib/Tactic/ProxyType.lean
+++ b/Mathlib/Tactic/ProxyType.lean
@@ -196,10 +196,10 @@ def ensureProxyEquiv (config : ProxyEquivConfig) (indVal : InductiveVal) : TermE
       setReducibleAttribute config.proxyName
       setProtected config.proxyName
       -- Add a docstring
-      addDocString config.proxyName s!"A \"proxy type\" equivalent to `{indVal.name}` that is {
-        ""}constructed from `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum`. {
-        ""}See `{config.proxyEquivName}` for the equivalence. {
-        ""}(Generated by the `proxy_equiv%` elaborator.)"
+      addDocString config.proxyName s!"A \"proxy type\" equivalent to `{indVal.name}` that is \
+        constructed from `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum`. \
+        See `{config.proxyEquivName}` for the equivalence. \
+        (Generated by the `proxy_equiv%` elaborator.)"
       trace[Elab.ProxyType] "defined {config.proxyName}"
 
     -- Create the `Equiv`
@@ -232,12 +232,12 @@ def ensureProxyEquiv (config : ProxyEquivConfig) (indVal : InductiveVal) : TermE
           type := (← inferType equiv')
           value := equiv' }
       setProtected config.proxyEquivName
-      addDocString config.proxyEquivName s!"An equivalence between the \"proxy type\" {
-        ""}`{config.proxyName}` and `{indVal.name}`. The proxy type is a reducible definition {
-        ""}that represents the inductive type using `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum` {
-        ""}(and whatever other inductive types appear within the inductive type), and the {
-        ""}intended use is to define typeclass instances uses pre-existing instances on these. {
-        ""}(Generated by the `proxy_equiv%` elaborator.)"
+      addDocString config.proxyEquivName s!"An equivalence between the \"proxy type\" \
+        `{config.proxyName}` and `{indVal.name}`. The proxy type is a reducible definition \
+        that represents the inductive type using `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum` \
+        (and whatever other inductive types appear within the inductive type), and the \
+        intended use is to define typeclass instances uses pre-existing instances on these. \
+        (Generated by the `proxy_equiv%` elaborator.)"
       trace[Elab.ProxyType] "defined {config.proxyEquivName}"
 
 /-- Helper function for `proxy_equiv% type : expectedType` elaborators.
diff --git a/Mathlib/Tactic/Recall.lean b/Mathlib/Tactic/Recall.lean
index 872218bef3a8e..31569dbba1b52 100644
--- a/Mathlib/Tactic/Recall.lean
+++ b/Mathlib/Tactic/Recall.lean
@@ -57,9 +57,9 @@ elab_rules : command
           throwTypeMismatchError none info.type newInfo.type declConst
         let newVal := newInfo.value?.get!.instantiateLevelParams newInfo.levelParams mvs
         unless (← isDefEq infoVal newVal) do
-          let err :=
-            m!"value mismatch{indentExpr declConst}\nhas value{indentExpr newVal}\n" ++
-            m!"but is expected to have value{indentExpr infoVal}"
+          let err := m!"\
+            value mismatch{indentExpr declConst}\nhas value{indentExpr newVal}\n\
+            but is expected to have value{indentExpr infoVal}"
           throwErrorAt val err
     else
       let (binders, type?) := expandOptDeclSig sig
diff --git a/Mathlib/Tactic/RewriteSearch.lean b/Mathlib/Tactic/RewriteSearch.lean
index ba11a43575115..10774fbe1fda8 100644
--- a/Mathlib/Tactic/RewriteSearch.lean
+++ b/Mathlib/Tactic/RewriteSearch.lean
@@ -143,11 +143,11 @@ def toString (n : SearchNode) : MetaM String := do
   | some (_, e, true) => do let pp ← ppExpr e; pure s!"rw [← {pp}]"
   | some (_, e, false) => do let pp ← ppExpr e; pure s!"rw [{pp}]"
   | none => pure ""
-  return s!"depth: {n.history.size}\n" ++
-    s!"history: {n.history.map fun p => hash p % 10000}\n" ++
-    tac ++ "\n" ++
-    "-- " ++ n.ppGoal ++ "\n" ++
-    s!"distance: {n.dist?.get!}+{n.history.size}, {n.ppGoal.length}"
+  return s!"depth: {n.history.size}\n\
+    history: {n.history.map fun p => hash p % 10000}\n\
+    {tac}\n\
+    -- {n.ppGoal}\n\
+    distance: {n.dist?.get!}+{n.history.size}, {n.ppGoal.length}"
 
 /-- Construct a `SearchNode`. -/
 def mk (history : Array (Nat × Expr × Bool)) (goal : MVarId) (ctx : Option MetavarContext := none) :
diff --git a/Mathlib/Tactic/Rewrites.lean b/Mathlib/Tactic/Rewrites.lean
index fb1869a4e04fe..2f7371145e076 100644
--- a/Mathlib/Tactic/Rewrites.lean
+++ b/Mathlib/Tactic/Rewrites.lean
@@ -344,8 +344,7 @@ elab_rules : tactic |
       let results ← rewrites hyps lems goal target (stopAtRfl := false) forbidden
       reportOutOfHeartbeats `rewrites tk
       if results.isEmpty then
-        throwError "Could not find any lemmas which can rewrite the hypothesis {
-          ← f.getUserName}"
+        throwError "Could not find any lemmas which can rewrite the hypothesis {← f.getUserName}"
       for r in results do withMCtx r.mctx do
         addRewriteSuggestion tk [(r.expr, r.symm)]
           r.result.eNew (loc? := .some (.fvar f)) (origSpan? := ← getRef)
diff --git a/Mathlib/Tactic/Says.lean b/Mathlib/Tactic/Says.lean
index c0c874507a2c7..3bff30ea421a7 100644
--- a/Mathlib/Tactic/Says.lean
+++ b/Mathlib/Tactic/Says.lean
@@ -32,8 +32,8 @@ namespace Mathlib.Tactic.Says
 register_option says.verify : Bool :=
   { defValue := false
     group := "says"
-    descr := "For every appearance of the `X says Y` combinator, " ++
-      "re-verify that running `X` produces `Try this: Y`." }
+    descr := "For every appearance of the `X says Y` combinator, \
+      re-verify that running `X` produces `Try this: Y`." }
 
 register_option says.no_verify_in_CI : Bool :=
   { defValue := false
diff --git a/Mathlib/Tactic/Simps/Basic.lean b/Mathlib/Tactic/Simps/Basic.lean
index bf8227a2bae45..1e8297e6b47d7 100644
--- a/Mathlib/Tactic/Simps/Basic.lean
+++ b/Mathlib/Tactic/Simps/Basic.lean
@@ -574,11 +574,11 @@ def applyProjectionRules (projs : Array ParsedProjectionData) (rules : Array Pro
           proj else
         projs.push {strName := nm, newName := nm, strStx := stx, newStx := stx, isPrefix := true}
   trace[simps.debug] "Projection info after applying the rules: {projs}."
-  unless (projs.map (·.newName)).toList.Nodup do throwError
-    "Invalid projection names. Two projections have the same name.\n{""
-    }This is likely because a custom composition of projections was given the same name as an {""
-    }existing projection. Solution: rename the existing projection (before naming the {""
-    }custom projection)."
+  unless (projs.map (·.newName)).toList.Nodup do throwError "\
+    Invalid projection names. Two projections have the same name.\n\
+    This is likely because a custom composition of projections was given the same name as an \
+    existing projection. Solution: rename the existing projection (before naming the \
+    custom projection)."
   pure projs
 
 /-- Auxiliary function for `getRawProjections`.
@@ -609,12 +609,13 @@ def findProjection (str : Name) (proj : ParsedProjectionData)
       let customProjType ← MetaM.run' (inferType customProj)
       let rawExprType ← MetaM.run' (inferType rawExpr)
       if (← MetaM.run' (isDefEq customProjType rawExprType)) then
-        throwError "Invalid custom projection:{indentExpr customProj}\n{""
-          }Expression is not definitionally equal to {indentExpr rawExpr}" else
-        throwError "Invalid custom projection:\n  {customProj}\n{""
-          }Expression has different type than {str ++ proj.strName}. Given type:{
-          indentExpr customProjType}\nExpected type:{indentExpr rawExprType
-          }\nNote: make sure order of implicit arguments is exactly the same."
+        throwError "Invalid custom projection:{indentExpr customProj}\n\
+          Expression is not definitionally equal to {indentExpr rawExpr}"
+      else
+        throwError "Invalid custom projection:{indentExpr customProj}\n\
+          Expression has different type than {str ++ proj.strName}. Given type:\
+          {indentExpr customProjType}\nExpected type:{indentExpr rawExprType}\n\
+          Note: make sure order of implicit arguments is exactly the same."
   | _ =>
     _ ← MetaM.run' <| TermElabM.run' <| addTermInfo proj.newStx rawExpr
     pure {proj with expr? := some rawExpr, projNrs := nrs}
@@ -628,9 +629,9 @@ def checkForUnusedCustomProjs (stx : Syntax) (str : Name) (projs : Array ParsedP
   let customDeclarations := env.constants.map₂.foldl (init := #[]) fun xs nm _ =>
     if (str ++ `Simps).isPrefixOf nm && !nm.isInternalDetail then xs.push nm else xs
   if nrCustomProjections < customDeclarations.size then
-    Linter.logLintIf linter.simpsUnusedCustomDeclarations stx
-      m!"Not all of the custom declarations {customDeclarations} are used. Double check the {
-        ""}spelling, and use `?` to get more information."
+    Linter.logLintIf linter.simpsUnusedCustomDeclarations stx m!"\
+      Not all of the custom declarations {customDeclarations} are used. Double check the \
+      spelling, and use `?` to get more information."
 
 /-- If a structure has a field that corresponds to a coercion to functions or sets, or corresponds
   to notation, find the custom projection that uses this coercion or notation.
@@ -648,8 +649,8 @@ def findAutomaticProjectionsAux (str : Name) (proj : ParsedProjectionData) (args
     let findArgs ← unsafe evalConst findArgType findArgs
     let classArgs ← try findArgs str className args
     catch ex =>
-      trace[simps.debug] "Projection {proj.strName} is likely unrelated to the projection of {
-        className}:\n{ex.toMessageData}"
+      trace[simps.debug] "Projection {proj.strName} is likely unrelated to the projection of \
+        {className}:\n{ex.toMessageData}"
       return none
     let classArgs ← classArgs.mapM fun e => match e with
       | none => mkFreshExprMVar none
@@ -661,8 +662,8 @@ def findAutomaticProjectionsAux (str : Name) (proj : ParsedProjectionData) (args
     let eInstType ←
       try withoutErrToSorry (elabAppArgs (← Term.mkConst className) #[] classArgs none true false)
       catch ex =>
-        trace[simps.debug] "Projection doesn't have the right type for the automatic projection:\n{
-          ex.toMessageData}"
+        trace[simps.debug] "Projection doesn't have the right type for the automatic projection:\n\
+          {ex.toMessageData}"
         return none
     return ← withLocalDeclD `self eStr fun instStr ↦ do
       trace[simps.debug] "found projection {proj.strName}. Trying to synthesize {eInstType}."
@@ -689,13 +690,13 @@ def findAutomaticProjections (str : Name) (projs : Array ParsedProjectionData) :
   let projs ← projs.mapM fun proj => do
     if let some (projExpr, projName) := ← findAutomaticProjectionsAux str proj args then
       unless ← isDefEq projExpr proj.expr?.get! do
-        throwError "The projection {proj.newName} is not definitionally equal to an application {
-          ""}of {projName}:{indentExpr proj.expr?.get!}\nvs{indentExpr projExpr}"
+        throwError "The projection {proj.newName} is not definitionally equal to an application \
+          of {projName}:{indentExpr proj.expr?.get!}\nvs{indentExpr projExpr}"
       if proj.isCustom then
-        trace[simps.verbose] "Warning: Projection {proj.newName} is given manually by the user, {
-          ""}but it can be generated automatically."
+        trace[simps.verbose] "Warning: Projection {proj.newName} is given manually by the user, \
+          but it can be generated automatically."
         return proj
-      trace[simps.verbose] "Using {indentExpr projExpr}\n for projection {proj.newName}."
+      trace[simps.verbose] "Using {indentExpr projExpr}\nfor projection {proj.newName}."
       return { proj with expr? := some projExpr }
     return proj
   return projs
@@ -1019,8 +1020,8 @@ partial def addProjections (nm : Name) (type lhs rhs : Expr)
       throwError "Invalid `simps` attribute. Target {str} is not a structure"
     if !todoNext.isEmpty && str ∉ cfg.notRecursive then
       let firstTodo := todoNext.head!.1
-      throwError "Invalid simp lemma {nm.appendAfter firstTodo}.\nProjection {
-        (firstTodo.splitOn "_")[1]!} doesn't exist, because target {str} is not a structure."
+      throwError "Invalid simp lemma {nm.appendAfter firstTodo}.\nProjection \
+        {(firstTodo.splitOn "_")[1]!} doesn't exist, because target {str} is not a structure."
     if cfg.fullyApplied then
       addProjection stxProj univs nm tgt lhsAp rhsAp newArgs cfg
     else
@@ -1044,37 +1045,38 @@ partial def addProjections (nm : Name) (type lhs rhs : Expr)
     -- if I'm about to run into an error, try to set the transparency for `rhsMd` higher.
     if cfg.rhsMd == .reducible && (mustBeStr || !todoNext.isEmpty || !toApply.isEmpty) then
       trace[simps.debug] "Using relaxed reducibility."
-      Linter.logLintIf linter.simpsNoConstructor ref
-        m!"The definition {nm} is not a constructor application. Please use `@[simps!]` instead.{
-        ""}\n\nExplanation: `@[simps]` uses the definition to find what the simp lemmas should {
-        ""}be. If the definition is a constructor, then this is easy, since the values of the {
-        ""}projections are just the arguments to the constructor. If the definition is not a {
-        ""}constructor, then `@[simps]` will unfold the right-hand side until it has found a {
-        ""}constructor application, and uses those values.\n\n{
-        ""}This might not always result in the simp-lemmas you want, so you are advised to use {
-        ""}`@[simps?]` to double-check whether `@[simps]` generated satisfactory lemmas.\n{
-        ""}Note 1: `@[simps!]` also calls the `simp` tactic, and this can be expensive in certain {
-        ""}cases.\n{
-        ""}Note 2: `@[simps!]` is equivalent to `@[simps (config := \{rhsMd := .default, {
-        ""}simpRhs := true})]`. You can also try `@[simps (config := \{rhsMd := .default})]` {
-        ""}to still unfold the definitions, but avoid calling `simp` on the resulting statement.\n{
-        ""}Note 3: You need `simps!` if not all fields are given explicitly in this definition, {
-        ""}even if the definition is a constructor application. For example, if you give a {
-        ""}`MulEquiv` by giving the corresponding `Equiv` and the proof that it respects {
-        ""}multiplication, then you need to mark it as `@[simps!]`, since the attribute needs to {
-        ""}unfold the corresponding `Equiv` to get to the `toFun` field."
+      Linter.logLintIf linter.simpsNoConstructor ref m!"\
+        The definition {nm} is not a constructor application. Please use `@[simps!]` instead.\n\
+        \n\
+        Explanation: `@[simps]` uses the definition to find what the simp lemmas should \
+        be. If the definition is a constructor, then this is easy, since the values of the \
+        projections are just the arguments to the constructor. If the definition is not a \
+        constructor, then `@[simps]` will unfold the right-hand side until it has found a \
+        constructor application, and uses those values.\n\n\
+        This might not always result in the simp-lemmas you want, so you are advised to use \
+        `@[simps?]` to double-check whether `@[simps]` generated satisfactory lemmas.\n\
+        Note 1: `@[simps!]` also calls the `simp` tactic, and this can be expensive in certain \
+        cases.\n\
+        Note 2: `@[simps!]` is equivalent to `@[simps (config := \{rhsMd := .default, \
+        simpRhs := true})]`. You can also try `@[simps (config := \{rhsMd := .default})]` \
+        to still unfold the definitions, but avoid calling `simp` on the resulting statement.\n\
+        Note 3: You need `simps!` if not all fields are given explicitly in this definition, \
+        even if the definition is a constructor application. For example, if you give a \
+        `MulEquiv` by giving the corresponding `Equiv` and the proof that it respects \
+        multiplication, then you need to mark it as `@[simps!]`, since the attribute needs to \
+        unfold the corresponding `Equiv` to get to the `toFun` field."
       let nms ← addProjections nm type lhs rhs args mustBeStr
         { cfg with rhsMd := .default, simpRhs := true } todo toApply
       return if addThisProjection then nms.push nm else nms
     if !toApply.isEmpty then
-      throwError "Invalid simp lemma {nm}.\nThe given definition is not a constructor {""
-        }application:{indentExpr rhsWhnf}"
+      throwError "Invalid simp lemma {nm}.\nThe given definition is not a constructor \
+        application:{indentExpr rhsWhnf}"
     if mustBeStr then
-      throwError "Invalid `simps` attribute. The body is not a constructor application:{
-        indentExpr rhsWhnf}"
+      throwError "Invalid `simps` attribute. The body is not a constructor application:\
+        {indentExpr rhsWhnf}"
     if !todoNext.isEmpty then
-      throwError "Invalid simp lemma {nm.appendAfter todoNext.head!.1}.\n{""
-        }The given definition is not a constructor application:{indentExpr rhsWhnf}"
+      throwError "Invalid simp lemma {nm.appendAfter todoNext.head!.1}.\n\
+        The given definition is not a constructor application:{indentExpr rhsWhnf}"
     if !addThisProjection then
       if cfg.fullyApplied then
         addProjection stxProj univs nm tgt lhsAp rhsEta newArgs cfg
@@ -1090,8 +1092,8 @@ partial def addProjections (nm : Name) (type lhs rhs : Expr)
     let some ⟨newRhs, _⟩ := projInfo[idx]?
       | throwError "unreachable: index of composite projection is out of bounds."
     let newType ← inferType newRhs
-    trace[simps.debug] "Applying a custom composite projection. Todo: {toApply}. Current lhs:{
-      indentExpr lhsAp}"
+    trace[simps.debug] "Applying a custom composite projection. Todo: {toApply}. Current lhs:\
+      {indentExpr lhsAp}"
     return ← addProjections nm newType lhsAp newRhs newArgs false cfg todo rest
   trace[simps.debug] "Not in the middle of applying a custom composite projection"
   /- We stop if no further projection is specified or if we just reduced an eta-expansion and we
@@ -1105,11 +1107,14 @@ partial def addProjections (nm : Name) (type lhs rhs : Expr)
     fun proj ↦ !(proj.getString ++ "_").isPrefixOf x then
     let simpLemma := nm.appendAfter x
     let neededProj := (x.splitOn "_")[0]!
-    throwError "Invalid simp lemma {simpLemma}. Structure {str} does not have projection {""
-      }{neededProj}.\nThe known projections are:\n  {projs}\nYou can also see this information {""
-      }by running\n  `initialize_simps_projections? {str}`.\nNote: these projection names might {""
-      }be customly defined for `simps`, and could differ from the projection names of the {""
-      }structure."
+    throwError "Invalid simp lemma {simpLemma}. \
+      Structure {str} does not have projection {neededProj}.\n\
+      The known projections are:\
+      {indentD <| toMessageData projs}\n\
+      You can also see this information by running\
+      \n  `initialize_simps_projections? {str}`.\n\
+      Note: these projection names might be customly defined for `simps`, \
+      and could differ from the projection names of the structure."
   let nms ← projInfo.concatMapM fun ⟨newRhs, proj, projExpr, projNrs, isDefault, isPrefix⟩ ↦ do
     let newType ← inferType newRhs
     let newTodo := todo.filterMap
diff --git a/Mathlib/Tactic/Simps/NotationClass.lean b/Mathlib/Tactic/Simps/NotationClass.lean
index 5c16cb4328b21..c86ffb059e124 100644
--- a/Mathlib/Tactic/Simps/NotationClass.lean
+++ b/Mathlib/Tactic/Simps/NotationClass.lean
@@ -53,8 +53,8 @@ def defaultfindArgs : findArgType := λ _ className args => do
   else if args.size == 1 then
     return mkArray arity args[0]!
   else
-    throwError "initialize_simps_projections cannot automatically find arguments for class {
-      className}"
+    throwError "initialize_simps_projections cannot automatically find arguments for class \
+      {className}"
 
 /-- Find arguments by duplicating the first argument. Used for `pow`. -/
 def copyFirst : findArgType := λ _ _ args => return (args.push <| args[0]?.getD default).map some
diff --git a/Mathlib/Tactic/TermCongr.lean b/Mathlib/Tactic/TermCongr.lean
index 702e0a0a7dc5e..8194e30a1f9e9 100644
--- a/Mathlib/Tactic/TermCongr.lean
+++ b/Mathlib/Tactic/TermCongr.lean
@@ -282,8 +282,8 @@ Throws an error if the `lhs` and `rhs` have non-defeq types.
 If `pf? = none`, this returns the `rfl` proof. -/
 def CongrResult.eq (res : CongrResult) : MetaM Expr := do
   unless ← isDefEq (← inferType res.lhs) (← inferType res.rhs) do
-    throwError "Expecting{indentD res.lhs}\nand{indentD res.rhs}\n{""
-      }to have definitionally equal types."
+    throwError "Expecting{indentD res.lhs}\nand{indentD res.rhs}\n\
+      to have definitionally equal types."
   match res.pf? with
   | some pf => pf .eq
   | none => mkEqRefl res.lhs
@@ -369,11 +369,11 @@ where
     let some (_, lhs', _, rhs') := (← whnf pfTy).sides?
       | panic! "Unexpectedly did not generate an eq or heq"
     unless ← isDefEq lhs lhs' do
-      throwError "Congruence hole has type{indentD pfTy}\n{""
-        }but its left-hand side is not definitionally equal to the expected value{indentD lhs}"
+      throwError "Congruence hole has type{indentD pfTy}\n\
+        but its left-hand side is not definitionally equal to the expected value{indentD lhs}"
     unless ← isDefEq rhs rhs' do
-      throwError "Congruence hole has type{indentD pfTy}\n{""
-        }but its right-hand side is not definitionally equal to the expected value{indentD rhs}"
+      throwError "Congruence hole has type{indentD pfTy}\n\
+        but its right-hand side is not definitionally equal to the expected value{indentD rhs}"
     return pf
 
 /-- Force the lhs and rhs to be defeq. For when `dsimp`-like congruence is necessary.
@@ -383,8 +383,8 @@ def CongrResult.defeq (res : CongrResult) : MetaM CongrResult := do
     return res
   else
     unless ← isDefEq res.lhs res.rhs do
-      throwError "Cannot generate congruence because we need{indentD res.lhs}\n{""
-        }to be definitionally equal to{indentD res.rhs}"
+      throwError "Cannot generate congruence because we need{indentD res.lhs}\n\
+        to be definitionally equal to{indentD res.rhs}"
     -- Propagate types into any proofs that we're dropping:
     discard <| res.eq
     return {res with pf? := none}
@@ -417,8 +417,8 @@ def CongrResult.mkDefault' (mvarCounterSaved : Nat) (lhs rhs : Expr) : MetaM Con
 
 /-- Throw an internal error. -/
 def throwCongrEx (lhs rhs : Expr) (msg : MessageData) : MetaM α := do
-  throwError "congr(...) failed with left-hand side{indentD lhs}\n{""
-    }and right-hand side {indentD rhs}\n{msg}"
+  throwError "congr(...) failed with left-hand side{indentD lhs}\n\
+    and right-hand side {indentD rhs}\n{msg}"
 
 /-- If `lhs` or `rhs` is a congruence hole, then process it.
 Only process ones that are at least as new as `mvarCounterSaved`
@@ -436,11 +436,11 @@ def mkCongrOfCHole? (mvarCounterSaved : Nat) (lhs rhs : Expr) : MetaM (Option Co
       throwCongrEx lhs rhs "Elaborated types of congruence holes are not defeq."
     if let some (_, lhsVal, _, rhsVal) := (← whnf <| ← inferType pf1).sides? then
       unless ← isDefEq val1 lhsVal do
-        throwError "Left-hand side of congruence hole is{indentD lhsVal}\n{""
-          }but is expected to be{indentD val1}"
+        throwError "Left-hand side of congruence hole is{indentD lhsVal}\n\
+          but is expected to be{indentD val1}"
       unless ← isDefEq val2 rhsVal do
-        throwError "Right-hand side of congruence hole is{indentD rhsVal}\n{""
-          }but is expected to be{indentD val2}"
+        throwError "Right-hand side of congruence hole is{indentD rhsVal}\n\
+          but is expected to be{indentD val2}"
     return some <| CongrResult.mk' val1 val2 pf1
   | some .., none =>
     throwCongrEx lhs rhs "Right-hand side lost its congruence hole annotation."
@@ -616,11 +616,11 @@ def elabTermCongr : Term.TermElab := fun stx expectedType? => do
         let rhs ← elaboratePattern t expRhsTy false
         -- Note: these defeq checks can leak congruence holes.
         unless ← isDefEq expLhs lhs do
-          throwError "Left-hand side of elaborated pattern{indentD lhs}\n{""
-            }is not definitionally equal to left-hand side of expected type{indentD expectedType}"
+          throwError "Left-hand side of elaborated pattern{indentD lhs}\n\
+            is not definitionally equal to left-hand side of expected type{indentD expectedType}"
         unless ← isDefEq expRhs rhs do
-          throwError "Right-hand side of elaborated pattern{indentD rhs}\n{""
-            }is not definitionally equal to right-hand side of expected type{indentD expectedType}"
+          throwError "Right-hand side of elaborated pattern{indentD rhs}\n\
+            is not definitionally equal to right-hand side of expected type{indentD expectedType}"
         Term.synthesizeSyntheticMVars (mayPostpone := true)
         let res ← mkCongrOf 0 mvarCounterSaved lhs rhs
         let expectedType' ← whnf expectedType
diff --git a/Mathlib/Tactic/ToAdditive.lean b/Mathlib/Tactic/ToAdditive.lean
index 6320f881ccf17..83bb87dd8afea 100644
--- a/Mathlib/Tactic/ToAdditive.lean
+++ b/Mathlib/Tactic/ToAdditive.lean
@@ -115,14 +115,14 @@ register_option linter.toAdditiveReorder : Bool := {
 certain attributes -/
 register_option linter.existingAttributeWarning : Bool := {
   defValue := true
-  descr := "Linter, mostly used by `@[to_additive]`, that checks that the source declaration " ++
-    "doesn't have certain attributes" }
+  descr := "Linter, mostly used by `@[to_additive]`, that checks that the source declaration \
+    doesn't have certain attributes" }
 
 /-- Linter to check that the `to_additive` attribute is not given manually -/
 register_option linter.toAdditiveGenerateName : Bool := {
   defValue := true
-  descr := "Linter used by `@[to_additive]` that checks if `@[to_additive]` automatically " ++
-    "generates the user-given name" }
+  descr := "Linter used by `@[to_additive]` that checks if `@[to_additive]` automatically \
+    generates the user-given name" }
 
 /-- Linter to check whether the user correctly specified that the additive declaration already
 exists -/
@@ -157,17 +157,17 @@ applying `@[to_additive]`. It is applied automatically by the `(reorder := ...)`
 initialize reorderAttr : NameMapExtension (List $ List Nat) ←
   registerNameMapAttribute {
     name := `to_additive_reorder
-    descr :=
-      "Auxiliary attribute for `to_additive` that stores arguments that need to be reordered.
-        This should not appear in any file.
-        We keep it as an attribute for now so that mathport can still use it, and it can generate a
-        warning."
+    descr := "\
+      Auxiliary attribute for `to_additive` that stores arguments that need to be reordered. \
+      This should not appear in any file. \
+      We keep it as an attribute for now so that mathport can still use it, and it can generate a \
+      warning."
     add := fun
     | _, stx@`(attr| to_additive_reorder $[$[$reorders:num]*],*) => do
-      Linter.logLintIf linter.toAdditiveReorder stx
-        m!"Using this attribute is deprecated. Use `@[to_additive (reorder := <num>)]` {""
-        }instead.\nThat will also generate the additive version with the arguments swapped, {""
-        }so you are probably able to remove the manually written additive declaration."
+      Linter.logLintIf linter.toAdditiveReorder stx m!"\
+        Using this attribute is deprecated. Use `@[to_additive (reorder := <num>)]` instead.\n\n\
+        That will also generate the additive version with the arguments swapped, \
+        so you are probably able to remove the manually written additive declaration."
       pure <| reorders.toList.map (·.toList.map (·.raw.isNatLit?.get! - 1))
     | _, _ => throwUnsupportedSyntax }
 
@@ -194,8 +194,8 @@ Warning: interactions between this and the `(reorder := ...)` argument are not w
 initialize relevantArgAttr : NameMapExtension Nat ←
   registerNameMapAttribute {
     name := `to_additive_relevant_arg
-    descr := "Auxiliary attribute for `to_additive` stating" ++
-      " which arguments are the types with a multiplicative structure."
+    descr := "Auxiliary attribute for `to_additive` stating \
+      which arguments are the types with a multiplicative structure."
     add := fun
     | _, `(attr| to_additive_relevant_arg $id) => pure <| id.1.isNatLit?.get!.pred
     | _, _ => throwUnsupportedSyntax }
@@ -390,8 +390,8 @@ where /-- Implementation of `applyReplacementFun`. -/
               if let some fxd := additiveTest findTranslation? ignore gAllArgs[relevantArgId]! then
                 Id.run <| do
                   if trace then
-                    dbg_trace s!"The application of {nm} contains the fixed type {fxd
-                      }, so it is not changed"
+                    dbg_trace s!"The application of {nm} contains the fixed type \
+                      {fxd}, so it is not changed"
                   gf
               else
                 r gf
@@ -409,8 +409,8 @@ where /-- Implementation of `applyReplacementFun`. -/
           if let some changedArgNrs := changeNumeral? nm then
             if additiveTest findTranslation? ignore firstArg |>.isNone then
               if trace then
-                dbg_trace s!"applyReplacementFun: We change the numerals in this expression. {
-                  ""}However, we will still recurse into all the non-numeral arguments."
+                dbg_trace s!"applyReplacementFun: We change the numerals in this expression. \
+                  However, we will still recurse into all the non-numeral arguments."
               -- In this case, we still update all arguments of `g` that are not numerals,
               -- since all other arguments can contain subexpressions like
               -- `(fun x ↦ ℕ) (1 : G)`, and we have to update the `(1 : G)` to `(0 : G)`
@@ -426,8 +426,8 @@ where /-- Implementation of `applyReplacementFun`. -/
     | .proj n₀ idx e => do
       let n₁ := n₀.mapPrefix findTranslation?
       if trace then
-        dbg_trace s!"applyReplacementFun: in projection {e}.{idx} of type {n₀}, {""
-          }replace type with {n₁}"
+        dbg_trace s!"applyReplacementFun: in projection {e}.{idx} of type {n₀}, \
+          replace type with {n₁}"
       return some <| .proj n₁ idx <| ← r e
     | _ => return none
 
@@ -545,9 +545,9 @@ partial def transformDeclAux
   -- if this declaration is not `pre` and not an internal declaration, we return an error,
   -- since we should have already translated this declaration.
   if src != pre && !src.isInternalDetail then
-    throwError "The declaration {pre} depends on the declaration {src} which is in the namespace {
-      pre}, but does not have the `@[to_additive]` attribute. This is not supported.\n{""
-      }Workaround: move {src} to a different namespace."
+    throwError "The declaration {pre} depends on the declaration {src} which is in the namespace \
+      {pre}, but does not have the `@[to_additive]` attribute. This is not supported.\n\
+      Workaround: move {src} to a different namespace."
   -- we find the additive name of `src`
   let tgt ← findTargetName env src pre tgt_pre
   -- we skip if we already transformed this declaration before.
@@ -584,9 +584,9 @@ partial def transformDeclAux
     -- and emit a more helpful error message if it fails
     discard <| MetaM.run' <| inferType value
   catch
-    | Exception.error _ msg => throwError "@[to_additive] failed.
-      Type mismatch in additive declaration. For help, see the docstring
-      of `to_additive.attr`, section `Troubleshooting`.
+    | Exception.error _ msg => throwError "@[to_additive] failed. \
+      Type mismatch in additive declaration. For help, see the docstring \
+      of `to_additive.attr`, section `Troubleshooting`. \
       Failed to add declaration\n{tgt}:\n{msg}"
     | _ => panic! "unreachable"
   if isNoncomputable env src then
@@ -618,13 +618,14 @@ def warnExt [Inhabited σ] (stx : Syntax) (ext : PersistentEnvExtension α β σ
     (thisAttr attrName src tgt : Name) : CoreM Unit := do
   if f (ext.getState (← getEnv)) src then
     Linter.logLintIf linter.existingAttributeWarning stx <|
-      m!"The source declaration {src} was given attribute {attrName} before calling @[{thisAttr}]. {
-      ""}The preferred method is to use `@[{thisAttr} (attr := {attrName})]` to apply the {
-      ""}attribute to both {src} and the target declaration {tgt}." ++
+      m!"The source declaration {src} was given attribute {attrName} before calling @[{thisAttr}]. \
+         The preferred method is to use `@[{thisAttr} (attr := {attrName})]` to apply the \
+         attribute to both {src} and the target declaration {tgt}." ++
       if thisAttr == `to_additive then
-      m!"\nSpecial case: If this declaration was generated by @[to_additive] {
-      ""}itself, you can use @[to_additive (attr := to_additive, {attrName})] on the original {
-      ""}declaration." else ""
+        m!"\nSpecial case: If this declaration was generated by @[to_additive] \
+          itself, you can use @[to_additive (attr := to_additive, {attrName})] on the original \
+          declaration."
+      else ""
 
 /-- Warn the user when the multiplicative declaration has a simple scoped attribute. -/
 def warnAttr [Inhabited β] (stx : Syntax) (attr : SimpleScopedEnvExtension α β)
@@ -841,9 +842,9 @@ def targetName (cfg : Config) (src : Name) : CoreM Name := do
   let pre := pre.mapPrefix <| findTranslation? (← getEnv)
   let (pre1, pre2) := pre.splitAt (depth - 1)
   if cfg.tgt == pre2.str tgt_auto && !cfg.allowAutoName && cfg.tgt != src then
-    Linter.logLintIf linter.toAdditiveGenerateName cfg.ref
-      m!"to_additive correctly autogenerated target name for {src}. {"\n"
-      }You may remove the explicit argument {cfg.tgt}."
+    Linter.logLintIf linter.toAdditiveGenerateName cfg.ref m!"\
+      to_additive correctly autogenerated target name for {src}.\n\
+      You may remove the explicit argument {cfg.tgt}."
   let res := if cfg.tgt == .anonymous then pre.str tgt_auto else pre1 ++ cfg.tgt
   -- we allow translating to itself if `tgt == src`, which is occasionally useful for `additiveTest`
   if res == src && cfg.tgt != src then
@@ -915,11 +916,11 @@ partial def applyAttributes (stx : Syntax) (rawAttrs : Array Syntax) (thisAttr s
   if linter.existingAttributeWarning.get (← getOptions) then
     let appliedAttrs ← getAllSimpAttrs src
     if appliedAttrs.size > 0 then
-      Linter.logLintIf linter.existingAttributeWarning stx <|
-        m!"The source declaration {src} was given the simp-attribute(s) {appliedAttrs} before {
-        ""}calling @[{thisAttr}]. The preferred method is to use {
-        ""}`@[{thisAttr} (attr := {appliedAttrs})]` to apply the attribute to both {
-        src} and the target declaration {tgt}."
+      Linter.logLintIf linter.existingAttributeWarning stx m!"\
+        The source declaration {src} was given the simp-attribute(s) {appliedAttrs} before \
+        calling @[{thisAttr}]. The preferred method is to use \
+        `@[{thisAttr} (attr := {appliedAttrs})]` to apply the attribute to both \
+        {src} and the target declaration {tgt}."
     warnAttr stx Std.Tactic.Ext.extExtension
       (fun b n => (b.tree.values.any fun t => t.declName = n)) thisAttr `ext src tgt
     warnAttr stx Std.Tactic.reflExt (·.values.contains ·) thisAttr `refl src tgt
@@ -1015,8 +1016,8 @@ partial def addToAdditiveAttr (src : Name) (cfg : Config) (kind := AttributeKind
   if cfg.existing == some !alreadyExists && !(← isInductive src) then
     Linter.logLintIf linter.toAdditiveExisting cfg.ref <|
       if alreadyExists then
-        m!"The additive declaration already exists. Please specify this explicitly using {
-          ""}`@[to_additive existing]`."
+        m!"The additive declaration already exists. Please specify this explicitly using \
+           `@[to_additive existing]`."
       else
         "The additive declaration doesn't exist. Please remove the option `existing`."
   if cfg.reorder != [] then
diff --git a/Mathlib/Tactic/Variable.lean b/Mathlib/Tactic/Variable.lean
index 40ca7d7cd437c..492733e07cb7f 100644
--- a/Mathlib/Tactic/Variable.lean
+++ b/Mathlib/Tactic/Variable.lean
@@ -161,21 +161,21 @@ partial def completeBinders' (maxSteps : Nat) (gas : Nat)
     TermElabM (TSyntaxArray ``bracketedBinder × Array Bool) := do
   if 0 < gas && i < binders.size then
     let binder := binders[i]!
-    trace[«variable?»]
-      "Have {(← getLCtx).getFVarIds.size} fvars and {(← getLocalInstances).size} local instances{
-      ""}. Looking at{indentD binder}"
+    trace[«variable?»] "\
+      Have {(← getLCtx).getFVarIds.size} fvars and {(← getLocalInstances).size} local instances. \
+      Looking at{indentD binder}"
     let sub? ← getSubproblem binder (bracketedBinderType binder).get!
     if let some (goalMsg, binder') := sub? then
       trace[«variable?»] m!"new subproblem:{indentD binder'}"
       if binders.any (stop := i) (· == binder') then
         let binders' := binders.extract 0 i
-        throwErrorAt binder
-          "Binder{indentD binder}\nwas not able to satisfy one of its dependencies using {
-          ""}the pre-existing binder{indentD binder'}\n\n{
-          ""}This might be due to differences in implicit arguments, which are not represented {
-          ""}in binders since they are generated by pretty printing unsatisfied dependencies.\n\n{
-          ""}Current variable command:{indentD (← `(command| variable $binders'*))}\n\n{
-          ""}Local context for the unsatisfied dependency:{goalMsg}"
+        throwErrorAt binder "\
+          Binder{indentD binder}\nwas not able to satisfy one of its dependencies using \
+          the pre-existing binder{indentD binder'}\n\n\
+          This might be due to differences in implicit arguments, which are not represented \
+          in binders since they are generated by pretty printing unsatisfied dependencies.\n\n\
+          Current variable command:{indentD (← `(command| variable $binders'*))}\n\n\
+          Local context for the unsatisfied dependency:{goalMsg}"
       let binders := binders.insertAt! i binder'
       completeBinders' maxSteps (gas - 1) checkRedundant binders toOmit i
     else
@@ -215,9 +215,9 @@ partial def completeBinders' (maxSteps : Nat) (gas : Nat)
   else
     if gas == 0 && i < binders.size then
       let binders' := binders.extract 0 i
-      logErrorAt binders[i]! m!"Maximum recursion depth for variables! reached. This might be a {
-        ""}bug, or you can try adjusting `set_option variable?.maxSteps {maxSteps}`{
-        ""}\n\nCurrent variable command:{indentD (← `(command| variable $binders'*))}"
+      logErrorAt binders[i]! m!"Maximum recursion depth for variables! reached. This might be a \
+        bug, or you can try adjusting `set_option variable?.maxSteps {maxSteps}`\n\n\
+        Current variable command:{indentD (← `(command| variable $binders'*))}"
     return (binders, toOmit)
 where
   isVariableAlias (type : Expr) : MetaM Bool := do
diff --git a/Mathlib/Tactic/Widget/Calc.lean b/Mathlib/Tactic/Widget/Calc.lean
index 0e2a1c8d4b2cf..abc5859ec2dbf 100644
--- a/Mathlib/Tactic/Widget/Calc.lean
+++ b/Mathlib/Tactic/Widget/Calc.lean
@@ -86,11 +86,12 @@ def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (par
   let insertedCode := match isSelectedLeft, isSelectedRight with
   | true, true =>
     if params.isFirst then
-      s!"{lhsStr} {relStr} {newLhsStr} := by sorry\n{spc}_ {relStr} {newRhsStr} := by sorry\n" ++
-      s!"{spc}_ {relStr} {rhsStr} := by sorry"
+      s!"{lhsStr} {relStr} {newLhsStr} := by sorry\n{spc}_ {relStr} {newRhsStr} := by sorry\n\
+         {spc}_ {relStr} {rhsStr} := by sorry"
     else
-      s!"_ {relStr} {newLhsStr} := by sorry\n{spc}_ {relStr} {newRhsStr} := by sorry\n" ++
-      s!"{spc}_ {relStr} {rhsStr} := by sorry"
+      s!"_ {relStr} {newLhsStr} := by sorry\n{spc}\
+         _ {relStr} {newRhsStr} := by sorry\n{spc}\
+         _ {relStr} {rhsStr} := by sorry"
   | false, true =>
     if params.isFirst then
       s!"{lhsStr} {relStr} {newRhsStr} := by sorry\n{spc}_ {relStr} {rhsStr} := by sorry"
diff --git a/Mathlib/Util/AssertExists.lean b/Mathlib/Util/AssertExists.lean
index 4c901b2d562da..41691c9dad605 100644
--- a/Mathlib/Util/AssertExists.lean
+++ b/Mathlib/Util/AssertExists.lean
@@ -49,7 +49,7 @@ You should *not* delete the `assert_not_exists` statement without careful discus
 -/
 elab "assert_not_exists " n:ident : command =>
   do let [] ← try resolveGlobalConstWithInfos n catch _ => return
-      | throw <| .error n <| m!"Declaration {n} is not allowed to be imported by this file.\n\n{
-           ""}These invariants are maintained by `assert_not_exists` statements, {
-           ""}and exist in order to ensure that \"complicated\" parts of the library {
-           ""}are not accidentally introduced as dependencies of \"simple\" parts of the library."
+      | throw <| .error n m!"Declaration {n} is not allowed to be imported by this file.\n\n\
+          These invariants are maintained by `assert_not_exists` statements, \
+          and exist in order to ensure that \"complicated\" parts of the library \
+          are not accidentally introduced as dependencies of \"simple\" parts of the library."
diff --git a/Mathlib/Util/Imports.lean b/Mathlib/Util/Imports.lean
index 7bbe6ecf4f006..146934733ce73 100644
--- a/Mathlib/Util/Imports.lean
+++ b/Mathlib/Util/Imports.lean
@@ -190,8 +190,8 @@ elab "#redundant_imports" : command => do
   if redundant.isEmpty then
     logInfo "No transitively redundant imports found."
   else
-    logInfo <| "Found the following transitively redundant imports:\n" ++
-      m!"{Format.joinSep redundant.toList "\n"}"
+    logInfo m!"Found the following transitively redundant imports:\n\
+      {Format.joinSep redundant.toList "\n"}"
 
 /--
 Return the names of the modules in which constants used in the current file were defined,
diff --git a/test/GCongr/inequalities.lean b/test/GCongr/inequalities.lean
index cb613c457d211..70caad895e639 100644
--- a/test/GCongr/inequalities.lean
+++ b/test/GCongr/inequalities.lean
@@ -104,7 +104,8 @@ example {x : ℤ} (hx : x ≥ 12) (h : Even x) : Even x := by
 
 example {a b x c d : ℝ} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 1 ≤ x + 1) : x * a + c ≤ x * b + d := by
   success_if_fail_with_msg
-    "rel failed, cannot prove goal by 'substituting' the listed relationships. The steps which could not be automatically justified were: \n0 ≤ x\nc ≤ d"
+    "rel failed, cannot prove goal by 'substituting' the listed relationships. \
+     The steps which could not be automatically justified were:\n0 ≤ x\nc ≤ d"
     (rel [h1])
   have : 0 ≤ x := by linarith
   rel [h1, h2]
diff --git a/test/eqns.lean b/test/eqns.lean
index 1b263d7c7b7f1..25c6c791108d1 100644
--- a/test/eqns.lean
+++ b/test/eqns.lean
@@ -22,7 +22,7 @@ theorem t_def : t = 1 := rfl
 theorem t_def' : t = 1 := by rw [t]
 
 /--
-error: There already exist stored eqns for 't' registering new equations
+error: There already exist stored eqns for 't'; registering new equations
 will not have the desired effect.
 -/
 #guard_msgs(error) in