Docs for simp attribute

Stream: mathlib4

[Filippo A. E. Nuccio]

The current snippet explaining what @[simps] does contains nothing about simps!: yet these explanations are in the linter, so it would perhaps be easy to merge the two. I do not feel competent enough to do it myself.

[Robin Arnez]

Which linter? I can only find simp! in proofs and not in a linter

[Robin Arnez]

Wait, you probably meant @[simps] and @[simps!], right? In that case, yeah I guess that would be reasonable