# Zulip Chat Archive

## Stream: general

### Topic: ite term golf

#### Andrew Ashworth (May 27 2018 at 07:28):

Suppose I need to prove `ite (x = y) tt ff = tt → x = y`

and `x = y → ite (x = y) tt ff = tt`

. Is there a succint way to do this in term mode? (I know `simp`

and `split_ifs`

is amazing here, but I'd like to do inversion by hand if possible)

#### Nicholas Scheel (May 27 2018 at 07:43):

this should take care of the second part: https://github.com/leanprover/lean/blob/master/library/init/logic.lean#L839

#### Nicholas Scheel (May 27 2018 at 07:48):

for the first part I wonder if something like the following would work (untested):

λ h, if p : (x = y) then p else bool.no_confusion (eq.trans (eq.symm h) (if_neg p))

basically you decide the proposition (equivalent to the by_cases tactic) and then return the true case, or prove the false case is absurd

#### Nicholas Scheel (May 27 2018 at 07:50):

maybe this is easier than no_confusion: https://github.com/leanprover/lean/blob/master/library/init/logic.lean

#### Nicholas Scheel (May 27 2018 at 07:50):

`absurd (eq.symm (eq.trans .....)) bool.ff_ne_tt`

#### Nicholas Scheel (May 27 2018 at 07:51):

btw I think this is just `if p then tt else ff`

: https://github.com/leanprover/lean/blob/master/library/init/logic.lean#L590

#### Mario Carneiro (May 27 2018 at 13:11):

use `to_bool`

, it has lots of lemmas for this

#### Andrew Ashworth (May 27 2018 at 14:19):

thanks Nicholas / Mario for the pointers

Last updated: Dec 20 2023 at 11:08 UTC