`simpNF` should use dsimp for lemmas proved by `rfl`

[digama0]

The @[simp] attribute is used by both simp and dsimp, so it is possible for a rfl lemma to have a proof by simp but not one by dsimp, and so this is a false positive. The linter should check if the current declaration is a rfl lemma and if so restrict its attention to dsimp proofs.

[kim-em]

I've just updated the links in mathlib4 pointing to mathlib4#5081 to point to this issue instead.

This link searches for references to this issue in the mathlib4 source code.