doc: document the full syntax for the deprecation attribute

The other day, I wanted to apply the full form (with a custom message and a deprecation date) in mathlib and failed to guess the correct order. The doc-string seemed to suggest that combining them was impossible (which was luckily false). Let's clarify that
- a custom message and deprecation date can be combined
- what the expected order is

Author: grunweg

src/Init/Notation.lean

@@ -564,6 +564,8 @@ existing code. It may be removed in a future version of the library.
 * `@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
 * `@[deprecated myBetterDef "use myBetterDef instead"]` allows customizing the deprecation message.
 * `@[deprecated (since := "2024-04-21")]` records when the deprecation was first applied.
+* the last two options can be combined: @[deprecated myBetterDef "use myBetterDef instead" (since := "2024-04-21")]`
+  customizes the deprecation message and specifies the deprecation date
 -/
 syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
     (" (" &"since" " := " str ")")? : attr