[Merged by Bors] - feat(Tactic/ToFun): warn if provided name matches autogenerated one

[grunweg]

This PR advises the user to remove a name they explicitly provided to @[to_fun] if it matches the name @[to_fun] would autogenerate.

---

[github-actions]

PR summary dd364d5681

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ bar
+ id_eq'

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[JovanGerb]

The warning message is different from the one used in to_additive. Wouldn't it be better to use the same phrasing?

[grunweg]

Sure, but which one should be used?

[thorimur]

Thanks! Looks good. :)

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by thorimur.

[thorimur]

(Edited the title and PR description :) )

[adomani]

This is not part of this PR, but what happens if you use _root_.Foo.bar_fun? I suspect that the check will not warn, but you add a declaration whose name that starts with _root_. in the environment!

[adomani]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job

[grunweg]

root.Foo.bar_fun

Indeed, good catch! (And to_additive has the same issue.) Should this be disallowed, or should the _root_ be dropped --- what do you think?

[adomani]

I am not sure: I think that, if it were banned, no current use would get flagged. However, if it gets banned, I am not sure how you could signal the legitimate desire of "place the to_additive declaration in the root namespace"...

[grunweg]

Indeed, I just arrived at the same conclusion (and found another bug in the naming generation).
Should @[to_fun _root_.bar] instead just generate the name bar, i.e. overriding the namespace length heuristic?

[grunweg]

I have made #39962 with that fix