Distributing prod.fst or prod.snd over an ite

Stream: Is there code for X?

[Yakov Pechersky]

Do these lemmas exist?

@[simp] lemma prod.ite_fst {α β : Sort*} {p : Prop} [decidable p] {x y : α × β} :
  (ite p x y).fst = ite p x.fst y.fst :=
or.elim (em p) (λ h, by simp only [h, if_true]) (λ h, by simp only [h, if_false])

@[simp] lemma prod.ite_snd {α β : Sort*} {p : Prop} [decidable p] {x y : α × β} :
  (ite p x y).snd = ite p x.snd y.snd :=
or.elim (em p) (λ h, by simp only [h, if_true]) (λ h, by simp only [h, if_false])

[Yakov Pechersky]

Maybe in some pi format for inductive types?

[Kevin Buzzard]

They are surely both special cases of some function which should be called something like ite_congr or something, saying F (ite p x y) = ite p (F x) (F y)

[Yakov Pechersky]

docs#apply_ite

[Yakov Pechersky]

Heh, I wrote the docstring for that...

[Kevin Buzzard]

Thank you :-)