fix(Translate): preserve binder names when reordering lambdas (leanprover-community#40946)

To my surprise, `lambdaMetaTelescope` does not use the lambda binder names to give names to the introduced metavariables. As a result, `reorderLambda` would rename all lambda binder names to `x`. This is fixed by only using `forallMetaTelescope` to introduce the metavariables.

Author: JovanGerb

Mathlib/Tactic/Translate/Reorder.lean

@@ -213,15 +213,13 @@ partial def reorderForall (reorder : ArgReorder) (e : Expr) : MetaM Expr := do
 
 /-- Reorder the arguments of a function using the given `ArgReorder`. -/
 partial def reorderLambda (reorder : ArgReorder) (e : Expr) : MetaM Expr := do
-  let (mvars, bis, e) ← lambdaMetaTelescope e reorder.range
-  let (mvars', bis', _) ← forallMetaBoundedTelescope (← inferType e) (reorder.range - mvars.size)
-  let mut mvars := mvars ++ mvars'
+  let (mvars, bis, _) ← forallMetaBoundedTelescope (← inferType e) reorder.range
   unless mvars.size = reorder.range do
     throwError "the permutation (reorder := {reorder}) is out of bounds, \
       the function{indentExpr e}\nhas only {mvars.size} arguments"
-  let bis := reorder.permute! (bis ++ bis') |>.toList
+  let bis := reorder.permute! bis |>.toList
   -- Note that `mkLambdaFVars` also works with mvars.
-  fixBinderInfos bis <$> mkLambdaFVars (← reorderMVars mvars reorder) (mkAppN e mvars')
+  fixBinderInfos bis <$> mkLambdaFVars (← reorderMVars mvars reorder) (e.beta mvars)
 
 end
 

MathlibTest/Attribute/ToDual.lean

@@ -55,16 +55,17 @@ def SemilatticeSup.casesOn' {α} {motive : SemilatticeSup α → Sort*} (t : Sem
   t.casesOn mk
 
 /--
-info: SemilatticeInf.casesOn'.{u_1} {α : Type} {motive : SemilatticeInf α → Sort u_1}
-  (mk :
-    [inst : Min α] →
-      [inst_1 : PartialOrder α] →
-        (sup_le : ∀ (b a c : α), c ≤ a → c ≤ b → c ≤ a ⊓ b) →
-          motive { toPartialOrder := inst_1, toMin := inst, le_inf := ⋯ })
-  (t : SemilatticeInf α) : motive t
+info: @[expose] def SemilatticeInf.casesOn'.{u_1} : {α : Type} →
+  {motive : SemilatticeInf α → Sort u_1} →
+    ([inst : Min α] →
+        [inst_1 : PartialOrder α] →
+          (sup_le : ∀ (b a c : α), c ≤ a → c ≤ b → c ≤ a ⊓ b) →
+            motive { toPartialOrder := inst_1, toMin := inst, le_inf := ⋯ }) →
+      (t : SemilatticeInf α) → motive t :=
+fun {α} {motive} mk t => SemilatticeInf.casesOn t fun [PartialOrder α] [Min α] sup_le => mk ⋯
 -/
 #guard_msgs in
-#check SemilatticeInf.casesOn'
+#print SemilatticeInf.casesOn'
 
 class Semilattice (α : Type) extends SemilatticeInf α, SemilatticeSup α
 attribute [to_dual existing] Semilattice.toSemilatticeSup