## Stream: lean4

### Topic: Tactic for absurdity

#### Calvin Lee (Feb 26 2021 at 00:11):

Are there any tactics for showing absurdity? I find my self often doing exact _ where _  is some witness of falsehood

#### Mario Carneiro (Feb 26 2021 at 00:28):

What's wrong with exact? If you have a proof term already then that's the most straightforward option even in lean 3

#### Mario Carneiro (Feb 26 2021 at 00:28):

if your goal is not literally False but your proof term is then I will sometimes use cases e instead of exact false.rec e

#### Mario Carneiro (Feb 26 2021 at 00:29):

If you are referring specifically to the lean 3 contradiction tactic, I would expect that doesn't exist but it is a pretty simple tactic that can go in the mathlib prelude

Last updated: May 07 2021 at 13:21 UTC