Fixes #2495 and #2434 by making sure that withCollectingNewGoals only returns mvarIds created during elaboration. This changes the behavior of elabTermWithHoles and refine accordingly: refine e now replaces the main goal only with goals that were created during elaboration of e (and does not include goals that appear in e but existed prior to its elaboration).

Consequences of this change:

• This prevents duplication of goals in the infoview by refine (bug: refine duplicates goals in the infoview #2495): pre-existing goals are now excluded from the resulting tactic state, and thus don't appear twice.
• It also prevents "goal tunneling", wherein a goal that was created before a given refine statement manages to be included in its resulting goals unexpectedly, due to being present in e.g. an implicit argument.
• Previously, refine was inconsistent in which pre-existing goals were returned; this is the content of issue bug: refine loses track of natural goals #2434, which points out that pre-existing natural mvars are not returned, while synthetic mvars are. refine's occurs check relied on all mvars appearing in the expression being returned, and so goals were erroneously closed. This renders that issue moot by uniformly not returning any old mvars, and updating the occurs check accordingly.
• This PR breaks mathlib, and requires fixes to a few proofs that use refine and convert (which relies on withCollectingNewGoalsFrom). All breakages are instances of goal tunneling, and are easily fixed. These fixes are done in bump: lean4: account for leanprover/lean4#2502 leanprover-community/mathlib4#6928. Note, however, that it breaks mathlib less than an incremental fix of bug: refine loses track of natural goals #2434 alone, which required us to filter out old mvars anyway in change.
• Finally, metaprogrammers likely expect elabTermWithHoles and withCollectingNewGoalsFrom to behave in this way already—see zulip for an expression of this sentiment.

Note also that this streamlines the code of withCollectingNewGoalsFrom, replacing

    let newMVarIds ← if allowNaturalHoles then
      pure newMVarIds.toList
    else
      let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← mvarId.getKind).isNatural
      let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← mvarId.getKind).isNatural
      let naturalMVarIds ← filterOldMVars naturalMVarIds mvarCounterSaved
      logUnassignedAndAbort naturalMVarIds
      pure syntheticMVarIds.toList

with simply

    let newMVarIds ← filterOldMVars newMVarIds mvarCounterSaved
    unless allowNaturalHoles do
      let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← mvarId.getKind).isNatural
      logUnassignedAndAbort naturalMVarIds

(plus comments).

Changes made by this PR

• prevents withCollectingNewGoalsFrom, and therefore elabTermWithHoles, refine, and specialize from returning old goals

• updates the occurs check in refine to compensate for this change (note that specialize does not have an occurs check; this is a separate issue)

• adds a missing docstring to elabTermWithHoles

• adds tests for bug: refine duplicates goals in the infoview #2495, goal tunneling, and bug: refine loses track of natural goals #2434

• changes test run/492.lean, which made incidental use of goal tunneling

• Put an X in this bracket to confirm you have read the
  External Contribution Guidelines.