fix(Tactic/ToFun): correct location of hovers

When an explicit name for the new declaration is given, ensure to 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

@@ -49,11 +49,13 @@ def toFunImpl (src : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Name :=
   let name := match id with
     | some name => (src.splitAt name.getId.getNumParts).1 ++ name.getId
     | none => src.appendBefore "fun_"
+  let mut loc := tk
   if let some id := id then
+    loc := id
     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 loc optAttr
     (docstringPrefix? := s!"Eta-expanded form of `{src}`") (hoverInfo := true)
     fun value levels => do
     let type ← inferType value