feat: simpLocation

[semorrison]

This refactors evalSimp, the implementation of the simp [...] at ... syntax, into two functions. Now evalSimp just handles the Syntax parsing, while simpLocation dispatches to the simpGoal tactic in Lean.Meta.Tactic.Simp according to a location argument.

I want this separation so that when writing other tactics, I can invoke the simplifier using a location, without having to synthesize a Syntax. (The specific application is in porting split_ifs.)

See also discussion on zulip.

[leodemoura]

@semorrison BTW, we have a split tactic in core Lean that splits if and match expressions. It has many features for match. See split*.lean tests at tests/lean/run for examples. That being said, it may be incompatible with the splif_if tactic.