Switch current goal based on pattern

Stream: Is there code for X?

[Dylan Ede]

I'm only just beginning with Lean, so I'm probably missing something obvious, but how do I switch the current goal to the one matching a given pattern?

[Eric Wieser]

Can you give a #mwe?

[Eric Wieser]

Are you describing a case similar to having three goals x = 0, y = 0, and x + y = z, and you want to work on the y = 0 goal first?

[Eric Wieser]

If so that's tactic#show

[Dylan Ede]

Yes, exactly. I had tried that before but thought it didn't work. Now I see that my actual problem was that the pattern I gave matched both goals. D'oh!