rw generates duplicate goals

Stream: mathlib4

[Scott Morrison]

Sometimes rw produces duplicate goals, when one of the argument of the lemma you are rewriting by is unified with an existing metavariable:

example (f : Nat → Nat) (h : ∀ x, f x = 0) : { x : Nat // f x = 0 } := by
  refine ⟨?x, ?w⟩
  rotate_left
  rw [h]
  trace_state -- two goals! `case x` is reported twice, but ideally only once.
  exact 37

It don't really see a way around this except sticking a recover in the definition of rewriteTarget. Any other ideas?

It's not a particularly harmful problem, but it does annoy me a little!

[Sky Wilshaw]

I've seen a similar thing happen in certain have := ... ?_ statements where new metavariables need to be unified. The goals will be given twice, but closing one closes the other.