Zulip Chat Archive

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)

Yakov Pechersky (Nov 13 2020 at 20:44):

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: Dec 20 2023 at 11:08 UTC