From f10101cd583b0798e2f61a340e3d742c82ce87ec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Oct 2021 18:45:48 -0700
Subject: [PATCH] fix: preserve user variable names in decreasing goals

---
 src/Lean/Elab/PreDefinition/WF/PackMutual.lean | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean
index 5cba177731..d2cc4577fe 100644
--- a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean
+++ b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean
@@ -64,10 +64,21 @@ private partial def mkNewCoDomain (x : Expr) (preDefs : Array PreDefinition) : M
   This step is performed by `transform` with the following `post` method.
  -/
 private partial def packValues (x : Expr) (codomain : Expr) (preDefs : Array PreDefinition) : MetaM Expr := do
+  let varNames := preDefs.map fun preDef =>
+    assert! preDef.value.isLambda
+    preDef.value.bindingName!
   let mvar ← mkFreshExprSyntheticOpaqueMVar codomain
   let rec go (mvarId : MVarId) (x : FVarId) (i : Nat) : MetaM Unit := do
     if i < preDefs.size - 1 then
-      let #[s₁, s₂] ← cases mvarId x | unreachable!
+      /-
+        Names for the `cases` tactics. The names are important to preserve the user provided names (unary functions).
+      -/
+      let givenNames : Array AltVarNames :=
+         if i == preDefs.size - 2 then
+           #[{ varNames := [varNames[i]] }, { varNames := [varNames[i+1]] }]
+         else
+           #[{ varNames := [varNames[i]] }]
+       let #[s₁, s₂] ← cases mvarId x (givenNames := givenNames) | unreachable!
       assignExprMVar s₁.mvarId (mkApp preDefs[i].value s₁.fields[0]).headBeta
       go s₂.mvarId s₂.fields[0].fvarId! (i+1)
     else