diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index a599dfc05b..440067e8c0 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -342,7 +342,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
       let fvarId ← withoutModifyingState <| withNewMCtxDepth <| withoutRecover do
         let type ← elabTerm typeStx none (mayPostpone := true)
         let fvarId? ← (← getLCtx).findDeclRevM? fun localDecl => do
-          if (← isDefEq type localDecl.type) then return localDecl.fvarId else return none
+          if !localDecl.isImplementationDetail && (← isDefEq type localDecl.type) then return localDecl.fvarId else return none
         match fvarId? with
         | none => throwError "failed to find a hypothesis with type{indentExpr type}"
         | some fvarId => return fvarId
diff --git a/tests/lean/run/renameSelf.lean b/tests/lean/run/renameSelf.lean
new file mode 100644
index 0000000000..47df6110af
--- /dev/null
+++ b/tests/lean/run/renameSelf.lean
@@ -0,0 +1,11 @@
+variable {P Q : Prop}
+
+/--
+error: failed to find a hypothesis with type
+  P ↔ Q
+-/
+#guard_msgs in
+example : P ↔ Q := by
+  rename P ↔ Q => goal
+  obtain ⟨hpq, hqp⟩ := goal
+  constructor <;> trivial