## Stream: new members

### Topic: Prove false from not true?

#### Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:37):

Hi, I have an elementary question -- I'm proving something, and am down to having the proved statement "¬true", and the goal is "false". Is there a quick way to finish this?

#### Andrew Ashworth (Oct 05 2018 at 21:38):

are you in term mode or tactic mode?

#### Kenny Lau (Oct 05 2018 at 21:39):

if h : ¬true then exact h trivial

#### Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:39):

Oh ok -- thanks, that works.

#### Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:48):

By the way, is there a statement that automatically proves the goal "true"?

#### Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:49):

I.e. "anything -> true" just like ex falso is "false -> anything"

#### Kenny Lau (Oct 05 2018 at 21:50):

trivial

#### Andrew Ashworth (Oct 05 2018 at 21:52):

as an aside, I think trivial is named weirdly. Why does it exist when true.intro is the canonical name?

#### Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:52):

Thanks. Didn't know that could be used as a standalone statement.

#### Abhimanyu Pallavi Sudhir (Oct 05 2018 at 21:53):

Re:true.intro Doesn't that apply to exfalso too? false.elim having a special name.

#### Andrew Ashworth (Oct 05 2018 at 21:53):

exfalso is an eliminator

#### Andrew Ashworth (Oct 05 2018 at 21:54):

but yes, i also prefer using false.elim ;)

#### Chris Hughes (Oct 05 2018 at 21:58):

My favourite is induction h if h : false

#### Kenny Lau (Oct 05 2018 at 21:59):

my favourite is cases h

#### Charles Rezk (Oct 06 2018 at 00:31):

Where can I get help for installing lean?

#### Bryan Gin-ge Chen (Oct 06 2018 at 00:32):

Feel free to ask in this chat! But we may want to use a different "thread".

#### Charles Rezk (Oct 06 2018 at 00:33):

OK how do I do that?

Last updated: May 06 2021 at 22:13 UTC