feat(tactic/#simp): a user_command for #simp (#2446)
```lean
#simp 5 - 5
```
prints `0`.
If anyone knows how to get access to local `variables` while parsing an expression, that would be awesome. Then we could write
```lean
variable (x : ℝ)
#simp [exp_ne_zero] : deriv (λ x, (sin x) / (exp x)) x
```
as well as
```lean
#simp [exp_ne_zero] : λ x, deriv (λ x, (sin x) / (exp x)) x
```
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
