refactor: WF.Fix: Pass all remaining goals to Term.reportUnsolvedGoals (#2922)

This only really shows up when the `decreasing_tactic` fails with
multiple goals, as in
```
macro_rules
  | `(tactic|decreasing_tactic) => `(tactic| by_cases (2 > 1))
def foo (n : Nat) : Nat := foo (n - 1)
termination_by foo n => n
```
where we now get
```
unsolved goals
case inl
n: Nat
h✝: 2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n


case inr
n: Nat
h✝: ¬2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
```
rather than
```
LeanProject.lean:3:27

unsolved goals
case inl
n: Nat
h✝: 2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n

LeanProject.lean:3:27

unsolved goals
case inr
n: Nat
h✝: ¬2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
```

The effect is neglectible, but the code is a bit nicer, so why not,
before someone looks at it again and wonders whether the goals are
reported separately for a reason.

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -20,7 +20,8 @@ open Meta
 private def applyDefaultDecrTactic (mvarId : MVarId) : TermElabM Unit := do
   let remainingGoals ← Tactic.run mvarId do
     Tactic.evalTactic (← `(tactic| decreasing_tactic))
-  remainingGoals.forM fun mvarId => Term.reportUnsolvedGoals [mvarId]
+  unless remainingGoals.isEmpty do
+    Term.reportUnsolvedGoals remainingGoals
 
 private def mkDecreasingProof (decreasingProp : Expr) (decrTactic? : Option Syntax) : TermElabM Expr := do
   let mvar ← mkFreshExprSyntheticOpaqueMVar decreasingProp