Equivalent of `Or.elim` for if-then-else/`Decidable`

Stream: Is there code for X?

[Will Bradley]

I can eliminate an ite term if I know both branches satisfy a predicate. I'm sure there must be something like this in mathlib, but I can't find it. Would someone mind pointing me in the right direction?

theorem Decidable.ite_elim {p: Prop} {q: τ → Prop} {a b: τ} {ha: q a} {hb: q b} [Decidable p]: q (if p then a else b) := by
  split <;> assumption

theorem Decidable.dite_elim {p: Prop} {q: τ → Prop} {a b: τ} {ha: q a} {hb: q b} [Decidable p]: q (if _: p then a else b) := by
  split <;> assumption

[Yaël Dillies]

Something like simp [ite_apply, *] should work, but indeed I would hope there is a specific lemma for you to use

[Will Bradley]

Yaël Dillies said:

Something like simp [ite_apply, *] should work, but indeed I would hope there is a specific lemma for you to use

It should be apply_ite, right? Also, my use case is covered by the split tactic since I'm already in tactic mode

[Robert Maxton]

docs#iteInduction technically counts, though it's a bit clunky and I don't think it's rwable:

theorem Decidable.ite_elim {p: Prop} {q: τ → Prop} {a b: τ} {ha: q a} {hb: q b} [Decidable p]: q (if p then a else b) := by
  exact iteInduction (fun _ ↦ ha) (fun _ ↦ hb)

theorem Decidable.dite_elim {p: Prop} {q: τ → Prop} {a b: τ} {ha: q a} {hb: q b} [Decidable p]: q (if _: p then a else b) := by
  exact dif_eq_if .. ▸ iteInduction (fun _ ↦ ha) (fun _ ↦ hb)

[Robert Maxton]

as a side note, we maybe shouldn't have both docs#ite_id and docs#ite_self