## Stream: Is there code for X?

### Topic: ite lemma

#### 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?

#### Mario Carneiro (Jan 12 2021 at 19:41):

by simp gets it

#### 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

#### 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


#### 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