`apply` duplicates goals

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

The apply tactic sometimes duplicates the same MVarId in the list of goals

Context

Came up when trying to use split on a target containing metavariables.

Steps to Reproduce

Run

theorem apply_duplicate_goal : ∃ a : Int, a = 1 := by
  refine ⟨?x, ?y⟩
  rotate_left
  apply (eq_comm (b:=?x)).mp
  -- three goals
  sorry
  -- two goals
  sorry
  -- zero goals

(The (b:=?x) is actually optional.)

Expected behavior: There should be two goals after apply

Actual behavior: The goal state after apply is

case y
⊢ 1 = ?x
case x
⊢ Int
case x
⊢ Int

Versions

Lean 4.21.0, commit ebf455a13780ea508abee8016b8bb6c5549bf9d7

Additional Information

This is likely the same issue as https://github.com/leanprover/lean4/issues/6407.

Impact

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

Start with the minimal apply_duplicate_goal theorem and reproduce the goal state using the listed Lean 4.21.0 version. Trace the apply tactic from this example and verify that the same MVarId is not listed twice, leaving the expected two goals.