working with ite

Stream: new members

[Michael Hahn]

h: z = v
odd: path.crossed z (p_1.cons e hs hv hsv) = path.crossed z p_1 + ite (z = v ∨ z = p_1.head) 1 0

I'm not super familiar with how to use ite, but I want to use h into odd to reduce the ite that i have

[Alex J. Best]

As you know the if is true you can use

rw if_pos at odd

which will change the ite to be 1, and give you the goal to prove z = v ∨ z = p_1.head separately.

[Kenny Lau]

rw if_pos (or.inl h) at odd

[Jalex Stark]

maybe simp [h] would get you all the way to not have an ite any more. My model here is that first it will change z = v to z = z, then change that to true then change true \or _ to true then change ite true 1 _ to 1.

[Jalex Stark]

I think if you know about rw if_pos, rw if_neg, and split_ifs, you should always be able to navigate through ite.

[Jalex Stark]

(and if it's a dite, the lemmas are called dif_pos and dif_neg)