How to prove a target with `ite` by cases

Stream: new members

[Rui Liu]

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]

split_ifs should generate the two goals, casing on p

[Yakov Pechersky]

If you want more control, you can do

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

[Rui Liu]

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