fix: have Lean.Meta.ppGoal use hard newlines (#5640)

This function uses soft newlines in many places where hard newlines are
more appropriate. Pointed out by @gebner in #1967.

src/Lean/Meta/PPGoal.lean

@@ -33,7 +33,7 @@ register_builtin_option pp.showLetValues : Bool := {
 }
 
 private def addLine (fmt : Format) : Format :=
-  if fmt.isNil then fmt else fmt ++ Format.line
+  if fmt.isNil then fmt else fmt ++ "\n"
 
 def getGoalPrefix (mvarDecl : MetavarDecl) : String :=
   if isLHSGoal? mvarDecl.type |>.isSome then
@@ -99,6 +99,6 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
       let fmt := fmt ++ getGoalPrefix mvarDecl ++ Format.nest indent typeFmt
       match mvarDecl.userName with
       | Name.anonymous => return fmt
-      | name           => return "case " ++ format name.eraseMacroScopes ++ Format.line ++ fmt
+      | name           => return "case " ++ format name.eraseMacroScopes ++ "\n" ++ fmt
 
 end Lean.Meta

tests/lean/issue2981.lean.expected.out

@@ -8,4 +8,5 @@ Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
 n : Nat
 ⊢ n < n.succ
-n m : Nat ⊢ n < n.succ
+n m : Nat
+⊢ n < n.succ

tests/lean/simpDisch.lean.expected.out

@@ -8,7 +8,12 @@ h1 : x ≠ 0
 h2 : y ≠ 0
 h3 : x = y
 ⊢ x ≠ 0
-case simp.discharger x y : Nat h1 : x ≠ 0 h2 : y ≠ 0 h3 : x = y ⊢ y ≠ 0
+case simp.discharger
+x y : Nat
+h1 : x ≠ 0
+h2 : y ≠ 0
+h3 : x = y
+⊢ y ≠ 0
 x y : Nat
 h1 : x ≠ 0
 h2 : y ≠ 0