ite lemma

Stream: Is there code for X?

[Heather Macbeth]

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]

by simp gets it

[Mario Carneiro]

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]

the term mode proof being

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

[Heather Macbeth]

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