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.

[kim-em]

This is fixed now, no? #839 (and as reapplied in #844).

@jcommelin?

[jcommelin]

Yeah, we can close this.