fix: decreasing_by: preserve variable names of match alts (#10980)

This PR tries to preserve names of pattern variables in match
alternatives in `decreasing_by`, by telescoping into the concrete
alternative rather than the type of the matcher's alt. Fixes #10976.

Author: nomeata

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -22,8 +22,10 @@ private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNu
     let typeNew ← whnfD typeNew
     match typeNew with
     | Expr.forallE _ d b _ =>
-      let (alt, refined) ← forallBoundedTelescope d (some numParams) fun xs d => do
-        let alt ← try instantiateLambda alt xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
+      let (alt, refined) ← lambdaBoundedTelescope alt numParams fun xs alt => do
+        unless xs.size == numParams do
+          throwError "unexpected matcher application, alternative must have {numParams} parameters"
+        let d ← try instantiateForall d xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
         forallBoundedTelescope d (some 1) fun x _ => do
           let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative
           let refined ← if refined then

tests/lean/guessLexFailures.lean.expected.out

@@ -155,5 +155,5 @@ guessLexFailures.lean:131:14-131:31: error: failed to prove termination, possibl
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
-m n✝ n : Nat
-⊢ n < n✝ + 1
+n✝ m n : Nat
+⊢ n < n✝

tests/lean/run/issue10976.lean

@@ -0,0 +1,16 @@
+-- The variable names should be `a1` and `b1`
+
+/--
+error: Failed: `fail` tactic was invoked
+a1 b1 : Nat
+⊢ a1 + b1 < a1.succ + b1.succ
+-/
+#guard_msgs in
+def f (a b : Nat) := match a with
+| 0 => 0
+| a1+1 => match b with
+  | 0 => 0
+  | b1+1 => f a1 b1
+termination_by a+b
+decreasing_by
+  fail