Deferring `getElem` proofs leads to `declaration has free metavariables` when using `omega`

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

Deferring getElem proofs leads to declaration has free metavariables when using omega.
Trying grind for the same proofs can lead to tactic 'grind' failed, the goal mentions the declaration `_example`, which is being defined. To avoid circular reasoning, try rewriting the goal to eliminate `_example` before using `grind`..

Steps to Reproduce

Check

theorem Array.extract_add_one' {xs : Array α} (h₁ : i ≤ j) (h₂ : j < xs.size) :
    (xs.extract i (j + 1)) = (xs.extract i j).push xs[j] := by
  simp [h₁]

example {arr : Array Nat} (h : 1 < arr.size) : arr.extract 0 2 = #[1, 2] → arr[0] = 1 := by 
  intro h
  rw [Array.extract_add_one'] at h 
  rw [Array.extract_add_one'] at h
  simp at h
  all_goals try omega
  grind

(live)

Expected behavior: Should type check

Actual behavior: Does not type check. The use of omega reports (kernel) declaration has free variables '_example._proof_2'.

Versions

Lean 4.21.0-nightly-2025-06-05

Additional Information

• Moving the simp at h below the all_goals try omega resolves the issue.
• Discharging proofs immediately via rw [Array.extract_add_one'] at h <;> try omega resolves the issue.
• Using grind first instead of omega resolves the issue: all_goals try grind; all_goals omega. Doing all_goals grind fails with tactic 'grind' failed, the goal mentions the declaration `_example`, which is being defined. To avoid circular reasoning, try rewriting the goal to eliminate `_example` before using `grind`.

Impact

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

Start by reproducing the minimal theorem from the issue on Lean 4.21.0-nightly-2025-06-05, comparing the proof-ordering variants using omega and grind. Trace how deferred getElem proofs and simp affect the generated goals; done means the example type checks without free-metavariable or circular-declaration errors.