SimpNF failing to suggest right simp

Stream: mathlib4

[Jihoon Hyun]

In Algebra.Star.Basic L342, simpNF claims that the theorem can be proved with simp, and introduces by simp only [@RingHomCompTriple.comp_apply, @RingHom.id_apply]. However, this doesn't work. Will this be the bug of the linter?

[Siddhartha Gadgil]

I did not notice this or check and removed the simp attribute (adding a porting note). Alerting in case a proper fix is needed.