Combination of extended field notation, indexing, and `by` clobbers definition with metavariable

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

-- Any predicate works as long as extended field notation `e.f` can be used
abbrev Nat.isSucc : Nat → Bool
| .succ _ => true | .zero => false

example {arr : List Nat} :=
  List.finRange arr.length
    |>.filter (fun j => arr[j].isSucc)
    |>.get ⟨0, by sorry⟩

Observe that the state after the by is 0 < (List.filter (fun j => ?m.6) (List.finRange arr.length)).length; the filter function has been replaced by a metavariable.

Context

I was trying to finish the following function to find the next some in an array (possibly wrapping around).

def nextSome {arr : Array (Option α)}
    (i : Fin arr.size) (h : ∃ a ∈ arr, a.isSome) : Fin arr.size :=
  List.finRange arr.size
    |>.map (· + i)
    |>.filter (fun j => arr[j].isSome)
    |>.get ⟨0, by
      -- goal : `0 < (List.filter (fun j => ?m.20) ...`
      sorry⟩

I worked around the issue by generalizing the predicate.

@[specialize] private def next {arr : Array α} (p : α → Bool) (i : Fin arr.size)
    (h : ∃ a ∈ arr, p a) : Fin arr.size := ...

Steps to Reproduce

1. See above.

Expected behavior: The filter predicate is displayed in the goal state at the sorry.

Actual behavior: The goal state after the by is 0 < (List.filter (fun j => ?m.6) (List.finRange arr.length)).length.

Versions

Lean 4.22.0
Target: arm64-apple-darwin23.6.0 macOS
MacOS Sonoma 14.1

I initially encountered it on v4.23.0-rc2. I've also reproduced it on live.lean-lang.org.

Additional Information

Writing the predicate as Nat.isSucc arr[j] fixes the problem.

Removing the by fixes the problem.

Replacing the function with fun j => j.val.isSucc fixes the problem. So does modifying the predicate to have type Fin m → Bool and replacing the filter function with j.isSucc. Therefore, I believe the list indexing contributes to this bug.

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 reproducer in the issue and compare the failing combination of extended field notation, indexing, and by with the listed workarounds. Trace the elaboration of the filter predicate and verify that the goal preserves it after the proof block; done means the predicate is displayed correctly and the regression is covered by a test.