[Merged by Bors] - fix(Tactic/ToFun): correct location of hovers#39911

grunweg wants to merge 2 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

grunweg:tofun-fixhoversgrunweg/mathlib4:tofun-fixhoversCopy head branch name to clipboard