When to use @[simp]

Stream: new members

[Vlad Tsyrklevich]

I've read the simp page on the lean community site, but I still had a few questions about when a lemma should carry @[simp]. One simple example is neg_inj: in Mathlib, docs#neg_inj is a simp lemma, so for example:

import Mathlib
example (a b : Int) : -a = -b := by simp

leaves you with the final goal "a = b", but lean's internal docs#Int.neg_inj is not marked @[simp], so removing the Mathlib import leaves the final state as "-a = -b". This example is kind of trivial, since perhaps it's not necessary to get rid of the negative signs for simp to close the goal if you can actually simplify a and b to the same term, but given that Int.neg_inj is in the core library I thought perhaps there was a principled reason for why they chose to not mark it @[simp].

I guess I often see theorems not marked @[simp] that are clearly simplifying the LHS, and I'm not sure if they're not marked as such for a specific reason to do with normal forms/confluence/etc. or if there is also just a factor of 'the author didn't consider the theorem general enough to mark it @[simp]'