simpNF bug?

Stream: mathlib4

[Adam Topaz]

I'm confused about something that came up in my recent (non-porting) PR !4#4505
Specifically, see this line: https://github.com/leanprover-community/mathlib4/blob/907342d3115927f903ea5ff48c828e7c65402d50/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean#L275

The simpNF linter complains about some lemmas, but it seems to me that the two lemmas are perfectly valid simp lemmas (one of them being automatically generated by reassoc). Can anyone tell why it's complaining?

[Kevin Buzzard]

What is the actual complaint?

[Adam Topaz]

/- 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 @EffectiveEpiFamily.fac_assoc /- Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.
 -/
#check @EffectiveEpiFamily.fac /- Left-hand side does not simplify, when using the simp lemma on itself.
This usually means that it will never apply.
 -/

[Adam Topaz]

But as you can clearly see in the two examples, the lemmas do indeed apply :)