Bless test

Author: grunweg

MathlibTest/ToFun.lean

@@ -3,7 +3,10 @@ import Mathlib.Analysis.Normed.Ring.Basic
 
 set_option pp.unicode.fun true
 
-/-- warning: the autogenerated name `fun_id_eq'` matches the one provided -/
+/--
+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 _
@@ -56,7 +59,10 @@ theorem Function.mul_comm (f g : ℝ → ℝ) : f * g = g * f := _root_.mul_comm
 #guard_msgs in
 #check Function.fun_mul_comm
 
-/-- warning: the autogenerated name `fun_bar` matches the one provided -/
+/--
+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