Prove false from not true?

Stream: new members

[Abhimanyu Pallavi Sudhir]

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]

are you in term mode or tactic mode?

[Kenny Lau]

if h : ¬true then exact h trivial

[Abhimanyu Pallavi Sudhir]

Oh ok -- thanks, that works.

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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

[Kenny Lau]

trivial

[Andrew Ashworth]

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

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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

[Andrew Ashworth]

exfalso is an eliminator

[Andrew Ashworth]

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

[Chris Hughes]

My favourite is induction h if h : false

[Kenny Lau]

my favourite is cases h

[Charles Rezk]

Where can I get help for installing lean?

[Bryan Gin-ge Chen]

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

[Charles Rezk]

OK how do I do that?