fix(Tactic/ToFun): correct location of hovers (leanprover-community#39911)

When an explicit name for the new declaration is given, make hovering over the `to_fun` keyword show the keyword's documentation, and hovering over the new declaration show the declaration's name.
Right now, it is the opposite way around.

Author: grunweg

Mathlib/Tactic/ToFun.lean

@@ -53,7 +53,7 @@ def toFunImpl (src : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Name :=
     if name == src.appendBefore "fun_" then
       logWarningAt id m!"`to_fun` correctly autogenerated the provided name `{.ofConstName name}`.\
         \nYou may remove it."
-  MetaM.run' <| addRelatedDecl src name tk optAttr
+  MetaM.run' <| addRelatedDecl src name (id.elim tk (·.raw)) optAttr
     (docstringPrefix? := s!"Eta-expanded form of `{src}`") (hoverInfo := true)
     fun value levels => do
     let type ← inferType value