ite_eq_imp_iff

Stream: Is there code for X?

[Joshua E Cook]

Is there a library theorem that shows this?

example {α : Sort _} (p q : Prop) [dp: decidable p] [dq: decidable q] (a b : α)
: (a ≠ b) → (ite p a b = ite q a b) → (p ↔ q) := sorry

[Eric Wieser]

That last implication is an iff, right?

[Joshua E Cook]

@Eric Wieser yes it could be, but I'm currently only interested in this direction

[Joshua E Cook]

It appears this works; but do I need the match clause?

example {α : Sort _} (p q : Prop) [dp: decidable p] [dq: decidable q] (a b : α)
: (a ≠ b) → (ite p a b = ite q a b) → (p ↔ q) :=
match dp, dq with
| is_false hp, is_false hq := by cc
| is_false hp, is_true hq := by cc
| is_true hp, is_false hq := by cc
| is_true hp, is_true hq := by cc
end

[Kevin Buzzard]

If you're happy to use mathlib:

import tactic

example {α : Sort _} (p q : Prop) [dp: decidable p] [dq: decidable q] (a b : α)
: (a ≠ b) → (ite p a b = ite q a b) → (p ↔ q) :=
begin
  split_ifs;
  cc
end

[Joshua E Cook]

@Kevin Buzzard ty! I wasn't aware of split_ifs.