Bad `simp` lemmas for `AddConstMap`

Stream: mathlib4

[Yury G. Kudryashov]

About @Matthew Ballard 's #14233 (adding scoped to a bunch of simp lemmas). First of all, thank you for locating and fixing this! Second, could you please explain to me why these lemmas are bad, so that I don't introduce a similar performance issue in the future? Is it because Lean tries them every time when it sees DFunLike.coe f (_ + _) but they rarely apply (as opposed to _root_.map_add which usually applies when it matches)?

[Yury G. Kudryashov]

If yes, does it mean that lemmas like docs#AddConstMap.coe_mk and below are OK as non-scoped but you've scoped them for consistency?

[Matthew Ballard]

Yury G. Kudryashov said:

Is it because Lean tries them every time when it sees DFunLike.coe f (_ + _) but they rarely apply (as opposed to _root_.map_add which usually applies when it matches)?

Yes, my understanding is that they get through the discrimination tree filter now but rarely apply. Since this is a leaf file, we don't notice. But in linting, we have all of mathlib to check simp on.

[Matthew Ballard]

I just scoped everything mindlessly. But I think consistency is a good goal. You don't want to guess which are and which are out.

[Yury G. Kudryashov]

I guess, lemmas in AddConstMapClass should be scoped, lemmas about AddConstMaps don't need scoped.

[Yury G. Kudryashov]

Testing in #9726

[Yury G. Kudryashov]

I droped scoped on lemmas about concrete types. Bench says no significant changes. Would you like have a look from the perf point of view?

[Matthew Ballard]

Looks good to me.