Zulip Chat Archive

Stream: Is there code for X?

Topic: ite lemma


view this post on Zulip Heather Macbeth (Jan 12 2021 at 19:39):

import tactic

variables {α : Type*} [decidable_eq α]

example (a b : α) : ite (a = b) a b = b :=
begin
  split_ifs,
  { exact h },
  { refl }
end

Does this lemma exist? Or is there a short term-mode proof?

view this post on Zulip Mario Carneiro (Jan 12 2021 at 19:41):

by simp gets it

view this post on Zulip Mario Carneiro (Jan 12 2021 at 19:42):

example (a b : α) : ite (a = b) a b = b :=
by simp only [ite_eq_right_iff, imp_self]

a clever proof if I do say so myself

view this post on Zulip Mario Carneiro (Jan 12 2021 at 19:42):

the term mode proof being

example (a b : α) : ite (a = b) a b = b :=
ite_eq_right_iff.2 id

view this post on Zulip Heather Macbeth (Jan 12 2021 at 19:47):

Nice! It arose for me with the equality swapped -- here simp doesn't work, but a variation of your term mode proof does:

example (a b : ) : ite (b = a) a b = b :=
ite_eq_right_iff.2 eq.symm

Last updated: May 19 2021 at 02:10 UTC