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):
Chris Hughes (Aug 11 2018 at 20:16):
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):
introv instead of
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
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