`lambdaMetaTelescope` doesn't preserve binder names

[JovanGerb]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

lambdaMetaTelescope creates metavariables with anonymous user names instead of using the binder names from the lambda binders.

Context

This caused to_dual in mathlib to generate some definitions where the lambda binder names were wrong. That problem has now been fixed (leanprover-community/mathlib4#40946)

Steps to Reproduce

import Lean

open Lean Meta

/-- info: fun {x} => x -/
#guard_msgs in
run_meta
  let e := Expr.lam `a (.sort 0) (.bvar 0) .default
  let (mvars, _, e) ← lambdaMetaTelescope e
  let e ← mkLambdaFVars mvars e
  logInfo m!"{e}"

Expected behavior: The resulting bound variable is called a

Actual behavior: The resulting bound variable is called x

Versions

4.32.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.