diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean
index c2c981c16f..2a9afcc719 100644
--- a/src/Init/Data/Format/Basic.lean
+++ b/src/Init/Data/Format/Basic.lean
@@ -142,17 +142,36 @@ private structure WorkItem where
   indent : Int
   activeTags : Nat
 
+/--
+A directive indicating whether a given work group is able to be flattened.
+
+- `allow` indicates that the group is allowed to be flattened; its argument is `true` if
+  there is sufficient space for it to be flattened (and so it should be), or `false` if not.
+- `disallow` means that this group should not be flattened irrespective of space concerns.
+  This is used at levels of a `Format` outside of any flattening groups. It is necessary to track
+  this so that, after a hard line break, we know whether to try to flatten the next line.
+-/
+inductive FlattenAllowability where
+  | allow (fits : Bool)
+  | disallow
+  deriving BEq
+
+/-- Whether the given directive indicates that flattening should occur. -/
+def FlattenAllowability.shouldFlatten : FlattenAllowability → Bool
+  | allow true => true
+  | _ => false
+
 private structure WorkGroup where
-  flatten : Bool
-  flb     : FlattenBehavior
-  items   : List WorkItem
+  fla   : FlattenAllowability
+  flb   : FlattenBehavior
+  items : List WorkItem
 
 private partial def spaceUptoLine' : List WorkGroup → Nat → Nat → SpaceResult
   |   [],                         _,   _ => {}
   |   { items := [],    .. }::gs, col, w => spaceUptoLine' gs col w
   | g@{ items := i::is, .. }::gs, col, w =>
     merge w
-      (spaceUptoLine i.f g.flatten (w + col - i.indent) w)
+      (spaceUptoLine i.f g.fla.shouldFlatten (w + col - i.indent) w)
       (spaceUptoLine' ({ g with items := is }::gs) col)
 
 /-- A monad in which we can pretty-print `Format` objects. -/
@@ -169,11 +188,11 @@ open MonadPrettyFormat
 private def pushGroup (flb : FlattenBehavior) (items : List WorkItem) (gs : List WorkGroup) (w : Nat) [Monad m] [MonadPrettyFormat m] : m (List WorkGroup) := do
   let k  ← currColumn
   -- Flatten group if it + the remainder (gs) fits in the remaining space. For `fill`, measure only up to the next (ungrouped) line break.
-  let g  := { flatten := flb == FlattenBehavior.allOrNone, flb := flb, items := items : WorkGroup }
+  let g  := { fla := .allow (flb == FlattenBehavior.allOrNone), flb := flb, items := items : WorkGroup }
   let r  := spaceUptoLine' [g] k (w-k)
   let r' := merge (w-k) r (spaceUptoLine' gs k)
   -- Prevent flattening if any item contains a hard line break, except within `fill` if it is ungrouped (=> unflattened)
-  return { g with flatten := !r.foundFlattenedHardLine && r'.space <= w-k }::gs
+  return { g with fla := .allow (!r.foundFlattenedHardLine && r'.space <= w-k) }::gs
 
 private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGroup → m Unit
   | []                           => pure ()
@@ -200,11 +219,15 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
         pushNewline i.indent.toNat
         let is := { i with f := text (s.extract (s.next p) s.endPos) }::is
         -- after a hard line break, re-evaluate whether to flatten the remaining group
-        pushGroup g.flb is gs w >>= be w
+        -- note that we shouldn't start flattening after a hard break outside a group
+        if g.fla == .disallow then
+          be w (gs' is)
+        else
+          pushGroup g.flb is gs w >>= be w
     | line =>
       match g.flb with
       | FlattenBehavior.allOrNone =>
-        if g.flatten then
+        if g.fla.shouldFlatten then
           -- flatten line = text " "
           pushOutput " "
           endTags i.activeTags
@@ -220,10 +243,10 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
           endTags i.activeTags
           pushGroup FlattenBehavior.fill is gs w >>= be w
         -- if preceding fill item fit in a single line, try to fit next one too
-        if g.flatten then
+        if g.fla.shouldFlatten then
           let gs'@(g'::_) ← pushGroup FlattenBehavior.fill is gs (w - " ".length)
             | panic "unreachable"
-          if g'.flatten then
+          if g'.fla.shouldFlatten then
             pushOutput " "
             endTags i.activeTags
             be w gs'  -- TODO: use `return`
@@ -232,7 +255,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
         else
           breakHere
     | align force =>
-      if g.flatten && !force then
+      if g.fla.shouldFlatten && !force then
         -- flatten (align false) = nil
         endTags i.activeTags
         be w (gs' is)
@@ -247,7 +270,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
           endTags i.activeTags
           be w (gs' is)
     | group f flb =>
-      if g.flatten then
+      if g.fla.shouldFlatten then
         -- flatten (group f) = flatten f
         be w (gs' ({ i with f }::is))
       else
@@ -256,7 +279,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
 /-- Render the given `f : Format` with a line width of `w`.
 `indent` is the starting amount to indent each line by. -/
 def prettyM (f : Format) (w : Nat) (indent : Nat := 0) [Monad m] [MonadPrettyFormat m] : m Unit :=
-  be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent, activeTags := 0 }]}]
+  be w [{ flb := FlattenBehavior.allOrNone, fla := .disallow, items := [{ f := f, indent, activeTags := 0 }]}]
 
 /-- Create a format `l ++ f ++ r` with a flatten group.
 FlattenBehaviour is `allOrNone`; for `fill` use `bracketFill`. -/
diff --git a/tests/lean/1079.lean.expected.out b/tests/lean/1079.lean.expected.out
index f90c4de209..a715447b14 100644
--- a/tests/lean/1079.lean.expected.out
+++ b/tests/lean/1079.lean.expected.out
@@ -11,4 +11,7 @@
       ?a = ?a
     with
       Ordering.eq = Ordering.lt
-[Meta.Tactic.simp.rewrite] imp_self:10000: False → False ==> True
+[Meta.Tactic.simp.rewrite] imp_self:10000:
+      False → False
+    ==>
+      True
diff --git a/tests/lean/973b.lean.expected.out b/tests/lean/973b.lean.expected.out
index 249335fe41..573180ab90 100644
--- a/tests/lean/973b.lean.expected.out
+++ b/tests/lean/973b.lean.expected.out
@@ -1,5 +1,6 @@
 973b.lean:5:8-5:10: warning: declaration uses 'sorry'
 [Meta.Tactic.simp.discharge] ex discharge ❌️
       ?p x
-[Meta.Tactic.simp.discharge] ex discharge ❌️ ?p (f x)
+[Meta.Tactic.simp.discharge] ex discharge ❌️
+      ?p (f x)
 973b.lean:9:8-9:11: warning: declaration uses 'sorry'
diff --git a/tests/lean/discrTreeIota.lean.expected.out b/tests/lean/discrTreeIota.lean.expected.out
index f769cff125..f7247adcd5 100644
--- a/tests/lean/discrTreeIota.lean.expected.out
+++ b/tests/lean/discrTreeIota.lean.expected.out
@@ -2,4 +2,7 @@
       default
     ==>
       PUnit.unit
-[Meta.Tactic.simp.rewrite] eq_self:1000: PUnit.unit = x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      PUnit.unit = x
+    ==>
+      True
diff --git a/tests/lean/exceptionalTrace.lean.expected.out b/tests/lean/exceptionalTrace.lean.expected.out
index 5e9622086b..df628a5c5c 100644
--- a/tests/lean/exceptionalTrace.lean.expected.out
+++ b/tests/lean/exceptionalTrace.lean.expected.out
@@ -5,4 +5,5 @@ use `set_option diagnostics true` to get diagnostic information
     rt + 1
   [Elab.step] expected type: <not-available>, term
       binop% HAdd.hAdd✝ rt 1
-    [Elab.step] expected type: <not-available>, term rt
+    [Elab.step] expected type: <not-available>, term
+        rt
diff --git a/tests/lean/run/1234.lean b/tests/lean/run/1234.lean
index 59c63f092b..b4bd842987 100644
--- a/tests/lean/run/1234.lean
+++ b/tests/lean/run/1234.lean
@@ -28,7 +28,10 @@ trace: [Meta.Tactic.simp.rewrite] h₁:1000:
       if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩
     ==>
       ⟨v, ⋯⟩
-[Meta.Tactic.simp.rewrite] eq_self:1000: ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      ⟨v, ⋯⟩ = ⟨v, ⋯⟩
+    ==>
+      True
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):
@@ -65,7 +68,10 @@ trace: [Meta.Tactic.simp.rewrite] h₁:1000:
       if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩
     ==>
       ⟨v, ⋯⟩
-[Meta.Tactic.simp.rewrite] eq_self:1000: ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      ⟨v, ⋯⟩ = ⟨v, ⋯⟩
+    ==>
+      True
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):
@@ -100,7 +106,10 @@ trace: [Meta.Tactic.simp.rewrite] h₁:1000:
       if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩
     ==>
       ⟨v, ⋯⟩
-[Meta.Tactic.simp.rewrite] eq_self:1000: ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      ⟨v, ⋯⟩ = ⟨v, ⋯⟩
+    ==>
+      True
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):
diff --git a/tests/lean/run/1380.lean b/tests/lean/run/1380.lean
index d3896189d4..6858b17d54 100644
--- a/tests/lean/run/1380.lean
+++ b/tests/lean/run/1380.lean
@@ -21,7 +21,10 @@ trace: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
         v₁ < v₂
       ==>
         True
-[Meta.Tactic.simp.rewrite] Nat.ne_of_gt:1000: v₂ = v₁ ==> False
+[Meta.Tactic.simp.rewrite] Nat.ne_of_gt:1000:
+      v₂ = v₁
+    ==>
+      False
 -/
 #guard_msgs in
 set_option trace.Meta.Tactic.simp true in
diff --git a/tests/lean/run/1815.lean b/tests/lean/run/1815.lean
index 3b33f5ed8f..8cb4563e0b 100644
--- a/tests/lean/run/1815.lean
+++ b/tests/lean/run/1815.lean
@@ -13,7 +13,10 @@ trace: [Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected Left a ==> d
     ==>
       a * default
 [Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected a * default ==> default * a
-[Meta.Tactic.simp.rewrite] eq_self:1000: Left a = a * default ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      Left a = a * default
+    ==>
+      True
 -/
 #guard_msgs in
 example (a : α) : Left a = Right a := by
diff --git a/tests/lean/run/3257.lean b/tests/lean/run/3257.lean
index 329c452aee..8a448d4518 100644
--- a/tests/lean/run/3257.lean
+++ b/tests/lean/run/3257.lean
@@ -20,7 +20,10 @@ trace: [Meta.Tactic.simp.discharge] bar discharge ✅️
         T
       ==>
         True
-[Meta.Tactic.simp.rewrite] bar:1000: U ==> True
+[Meta.Tactic.simp.rewrite] bar:1000:
+      U
+    ==>
+      True
 -/
 #guard_msgs in
 example : U := by
diff --git a/tests/lean/run/790.lean b/tests/lean/run/790.lean
index e0d88bbe31..368b1084d3 100644
--- a/tests/lean/run/790.lean
+++ b/tests/lean/run/790.lean
@@ -20,7 +20,10 @@ trace: [Meta.Tactic.simp.rewrite] differential_of_linear:1000:
       differential f x dx
     ==>
       f dx
-[Meta.Tactic.simp.rewrite] eq_self:1000: f dx = f dx ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      f dx = f dx
+    ==>
+      True
 -/
 #guard_msgs in
 example {Y : Type} [Vec Y] (f : Nat → Y) (x dx : Nat)
diff --git a/tests/lean/run/binderNameHintSimp.lean b/tests/lean/run/binderNameHintSimp.lean
index 5aaa13178e..da75cc21b4 100644
--- a/tests/lean/run/binderNameHintSimp.lean
+++ b/tests/lean/run/binderNameHintSimp.lean
@@ -17,7 +17,10 @@ trace: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000:
     ==>
       z
 [Meta.Tactic.simp.rewrite] unfold z, z ==> 0
-[Meta.Tactic.simp.rewrite] eq_self:1000: 0 = 0 ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      0 = 0
+    ==>
+      True
 -/
 #guard_msgs in
 example : binderNameHint x y z = 0 := by
diff --git a/tests/lean/run/docstringRewrites.lean b/tests/lean/run/docstringRewrites.lean
index 43ef416a3b..9f4bdc9e89 100644
--- a/tests/lean/run/docstringRewrites.lean
+++ b/tests/lean/run/docstringRewrites.lean
@@ -107,7 +107,9 @@ info: Errors: ⏎
     Missing documentation type
    • "lean-manual://f":
     Unknown documentation type 'f'. Expected 'section'.
-   • "lean-manual://a/": Unknown documentation type 'a'. Expected 'section'.  ⏎
+   • "lean-manual://a/":
+    Unknown documentation type 'a'. Expected 'section'.
+
 ---
 info: Result: "foo [](lean-manual://) [](lean-manual://f) lean-manual://a/b"
 -/
@@ -120,7 +122,9 @@ info: Errors: ⏎
     Missing documentation type
    • "lean-manual://f":
     Unknown documentation type 'f'. Expected 'section'.
-   • "lean-manual://a/b": Unknown documentation type 'a'. Expected 'section'.  ⏎
+   • "lean-manual://a/b":
+    Unknown documentation type 'a'. Expected 'section'.
+
 ---
 info: Result: "foo [](lean-manual://) [](lean-manual://f) lean-manual://a/b "
 -/
diff --git a/tests/lean/run/fixedParams.lean b/tests/lean/run/fixedParams.lean
index d857e616ae..e16a5d4c6c 100644
--- a/tests/lean/run/fixedParams.lean
+++ b/tests/lean/run/fixedParams.lean
@@ -59,7 +59,9 @@ namespace Ex4
 trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 3:
     In foo c n b m
     m not matched
-[Elab.definition.fixedParams] getFixedParams: • [#1 #3] ❌ [#3 #1] ❌ • [#3 #1] ❌ [#1 #3] ❌
+[Elab.definition.fixedParams] getFixedParams:
+      • [#1 #3] ❌ [#3 #1] ❌
+      • [#3 #1] ❌ [#1 #3] ❌
 -/
 #guard_msgs in
 mutual
@@ -79,7 +81,8 @@ trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
 [Elab.definition.fixedParams] getFixedParams: notFixed 0 2:
     In app as bs
     x✝ =/= bs
-[Elab.definition.fixedParams] getFixedParams: • [#1] ❌ ❌
+[Elab.definition.fixedParams] getFixedParams:
+      • [#1] ❌ ❌
 -/
 #guard_msgs(trace) in
 def app : List α → List α → List α
@@ -90,7 +93,8 @@ def app : List α → List α → List α
 trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
     In app' as bs
     as✝ =/= as
-[Elab.definition.fixedParams] getFixedParams: • [#1] ❌ [#3]
+[Elab.definition.fixedParams] getFixedParams:
+      • [#1] ❌ [#3]
 -/
 #guard_msgs(trace) in
 def app' (as : List α) (bs : List α) : List α :=
diff --git a/tests/lean/run/formatHardLineBreaks.lean b/tests/lean/run/formatHardLineBreaks.lean
new file mode 100644
index 0000000000..3508801770
--- /dev/null
+++ b/tests/lean/run/formatHardLineBreaks.lean
@@ -0,0 +1,105 @@
+import Lean.Data.Format
+import Lean.Meta.Basic
+
+/-! # Hard line breaks in `Format` text
+
+Hard line breaks in `Format`s should not induce inescapable flattening groups, which they did in
+previous versions of Lean.
+-/
+
+open Lean Meta
+
+/--
+info: A
+B
+C
+-/
+#guard_msgs (whitespace := exact) in
+#eval
+  let f : Format := .text "A\nB" ++ .line ++ "C"
+  IO.println f.pretty
+
+/--
+info: A
+  B
+C
+-/
+#guard_msgs (whitespace := exact) in
+run_meta do
+  logInfo <| m!"A{indentD "B"}" ++ Format.line ++ "C"
+
+/--
+info: A
+B
+  C
+D
+-/
+#guard_msgs (whitespace := exact) in
+run_meta do
+  let text := toMessageData
+  let line := toMessageData Format.line
+  logInfo <| text m!"A" ++ line ++ .nest 2 (m!"B" ++ line ++ m!"C") ++ line ++ "D"
+
+/--
+info: a
+b
+a b
+-/
+#guard_msgs (whitespace := exact) in
+run_meta do logInfo (m!"a" ++ Format.line ++ m!"b" ++ Format.line ++ .group m!"a\nb")
+
+/--
+info: Indented expression:
+  Nat
+Bulleted list:
+  • A
+  • B
+---
+info: Indented expression:
+  Nat
+Bulleted list:
+  • A
+  • B
+---
+info: Bulleted list:
+  • A
+  • B
+Indented expression:
+  Nat
+---
+info: Bulleted list:
+  • A
+  • B
+Indented expression:
+  Nat
+-/
+#guard_msgs (whitespace := exact) in
+run_meta do
+  let e := m!"Indented expression:{indentExpr (.const `Nat [])}"
+  let l := m!"Bulleted list:{indentD m!"• A\n• B"}"
+  logInfo (e ++ .ofFormat (.text "\n") ++ l)
+  logInfo (e ++ Format.line ++ l)
+  logInfo (l ++ .ofFormat (.text "\n") ++ e)
+  logInfo (l ++ Format.line ++ e)
+
+-- *Within* flattening groups, flattening should be recomputed after a hard line break:
+/--
+info: A
+A long line
+B
+C
+D
+
+A
+A long line
+B C
+D
+-/
+#guard_msgs (whitespace := exact) in
+#eval
+  let f : Format := .text "A" ++ .line ++ .group ("A long line" ++ .line ++ .text "B" ++ .line ++ "C") ++ .line ++ "D"
+  let f' : Format := .text "A" ++ .line ++ .group ("A long line\nB" ++ .line ++ "C") ++ .line ++ "D"
+  do
+  IO.println (f.pretty 10)
+  IO.println ""
+  IO.println (f'.pretty 10)
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index 0e97608e90..50b8b7b049 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -208,7 +208,11 @@ h_2 : ¬f a = g b
     [eqc] {a, b}
     [eqc] {f, g}
 [grind] Issues
-  [issue] found congruence between g b and f a but functions have different types
+  [issue] found congruence between
+        g b
+      and
+        f a
+      but functions have different types
 -/
 #guard_msgs (error) in
 example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by
diff --git a/tests/lean/run/info_trees.lean b/tests/lean/run/info_trees.lean
index 47710d5aa4..0429c1c26a 100644
--- a/tests/lean/run/info_trees.lean
+++ b/tests/lean/run/info_trees.lean
@@ -3,58 +3,58 @@
 -- it is fine to simply remove the `#guard_msgs` and expected output.
 
 /--
-info: • command @ ⟨82, 0⟩-⟨82, 40⟩ @ Lean.Elab.Command.elabDeclaration
-  • Nat : Type @ ⟨82, 15⟩-⟨82, 18⟩ @ Lean.Elab.Term.elabIdent
-    • [.] Nat : some Sort.{?_uniq.1} @ ⟨82, 15⟩-⟨82, 18⟩
-    • Nat : Type @ ⟨82, 15⟩-⟨82, 18⟩
-  • n (isBinder := true) : Nat @ ⟨82, 11⟩-⟨82, 12⟩
-  • 0 ≤ n : Prop @ ⟨82, 22⟩-⟨82, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
+info: • command @ ⟨83, 0⟩-⟨83, 40⟩ @ Lean.Elab.Command.elabDeclaration
+  • Nat : Type @ ⟨83, 15⟩-⟨83, 18⟩ @ Lean.Elab.Term.elabIdent
+    • [.] Nat : some Sort.{?_uniq.1} @ ⟨83, 15⟩-⟨83, 18⟩
+    • Nat : Type @ ⟨83, 15⟩-⟨83, 18⟩
+  • n (isBinder := true) : Nat @ ⟨83, 11⟩-⟨83, 12⟩
+  • 0 ≤ n : Prop @ ⟨83, 22⟩-⟨83, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2»
     • Macro expansion
       0 ≤ n
       ===>
       binrel% LE.le✝ 0 n
-      • 0 ≤ n : Prop @ ⟨82, 22⟩†-⟨82, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
-        • 0 ≤ n : Prop @ ⟨82, 22⟩†-⟨82, 27⟩†
-          • [.] LE.le✝ : none @ ⟨82, 22⟩†-⟨82, 27⟩†
-          • 0 : Nat @ ⟨82, 22⟩-⟨82, 23⟩ @ Lean.Elab.Term.elabNumLit
-          • n : Nat @ ⟨82, 26⟩-⟨82, 27⟩ @ Lean.Elab.Term.elabIdent
-            • [.] n : none @ ⟨82, 26⟩-⟨82, 27⟩
-            • n : Nat @ ⟨82, 26⟩-⟨82, 27⟩
+      • 0 ≤ n : Prop @ ⟨83, 22⟩†-⟨83, 27⟩† @ Lean.Elab.Term.Op.elabBinRel
+        • 0 ≤ n : Prop @ ⟨83, 22⟩†-⟨83, 27⟩†
+          • [.] LE.le✝ : none @ ⟨83, 22⟩†-⟨83, 27⟩†
+          • 0 : Nat @ ⟨83, 22⟩-⟨83, 23⟩ @ Lean.Elab.Term.elabNumLit
+          • n : Nat @ ⟨83, 26⟩-⟨83, 27⟩ @ Lean.Elab.Term.elabIdent
+            • [.] n : none @ ⟨83, 26⟩-⟨83, 27⟩
+            • n : Nat @ ⟨83, 26⟩-⟨83, 27⟩
   • CustomInfo(Lean.Elab.Term.AsyncBodyInfo)
-    • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨82, 8⟩-⟨82, 9⟩
-    • n (isBinder := true) : Nat @ ⟨82, 11⟩-⟨82, 12⟩
+    • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨83, 8⟩-⟨83, 9⟩
+    • n (isBinder := true) : Nat @ ⟨83, 11⟩-⟨83, 12⟩
     • CustomInfo(Lean.Elab.Term.BodyInfo)
-      • Tactic @ ⟨82, 31⟩-⟨82, 40⟩
+      • Tactic @ ⟨83, 31⟩-⟨83, 40⟩
         (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])))
         before ⏎
         n : Nat
         ⊢ 0 ≤ n
         after no goals
-        • Tactic @ ⟨82, 31⟩-⟨82, 33⟩
+        • Tactic @ ⟨83, 31⟩-⟨83, 33⟩
           "by"
           before ⏎
           n : Nat
           ⊢ 0 ≤ n
           after no goals
-          • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
+          • Tactic @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq
             (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]))
             before ⏎
             n : Nat
             ⊢ 0 ≤ n
             after no goals
-            • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
+            • Tactic @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented
               (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])
               before ⏎
               n : Nat
               ⊢ 0 ≤ n
               after no goals
-              • Tactic @ ⟨82, 34⟩-⟨82, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
+              • Tactic @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.LibrarySearch.evalExact
                 (Tactic.exact? "exact?" [])
                 before ⏎
                 n : Nat
                 ⊢ 0 ≤ n
                 after no goals
-                • Tactic @ ⟨82, 34⟩†-⟨82, 40⟩† @ Lean.Elab.Tactic.evalExact
+                • Tactic @ ⟨83, 34⟩†-⟨83, 40⟩† @ Lean.Elab.Tactic.evalExact
                   (Tactic.exact "exact" (Term.app `Nat.zero_le [`n]))
                   before ⏎
                   n : Nat
@@ -71,9 +71,10 @@ info: • command @ ⟨82, 0⟩-⟨82, 40⟩ @ Lean.Elab.Command.elabDeclaration
                   {"suggestions": [{"suggestion": "exact Nat.zero_le n"}],
                    "style": null,
                    "range":
-                   {"start": {"line": 81, "character": 34}, "end": {"line": 81, "character": 40}},
+                   {"start": {"line": 82, "character": 34}, "end": {"line": 82, "character": 40}},
                    "isInline": true,
-                   "header": "Try this: "} • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨82, 8⟩-⟨82, 9⟩
+                   "header": "Try this: "}
+    • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨83, 8⟩-⟨83, 9⟩
 ---
 info: Try this: exact Nat.zero_le n
 -/
diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean
index 421eebd47a..77d8d9a3ef 100644
--- a/tests/lean/run/trace.lean
+++ b/tests/lean/run/trace.lean
@@ -73,7 +73,8 @@ info: [module] message
   [module] hello
                world
   [bughunt] at test2
-  [module] hello world
+  [module] hello
+               world
 [module] hello
              world
 [bughunt] at end of tst3
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
index d8552c4d0d..8070fab5c7 100644
--- a/tests/lean/simp_trace.lean.expected.out
+++ b/tests/lean/simp_trace.lean.expected.out
@@ -1,10 +1,16 @@
 Try this: simp only [f, reduceCtorEq]
 [Meta.Tactic.simp.rewrite] unfold f, f (a :: b = []) ==> a :: b = []
-[Meta.Tactic.simp.rewrite] eq_self:1000: False = False ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      False = False
+    ==>
+      True
 Try this: simp only [length, gt_iff_lt]
 [Meta.Tactic.simp.rewrite] unfold length, length (a :: b :: as) ==> length (b :: as) + 1
 [Meta.Tactic.simp.rewrite] unfold length, length (b :: as) ==> length as + 1
-[Meta.Tactic.simp.rewrite] gt_iff_lt:1000: length as + 1 + 1 > length as ==> length as < length as + 1 + 1
+[Meta.Tactic.simp.rewrite] gt_iff_lt:1000:
+      length as + 1 + 1 > length as
+    ==>
+      length as < length as + 1 + 1
 Try this: simp only [fact, gt_iff_lt, Nat.zero_lt_succ, Nat.mul_pos_iff_of_pos_left]
 [Meta.Tactic.simp.rewrite] unfold fact, fact (x + 1) ==> (x + 1) * fact x
 [Meta.Tactic.simp.rewrite] gt_iff_lt:1000:
@@ -15,15 +21,24 @@ Try this: simp only [fact, gt_iff_lt, Nat.zero_lt_succ, Nat.mul_pos_iff_of_pos_l
       0 < x + 1
     ==>
       True
-[Meta.Tactic.simp.rewrite] Nat.mul_pos_iff_of_pos_left:1000: 0 < (x + 1) * fact x ==> 0 < fact x
+[Meta.Tactic.simp.rewrite] Nat.mul_pos_iff_of_pos_left:1000:
+      0 < (x + 1) * fact x
+    ==>
+      0 < fact x
 Try this: simp only [head]
 [Meta.Tactic.simp.rewrite] unfold head, head (a :: as) ==> match a :: as with
     | [] => default
     | a :: tail => a
-[Meta.Tactic.simp.rewrite] eq_self:1000: a = a ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      a = a
+    ==>
+      True
 Try this: simp only [foo]
 [Meta.Tactic.simp.rewrite] unfold foo, foo ==> 10
-[Meta.Tactic.simp.rewrite] eq_self:1000: 10 + x = 10 + x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      10 + x = 10 + x
+    ==>
+      True
 Try this: simp only [g, pure]
 [Meta.Tactic.simp.rewrite] unfold g, g x ==> (let x := x;
       pure x).run
@@ -43,13 +58,19 @@ Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modify
 [Meta.Tactic.simp.rewrite] unfold getThe, getThe Nat s ==> MonadStateOf.get s
 [Meta.Tactic.simp.rewrite] unfold StateT.get, StateT.get s ==> pure (s, s)
 [Meta.Tactic.simp.rewrite] unfold StateT.set, StateT.set (g s) s ==> pure (PUnit.unit, g s)
-[Meta.Tactic.simp.rewrite] eq_self:1000: (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s) ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s)
+    ==>
+      True
 Try this: simp only [bla, h]
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] eq_self:1000: x + x = x + x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      x + x = x + x
+    ==>
+      True
 Try this: simp only [h, Nat.sub_add_cancel]
 [Meta.Tactic.simp.rewrite] h:1000:
       1 ≤ x
@@ -59,7 +80,10 @@ Try this: simp only [h, Nat.sub_add_cancel]
       x - 1 + 1
     ==>
       x
-[Meta.Tactic.simp.rewrite] eq_self:1000: x + 2 = x + 2 ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      x + 2 = x + 2
+    ==>
+      True
 Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel, dite_eq_ite]
 [Meta.Tactic.simp.rewrite] h:1000:
       1 ≤ x
@@ -77,25 +101,37 @@ Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel, dite
       if _h : 1 ≤ x then x else 0
     ==>
       if 1 ≤ x then x else 0
-[Meta.Tactic.simp.rewrite] eq_self:1000: (if 1 ≤ x then x else 0) = if 1 ≤ x then x else 0 ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      (if 1 ≤ x then x else 0) = if 1 ≤ x then x else 0
+    ==>
+      True
 Try this: simp only [and_self]
 [Meta.Tactic.simp.rewrite] and_self:1000:
       b ∧ b
     ==>
       b
-[Meta.Tactic.simp.rewrite] iff_self:1000: a ∧ b ↔ a ∧ b ==> True
+[Meta.Tactic.simp.rewrite] iff_self:1000:
+      a ∧ b ↔ a ∧ b
+    ==>
+      True
 Try this: simp only [my_thm]
 [Meta.Tactic.simp.rewrite] my_thm:1000:
       b ∧ b
     ==>
       b
-[Meta.Tactic.simp.rewrite] eq_self:1000: (a ∧ b) = (a ∧ b) ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      (a ∧ b) = (a ∧ b)
+    ==>
+      True
 Try this: simp (discharger := sorry) only [Nat.sub_add_cancel]
 [Meta.Tactic.simp.rewrite] Nat.sub_add_cancel:1000:
       x - 1 + 1
     ==>
       x
-[Meta.Tactic.simp.rewrite] eq_self:1000: x = x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000:
+      x = x
+    ==>
+      True
 simp_trace.lean:86:0-86:7: warning: declaration uses 'sorry'
 Try this: simp only [bla, h] at *
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
@@ -119,7 +155,10 @@ h₂ : xs.length + ys.length = y
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] List.length_append:1000: (xs ++ ys).length ==> xs.length + ys.length
+[Meta.Tactic.simp.rewrite] List.length_append:1000:
+      (xs ++ ys).length
+    ==>
+      xs.length + ys.length
 Try this: simp only [bla, h, List.length_append] at *
 simp_trace.lean:107:101-108:53: error: unsolved goals
 x y : Nat
@@ -132,7 +171,10 @@ h₂ : xs.length + ys.length = y
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] List.length_append:1000: (xs ++ ys).length ==> xs.length + ys.length
+[Meta.Tactic.simp.rewrite] List.length_append:1000:
+      (xs ++ ys).length
+    ==>
+      xs.length + ys.length
 Try this: simp only [bla, h] at *
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
@@ -162,7 +204,10 @@ Try this: simp only [← my_thm']
       P ∧ P
     ==>
       P
-[Meta.Tactic.simp.rewrite] iff_self:1000: P ↔ P ==> True
+[Meta.Tactic.simp.rewrite] iff_self:1000:
+      P ↔ P
+    ==>
+      True
 Try this: simp only [h]
 [Meta.Tactic.simp.rewrite] h:1000:
       P
@@ -183,4 +228,7 @@ Try this: simp_all only
       n
     ==>
       m
-[Meta.Tactic.simp.rewrite] h₁:1000: n ==> m
+[Meta.Tactic.simp.rewrite] h₁:1000:
+      n
+    ==>
+      m
diff --git a/tests/lean/test_extern.lean.expected.out b/tests/lean/test_extern.lean.expected.out
index 25c3a995a9..64482b2ddf 100644
--- a/tests/lean/test_extern.lean.expected.out
+++ b/tests/lean/test_extern.lean.expected.out
@@ -1,3 +1,6 @@
 test_extern.lean:6:0-6:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute or @[implemented_by] attribute
 test_extern.lean:15:0-15:13: error: native implementation did not agree with reference implementation!
-Compare the outputs of: #eval g  and #eval 4
+Compare the outputs of:
+#eval g
+ and
+#eval 4