fix: have rename ignore implementation detail hypotheses (#8241)

This PR changes the behavior of the `rename` tactic to skip over
implementation detail hypotheses when finding a hypothesis to rename.

Closes #8240.

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

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