unnecessarily tombstoned argument

Stream: lean4

[Scott Morrison]

In

theorem foo {P : R → Prop} : (a : R) → P a
  | a => sorry

at the sorry the goal state is

x✝: R
a: R := x✝
⊢ P x✝

This is weird, and inconvenient, and requires using change to get to goal back to usable form in some proofs. Am I missing some essential reason this is expected, or should I file an issue for this?

[Scott Morrison]

(This came up in mathlib4#871.)

[Trebor Huang]

Doesn't that mean you pattern matched on a unnamed variable (since it is at the right of the copula) with a trivial pattern? So we naturally have this situation. Lean could have done some simplification though