when do simp lemmas have to be added explicitly?

Stream: general

[Bryan Gin-ge Chen]

In #6530, there are some simps that don't close the goal unless docs#pi.smul_apply is added to the list of lemmas. However, pi.smul_apply is already tagged with @[simp]. I haven't seen this before - is this expected?

[Eric Rodriguez]

I have no idea why this is (just a novice), but the correct GH number is #6350.

[Bryan Gin-ge Chen]

Thanks, corrected!