From 44366382d3fdafb4e4f3de86d746624f0590c4a8 Mon Sep 17 00:00:00 2001
From: Jannis Limperg <jannis@limperg.de>
Date: Tue, 27 Aug 2024 16:45:16 +0200
Subject: [PATCH] fix: ignore implementationDetail hyps in rename_i (#5183)

Closes #5176
---
 src/Lean/Elab/Tactic/BuiltinTactic.lean |  2 ++
 tests/lean/run/5176.lean                | 14 ++++++++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 tests/lean/run/5176.lean

diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index fe3640210048..28fc2ee15638 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -458,6 +458,8 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta
       match lctx.getAt? j with
       | none => pure ()
       | some localDecl =>
+        if localDecl.isImplementationDetail then
+          continue
         let inaccessible := !(extractMacroScopes localDecl.userName |>.equalScope callerScopes)
         let shadowed := found.contains localDecl.userName
         if inaccessible || shadowed then
diff --git a/tests/lean/run/5176.lean b/tests/lean/run/5176.lean
new file mode 100644
index 000000000000..231e6db4f951
--- /dev/null
+++ b/tests/lean/run/5176.lean
@@ -0,0 +1,14 @@
+class Foo where
+
+class Bar extends Foo where
+  bar : True
+
+def foo : Foo := {}
+
+example [Bar] : Bar := {
+  foo with bar := by {
+    rename_i inst
+    guard_hyp inst : Bar
+    trivial
+  }
+}