Focus on case without closing it

Stream: lean4

[Alex Keizer]

Is there a way to focus on a specific goal in a cases proof, preferably by tag/name, without having to close it within the focused block?

I currently have something like this

  intro eqv wt;
  induction wt
  <;> cases eqv
  case SndLeft.refl     => apply SndLeft          <;> repeat assumption
  case SndRight.refl    => apply SndRight         <;> repeat assumption
  case RcvLeft.refl     => apply RcvLeft          <;> repeat assumption
  case RcvRight.refl    => apply RcvRight         <;> repeat assumption

Where each case starts differently, but they all end the same. Instead of having <;> repeat assumption everywhere, I'd much rather have the following

  case SndLeft.refl     => apply SndLeft
  case SndRight.refl    => apply SndRight
  case RcvLeft.refl     => apply RcvLeft
  case RcvRight.refl    => apply RcvRight
  any_goals
    repeat assumption

But this fails with unsolved goals at each case

[Arthur Paulino]

Mathlib4 has the on_goal tactic, which is similar to work_on_goal. The difference is basically the syntax, since tactic mode is slightly different from Lean 3

[Arthur Paulino]

Ah, the index now starts from 1 instead of 0 (for standardization purposes). You'll see it in the docstring