fix: ignore implDetail hyps in withLocation

[JLimperg]

As reported on Zulip, the MWE

theorem a_lemma : 1 = 2 := sorry

example : 1 = 3 -> 1 = 3 := by
  intro h
  rewrite [a_lemma] at *

would produce the goal

_example: 2 = 3 → 2 = 3
h: 2 = 3
⊢ 2 = 3

since rewrite also applied to the implementation detail hypothesis _example. This PR makes the withLocation combinator, which rewrite uses to process the at * syntax, ignore implementation detail hypotheses.