## Stream: new members

### Topic: simplification of ite

#### Ken Roe (Aug 11 2018 at 20:09):

How do I complete the following theorem:

theorem th : ∀ (a:ℕ) (b:ℕ), a ≠ b → (if a=b then 5 else 3)=3 :=
begin
intros, ...
end


#### Simon Hudon (Aug 11 2018 at 20:12):

simp *

#### Chris Hughes (Aug 11 2018 at 20:16):

Also rw if_neg h if h is your proof of a \ne b

#### Simon Hudon (Aug 11 2018 at 20:17):

For @Chris Hughes 's solution, you might make it clearer as introv h, rw if_neg h. As a habit, you should avoid referring to auto generated variable names.

#### Patrick Massot (Aug 11 2018 at 20:19):

why introv instead of intro or intros?

#### Patrick Massot (Aug 11 2018 at 20:20):

I would have done intros a b h

#### Simon Hudon (Aug 11 2018 at 20:21):

Because the two natural numbers already have a name and we can just keep them. The assumption however is anonymous in the statement and you should rely on the name given under the hood. Additionally, we don't refer to a and b in the proof so renaming them is not very useful.

#### Patrick Massot (Aug 11 2018 at 20:22):

I didn't know that tactic!

#### Simon Hudon (Aug 11 2018 at 20:22):

Pretty neat eh? :)

#### Patrick Massot (Aug 11 2018 at 20:23):

what does the v stand for?

#### Simon Hudon (Aug 11 2018 at 20:23):

Btw @Ken Roe, feel free to migrate your questioning to the general stream of Zulip. new members is more for introductions I believe.

Last updated: May 14 2021 at 11:10 UTC