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

Mathlib/Tactic/ToFun.lean

@@ -47,9 +47,12 @@ def toFunImpl (src : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Name :=
   if (kind != AttributeKind.global) then
     throwError "`to_fun` can only be used as a global attribute"
   let name := match id with
-    | some name =>
-      (src.splitAt name.getId.getNumParts).1 ++ name.getId
+    | some name => (src.splitAt name.getId.getNumParts).1 ++ name.getId
     | none => src.appendBefore "fun_"
+  if let some id := id then
+    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
     (docstringPrefix? := s!"Eta-expanded form of `{src}`") (hoverInfo := true)
     fun value levels => do

MathlibTest/ToFun.lean

@@ -3,10 +3,17 @@ import Mathlib.Analysis.Normed.Ring.Basic
 
 set_option pp.unicode.fun true
 
-variable {R : Type*}
+/--
+warning: `to_fun` correctly autogenerated the provided name `fun_id_eq'`.
+You may remove it.
+-/
+#guard_msgs in
+@[to_fun fun_id_eq']
+lemma id_eq' {R : Type*} : (@id R) = id := id_eq _
 
 @[to_fun baz]
 lemma Foo.bar (f g : ℝ → ℝ) : f * g = g * f := mul_comm f g
+
 /-- info: Foo.baz (f g : ℝ → ℝ) : (fun i ↦ f i * g i) = fun i ↦ g i * f i -/
 #guard_msgs in #check Foo.baz
 
@@ -52,6 +59,14 @@ theorem Function.mul_comm (f g : ℝ → ℝ) : f * g = g * f := _root_.mul_comm
 #guard_msgs in
 #check Function.fun_mul_comm
 
+/--
+warning: `to_fun` correctly autogenerated the provided name `fun_bar`.
+You may remove it.
+-/
+#guard_msgs in
+@[to_fun fun_bar]
+theorem bar (f g : ℝ → ℝ) : f * g = g * f := _root_.mul_comm f g
+
 /-- Look I am the doc-string of `foo`. -/
 @[to_fun]
 theorem foo : (1 : Nat → Nat) = 1 := rfl