ite_or equivalent of ite_and

Stream: mathlib4

[EdwardW]

As far as I can tell, there is no ite_or equivalent of ite_and.
The implementation can be identical to ite_and, and it seems both useful and nice for the sake of completeness:

theorem ite_and : ite (P ∧ Q) a b = ite P (ite Q a b) b := by
  by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

theorem ite_or : ite (P ∨ Q) a b = ite P a (ite Q a b) := by
  by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

Is there any particular reason that this is not in Mathlib / Is this wanted in Mathlib?

[Johan Commelin]

I think it makes perfect sense to have this in mathlib

[EdwardW]

Cool, I'll submit a PR tomorrow if no one objects