contracting `by_cases`

Stream: new members

[Heather Macbeth]

Suppose I have a proof beginning with by_cases, and one of the cases is answered by a single lemma. Is there a syntactic trick to combine these two lines (the by_cases and the exact [lemma]) into one line?

[Adam Topaz]

You can probably do something with refine and LEM.

[Heather Macbeth]

Yes, I was hoping so -- do you know the syntax?

[Adam Topaz]

My first guess would be to try something approximately like this: refine or.elim (classical.em h) _ _ and fill in the blanks as necessary.

[Heather Macbeth]

Thanks! The or.elim is what I needed.

[Adam Topaz]

Maybe a better way would be to refine decidable.by_cases, since (I assume) that's what by_cases actually does

[Mario Carneiro]

You could also write something like refine if h : p then term else _