simplification of ite

Stream: new members

[Ken Roe]

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]

simp *

[Chris Hughes]

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

[Simon Hudon]

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]

why introv instead of intro or intros?

[Patrick Massot]

I would have done intros a b h

[Simon Hudon]

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]

I didn't know that tactic!

[Simon Hudon]

Pretty neat eh? :)

[Patrick Massot]

what does the v stand for?

[Simon Hudon]

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