## Stream: Is there code for X?

### Topic: Distributing prod.fst or prod.snd over an ite

#### Yakov Pechersky (Nov 13 2020 at 18:48):

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 (Nov 13 2020 at 18:48):

Maybe in some pi format for inductive types?

#### Kevin Buzzard (Nov 13 2020 at 20:42):

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)

docs#apply_ite

#### Yakov Pechersky (Nov 13 2020 at 20:49):

Heh, I wrote the docstring for that...

#### Kevin Buzzard (Nov 13 2020 at 20:50):

Thank you :-)

Last updated: May 16 2021 at 05:21 UTC