simpNF vs "dsimpNF"

Stream: mathlib4

[Calle Sönne]

I am adding some API to Cat, and I am runnning into a linter problem with simpNF and I am wondering what to do. The short story is that my lemma is not in simpNF, but it is proven by rfl, and the lemmas taking it to simpNF are not dsimp lemmas. What should I do here? The problem is if I rewrite it to simpNF then dsimp will not be able to prove the original lemma, because the lemmas taking it to simpNF are not dsimp lemmas.

Here is one of the lemmas for reference:

@[simp]
lemma leftUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : B) : (λ_ F).hom.app X = 𝟙 (F.obj X) :=
    rfl

The reason the LHS is not in simpNF is because strict bicategories have a simp-lemma rewriting (λ_ F) to eqToIso, but this is usually proved automatically by aesop_cat when defining the strict bicategory instance, so dsimp can't use it.

[Eric Wieser]

There is work going on to fix this right now :)

[Eric Wieser]

For now you can nolint simpNF with a comment about dsimp

[Calle Sönne]

perfect, thanks!

[Calle Sönne]

Actually, maybe it would be a good idea to make the lemma (λ_ F) = eqToIso a dsimp lemma. How would I go about doing this? Proving it by rfl when defining the instance as follows doesn't seem to work:

instance bicategory.strict : Bicategory.Strict Cat.{v, u} where
  id_comp {C} {D} F := by cases F; rfl
  comp_id {C} {D} F := by cases F; rfl
  assoc := by intros; rfl
 -- This doesn't make it a dsimp lemma sadly
  leftUnitor_eqToIso F := rfl

I'm guessing this is because the place where its tagged @[simp] is in another file, which is in a more general setting where it can't be proven by rfl. Can I somehow overwrite that here (and would that even be a good idea)?