help reducing duplicated code

Stream: lean4

[Jesse Slater]

I am doing a proof by cases with a match statement , and three of my cases have exactly the same proof. However, I can't figure out how to combine it and only write that proof once.
image.png

I tried using wildcards, but that did not work.
image.png

The match does recognize that these are the three cases that need to be solved if I omit them.
image.png

[Marcus Rossel]

Could you post a #mwe? Also, images are a bit annoying to work with for people trying to give solutions - try #backticks.

[Chris Bailey]

Try this syntax:

| ⟨1, 0⟩ | ⟨0, 1⟩ | ⟨0, 0⟩ => /- your proof -/

[Jesse Slater]

Thanks!