rw if then else

Stream: Is there code for X?

[Winston Yin (尹維晨)]

I don't really know how to work with ite. If I have a hypothesis hp : p, how can I rewrite if p then a else b into a? Similarly for hp : ¬p, please.

[Mario Carneiro]

if_pos, if_neg

[Mario Carneiro]

or simp [hp], since these are simp lemmas

[Eric Rodriguez]

I thought simp simplified by rewriting p into True, and then used docs#if_true

[Eric Rodriguez]

(indeed it seems docs#if_pos isn't simp)

[Winston Yin (尹維晨)]

^ yes, that's why I couldn't find if_pos...

[Andrew Yang]

There's also dif_pos and dif_neg for dependent ifs.