Getting stuff out of a definition using dite

Stream: new members

[Alexandru-Andrei Bosinta]

How do I use a definition that uses dite? All my attempts of writing the definition, it's required arguments followed by a proof of the if condition failed, with Lean giving me an error like it had no idea what I was trying to do.

[Kenny Lau]

dif_pos / dif_neg

[Kevin Buzzard]

in tactic mode perhaps split_ifs can also help.