Using proof of case to reduce if-then-else expression

Stream: new members

[Oskar Berndal]

Hi there! I am having more troubles with simple if-then-else constructions. Here's an example:

inductive AB
| a : AB
| b : AB

def ab : ℕ → ℕ → AB
| n m := if n = m then AB.a else AB.b

lemma eq : Π n m : ℕ, ¬ n = m → (ab n m = AB.b) :=
begin
  sorry
end

Say that I do intros and my context now contains the term a : ¬ n = m. How can I use this hypothesis to 'simplify' goal to AB.b = AB.b?

[Johan Commelin]

unfold ab, to unfold the definition, and then rw if_neg a

[Johan Commelin]

also, note that there is a split_ifs tactic, to break an if-statement into its branches.

[Oskar Berndal]

This was precisely what I was looking for, especially digging the if_neg, many thanks ^_____^