rw duplicates goals for metavariables appearing in the rewritten expression

[JovanGerb]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When rewriting a term that contains metavariables, this metavariable is added as a new goal in the tactic state, even if it already is a goal. This clutters the tactic state and is confusing.

Context

Question on Zulip

Steps to Reproduce

The example provided on Zulip is:

example : ∀ d g, d = g → exists x : Nat, x = d := by
  intros d g H1
  constructor
  rewrite [H1,←H1,H1,←H1,H1]
  -- rotate_left; exact g; rfl

Expected behavior: [Clear and concise description of what you expect to happen]

The goal

dg: Nat
H1: d = g
⊢ Nat

should still appear only once after the rewrites

Actual behavior: [Clear and concise description of what actually happens]

The goal appears 6 times after the 5 rewrites.

Versions

4.7.0 (works on any version)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[JovanGerb]

I've made a fix for it here: #4383

[eric-wieser]

Either this has regressed, or the fix wasn't exhaustive: see #6407