bug in replace

Stream: mathlib4

[Scott Morrison]

There's a bug in goal handling in replace:

import Mathlib.Tactic.Replace

example (h : True) : False := by -- (kernel) declaration has metavariables '_example'
  replace h

Would anyone like to investigate? I hope it is pretty straightforward to fix.

[Jireh Loreaux]

I'll have a look tonight.

[Kyle Miller]

#7939 (If anyone wants more tests, feel free to push.)