## Stream: new members

### Topic: Getting stuff out of a definition using dite

#### Alexandru-Andrei Bosinta (Nov 25 2018 at 23:34):

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 (Nov 25 2018 at 23:36):

dif_pos / dif_neg

#### Kevin Buzzard (Nov 26 2018 at 08:24):

in tactic mode perhaps split_ifs can also help.

Last updated: May 06 2021 at 22:13 UTC