Panic when using `intro` followed by `pattern` in `conv` mode

Prerequisites

• 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

Using pattern under a binder in conv mode causes a panic at Lean.Expr.mvarId!.

Steps to Reproduce

Lean 4 Web

-- panics at Lean.Expr.mvarId!
example : (fun x : Nat => x + (x - x)) = (fun x => x) := by
  conv =>
    lhs
    intro x
    pattern _ - _
    simp

-- works
example (x : Nat) : x + (x - x) = x := by
  conv =>
    lhs
    pattern _ - _
    simp
  simp

Expected behavior: No panic.

Actual behavior: PANIC at Lean.Expr.mvarId! Lean.Expr:1012:14: mvar expected.

Context

Discussion on Zulip about a related error

Versions

4.32.0-nightly-2026-06-10

Start with the minimal reproducer in the issue and compare it with the working example that omits the binder. Trace the conv handling of intro followed by pattern, focusing on the Lean.Expr.mvarId! panic. Done means the reproducer no longer panics and the existing working case remains valid.