fix: counterexample generation for new match encoding

src/Lean/Meta/Match/Match.lean

@@ -838,7 +838,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := do
     withAlts motive discrs discrInfos lhss fun alts minors => do
       let mvar ← mkFreshExprMVar mvarType
       trace[Meta.Match.debug] "goal\n{mvar.mvarId!}"
-      let examples := discrs.toList.map fun discr => Example.var discr.fvarId!
+      let examples := discrs'.toList.map fun discr => Example.var discr.fvarId!
       let (_, s) ← (process { mvarId := mvar.mvarId!, vars := discrs'.toList, alts := alts, examples := examples }).run {}
       let val ← mkLambdaFVars discrs' mvar
       trace[Meta.Match.debug] "matcher\nvalue: {val}\ntype: {← inferType val}"

tests/lean/matchMissingCasesAsStuckError.lean.expected.out

@@ -1,2 +1,2 @@
 matchMissingCasesAsStuckError.lean:2:2-2:7: error: missing cases:
-none, _
+none

tests/lean/matchUnknownFVarBug.lean.expected.out

@@ -1,9 +1,10 @@
 matchUnknownFVarBug.lean:2:2-2:7: error: missing cases:
-(some (Nat.succ _)), Eq.refl, (some _), Eq.refl
-none, Eq.refl, none, Eq.refl
+(some (Nat.succ _)), (some _)
+(some (Nat.succ _)), none
+none, (some _)
+none, none
 matchUnknownFVarBug.lean:3:18-3:19: error: unsolved goals
-n? : Option Nat
+n? x✝ : Option Nat
 h : n? = some 0
-x✝ : Option Nat
-h' : some 0 = x✝
+h' : n? = x✝
 ⊢ False

tests/lean/rwEqThms.lean.expected.out

@@ -2,7 +2,7 @@
 a : α
 as bs : List α
 h : bs = a :: as
-⊢ List.length (?a_1 :: as) = List.length bs
+⊢ List.length (?a :: as) = List.length bs
 
 case a
 α : Type ?u