attribute simp_NF_my_lemma?

Stream: mathlib4

[Joël Riou]

In the linked code https://github.com/leanprover-community/mathlib4/pull/13463/files#diff-0e85160543270c3e17ee0dccb9d4dfef5316069b47db4d288a89c1a67ded1c07R67-R76 there are two lemmas both of which I would like to be (d)simp lemmas, but the first lemma would simplify the LHS of the second lemma, so that the linter complains:

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
#check @pushforward_obj_map_apply /- Left-hand side simplifies from
  (((pushforward φ).obj M).map f) m
to
  (((pushforward φ).obj M).map f) m
using
  simp only [@pushforward_obj_obj, @Functor.comp_obj, @Functor.op_obj]
Try to change the left-hand side to the simplified term!
 -/

Here, pushforward_obj_obj simplifies (in a rather invisible manner) the LHS of pushforward_obj_map_apply. (Similar issues happen all the time with lemmas involving DFunLike.coe.)

At the declaration of the second lemma pushforward_obj_map_apply, would there be a way to say (via an attribute?): I know that the LHS is not in simpNF, please simpNF it for me!

If this were possible, I feel it would ease very much the development of category theory and algebraic geometry!

[Andrew Yang]

I also encountered such a problem at #13412 and here's a mwe

import Mathlib.Logic.Equiv.Defs

@[simp] def A := Nat
def e : A ≃ Nat := Equiv.refl _
@[simp] lemma e_apply (x) : e x = x := rfl

example (x) : e x = x := by simp -- fails because `A` gets rewritten to `Nat` first.

#lint only simpNF -- fails (as expected)