fix: matching inside new termination_by

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

@@ -57,7 +57,7 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) (wf?
       let pendingMVarIds ← getMVars wfRel
       discard <| logUnassignedUsingErrorInfos pendingMVarIds
       return wfRel
-  | some (TerminationWF.ext elements) => withRef (getRefFromElems elements) do
+  | some (TerminationWF.ext elements) => withDeclName unaryPreDef.declName <| withRef (getRefFromElems elements) do
     let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
     let [fMVarId, wfRelMVarId, _] ← apply mainMVarId (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
     let (d, fMVarId) ← intro1 fMVarId

tests/lean/run/955.lean

@@ -0,0 +1,26 @@
+namespace Ex2
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by _ n =>
+  match n with
+  | _ => n
+end Ex2
+
+
+namespace Ex3
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by' measure (fun n => match n with | Sum.inl n => n | Sum.inr n => n)
+end Ex3