## Stream: new members

### Topic: How to prove a target with ite by cases

#### Rui Liu (Dec 25 2020 at 16:23):

I have a goal of form (ite p a b) = c, how do I prove by cases on p and generate two goals?

#### Yakov Pechersky (Dec 25 2020 at 16:27):

split_ifs should generate the two goals, casing on p

#### Yakov Pechersky (Dec 25 2020 at 16:28):

If you want more control, you can do

by_cases hp : p,
{ rw if_pos hp,
sorry },
{ rw if_neg hp,
sorry }


#### Rui Liu (Dec 25 2020 at 16:29):

@Yakov Pechersky Thank you, that's fast and exactly what I want :)

Last updated: May 14 2021 at 12:18 UTC