exfalso

Summary

The exfalso tactic changes your goal to false. Why might you want to do that? Usually because at this point you can deduce a contradiction from your hypotheses (for example because you are in the middle of a proof by contradiction).

Examples

If your tactic state is like this:

hP : P
h : P → false
⊢ Q

then this might initially look problematic, because we don’t have any facts about Q to hand. However, false → Q regardless of whether Q is true or false, so and hP and h between them are enough to prove false. So you can solve the goal with

exfalso,
apply h,
exact hP

Warning

Don’t use this tactic unless you can deduce a contradiction from your hypotheses! If your hypotheses are not contradictory then exfalso will leave you with an unsolvable goal.

Details

What is actually happening here is that there’s a theorem in Lean called false.elim which says that for all propositions P, false → P. Under the hood this tactic is just doing apply false.elim, but exfalso is a bit shorter.