fix: allow renameI to rename shadowed names

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -220,15 +220,16 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId :
     return mvarId
   else
     let mvarDecl ← getMVarDecl mvarId
-    let mut lctx := mvarDecl.lctx
-    let mut hs   := hs
+    let mut lctx  := mvarDecl.lctx
+    let mut hs    := hs
+    let mut found : NameSet := {}
     let n := lctx.numIndices
     for i in [:n] do
       let j := n - i - 1
       match lctx.getAt? j with
       | none => pure ()
       | some localDecl =>
-        if localDecl.userName.hasMacroScopes then
+        if localDecl.userName.hasMacroScopes || found.contains localDecl.userName then
           let h := hs.back
           if h.isIdent then
             let newName := h.getId
@@ -236,6 +237,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId :
           hs := hs.pop
           if hs.isEmpty then
             break
+        found := found.insert localDecl.userName
     unless hs.isEmpty do
       logError m!"too many variable names provided"
     let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances mvarDecl.type MetavarKind.syntheticOpaque mvarDecl.userName

tests/lean/renameI.lean

@@ -0,0 +1,17 @@
+example : (m n : Nat) → m = n := by
+  intro y y
+  renameI x
+  traceState
+  admit
+
+example : (m n : Nat) → m = n := by
+  intro a.b a.b
+  renameI x
+  traceState
+  admit
+
+example : (m o p n: Nat) → m + p = n + o := by
+  intro a.b _ _ a.b
+  renameI x _ y
+  traceState
+  admit

tests/lean/renameI.lean.expected.out

@@ -0,0 +1,9 @@
+x y : Nat
+⊢ x = y
+renameI.lean:5:2-5:7: warning: declaration uses 'sorry'
+x a.b : Nat
+⊢ x = a.b
+renameI.lean:11:2-11:7: warning: declaration uses 'sorry'
+x o✝ y a.b : Nat
+⊢ x + y = a.b + o✝
+renameI.lean:17:2-17:7: warning: declaration uses 'sorry'