ite or

Stream: Is there code for X?

[Yaël Dillies]

Do we not have this?

lemma ite_eq_or_eq {p : Prop} [decidable p] (a b : V) :
  ite p a b = a ∨ ite p a b = b :=
decidable.by_cases (λ h, or.inl (if_pos h)) (λ h, or.inr (if_neg h))

[Ruben Van de Velde]

docs#ite_eq_iff is a little stronger

[Yaël Dillies]

Argh, I want to .resolve that.
I'll just PR it. #8557