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 -- goal now `False`
apply h -- goal now `P`
exact hP -- goal solved

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.