test: exposeNames

src/Init/Tactics.lean

@@ -1602,6 +1602,12 @@ using `show_term`.
 -/
 macro (name := by?) tk:"by?" t:tacticSeq : term => `(show_term%$tk by%$tk $t)
 
+/--
+`expose_names` creates a new goal whose local context has been "exposed" so that every local declaration has a clear,
+accessible name. If no local declarations require renaming, the original goal is returned unchanged.
+-/
+syntax (name := exposeNames) "expose_names" : tactic
+
 end Tactic
 
 namespace Attr

src/Lean/Elab/Tactic.lean

@@ -49,3 +49,4 @@ import Lean.Elab.Tactic.Monotonicity
 import Lean.Elab.Tactic.Try
 import Lean.Elab.Tactic.AsAuxLemma
 import Lean.Elab.Tactic.TreeTacAttr
+import Lean.Elab.Tactic.ExposeNames

src/Lean/Elab/Tactic/ExposeNames.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.ExposeNames
+import Lean.Elab.Tactic.Basic
+
+namespace Lean.Elab.Tactic
+
+@[builtin_tactic Lean.Parser.Tactic.exposeNames] def evalExposeNames : Tactic := fun _ =>
+  liftMetaTactic1 fun mvarId => mvarId.exposeNames
+
+end Lean.Elab.Tactic

src/Lean/Meta/Tactic/ExposeNames.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Util
+
+namespace Lean.Meta
+/--
+Creates a new goal whose local context has been "exposed" so that every local declaration has a clear, accessible name.
+If no local declarations require renaming, the original goal is returned unchanged.
+-/
+def _root_.Lean.MVarId.exposeNames (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  mvarId.checkNotAssigned `expose_names
+  let mut map : Std.HashMap Name FVarId := {}
+  let mut toRename := #[]
+  for localDecl in (← getLCtx) do
+    let userName := localDecl.userName
+    if userName.hasMacroScopes then
+      toRename := toRename.push localDecl.fvarId
+    else
+      if let some fvarId := map[userName]? then
+        -- Variable has been shadowed
+        toRename := toRename.push fvarId
+      map := map.insert userName localDecl.fvarId
+  if toRename.isEmpty then
+    return mvarId
+  let mut next : Std.HashMap Name Nat := {}
+  let mut lctx ← getLCtx
+  -- Remark: Shadowed variables may be inserted later.
+  toRename := toRename.qsort fun fvarId₁ fvarId₂ =>
+    (lctx.get! fvarId₁).index < (lctx.get! fvarId₂).index
+  for fvarId in toRename do
+    let localDecl := lctx.get! fvarId
+    let mut baseName := localDecl.userName
+    if baseName.hasMacroScopes then
+      baseName := baseName.eraseMacroScopes
+      if baseName == `x then
+        if (← isProp localDecl.type) then
+          baseName := `h
+    let mut userName := baseName
+    let mut i := next[baseName]?.getD 0
+    repeat
+      if !map.contains userName then
+        break
+      i := i + 1
+      userName := baseName.appendIndexAfter i
+    next := next.insert baseName i
+    map := map.insert userName fvarId
+    lctx := lctx.modifyLocalDecl fvarId (·.setUserName userName)
+  let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) (← mvarId.getType) .syntheticOpaque (← mvarId.getTag)
+  mvarId.assign mvarNew
+  return mvarNew.mvarId!
+
+end Lean.Meta

tests/lean/run/exposeNames.lean

@@ -0,0 +1,48 @@
+/--
+info: α : Type u_1
+inst : DecidableEq α
+inst_1 : Add α
+a_1 b_1 : α
+h : a_1 = b_1
+a_2 b : α
+h_1 : b = a_2
+a : α
+⊢ a = b
+-/
+#guard_msgs (info) in
+example [DecidableEq α] [Add α] (a b : α) (_ : a = b) (a : α) (b : α) (_ : b = a) (a : α) : a = b := by
+  expose_names
+  trace_state
+  sorry
+
+/--
+info: α : Sort u_1
+a b : α
+h_1 : a = b
+h_2 : True
+h_3 : True ∨ False
+h : b = a
+⊢ b = a
+-/
+#guard_msgs (info) in
+example (a b : α) (h : a = b) (_ : True) (_ : True ∨ False) (h : b = a) : b = a := by
+  expose_names
+  trace_state
+  rw [h]
+
+/--
+info: α : Sort u_1
+a b : α
+h : a = b
+h_3 : True
+h_4 : False
+h_1 : True ∨ False
+h_5 : True
+h_2 : b = a
+⊢ b = a
+-/
+#guard_msgs (info) in
+example (a b : α) (h : a = b) (_ : True) (_ : False) (h_1 : True ∨ False) (_ : True) (h_2 : b = a) : b = a := by
+  expose_names
+  trace_state
+  contradiction