PR #5883 added a new syntax for tactic configuration, and this PR
enables it in most tactics. Example: `simp +contextual`.
There will be followup PRs to modify the remaining ones.
Breaking change: Tactics that are macros for `simp` or other core
tactics need to adapt. The easiest way is to replace `(config)?` with
`optConfig` and then in the syntax quotations replace `$[$cfg]?` by
`$cfg:optConfig`. For tactics that manipulate the configuration, see
`erw` for an example:
```lean
macro "erw" c:optConfig s:rwRuleSeq loc:(location)? : tactic => do
`(tactic| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq $(loc)?)
```
Configuration options are processed left-to-right, so this forces the
`transparency` to always be `.default`.
This is a quite substantial tactic.
It also includes the infamour `NatCast` typeclass (which I've equipped
with a module-doc). I wasn't at all sure where that should live, so it
is currently randomly in `Lean/Elan/Tactic/NatCast.lean`: presumably if
we're doing this it will go somewhere in `Init`.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
