Rpc error on hole in `cases with` tactic

Stream: lean4

[Yakov Pechersky]

The error I get in the goal view is Error updating: Error fetching goals: Rpc error: InternalError: unknown metavariable '?_uniq.138'., from:

theorem foo : True := by
  have : ∃ x, x = 0 := ⟨0, rfl⟩
  cases this with | intro x h => _

Is cases incompatible with _ to see the goal?

[Mario Carneiro]

cases has special handling for _ (which can be surprising if you are using the _ tactic from mathlib/std which is shorthand for {}), it will just return the subgoal after the cases instead of inside the match arm

[Mario Carneiro]

that may be affecting the goal annotations

[Kevin Buzzard]

Can you put sorry and click just before the s?

[Mario Carneiro]

tested: you can, it works fine. It is only the _ itself that is messed up

[Mario Carneiro]

same thing happens with ?_ in that position

[Mario Carneiro]

same thing also happens with ?a in

theorem foo : True := by
  have : ∃ x, x = 0 := ⟨0, rfl⟩
  cases this with | intro x h => ?a
  case a => sorry

[Mario Carneiro]

my guess is that cases isn't registering the metavars created for the subgoals here in the metavar context