Tactic for absurdity

Stream: lean4

[Calvin Lee]

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

[Mario Carneiro]

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]

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]

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