simplify dite

Stream: Is there code for X?

[Chase Norman]

I have a goal with a dite expression. For ite, ite_eq_left_iff and ite_eq_right_iff allow me to simplify the expression easily. Are there analogous lemmas for dite?

[Adam Topaz]

The API search came up short for me, but you can always use the split_ifs tactic

[Adam Topaz]

tactic#split_ifs

[Chase Norman]

Thank you so much!

[Scott Morrison]

I use rw dif_pos or rw dif_neg when I want to specify which way it goes.