From a contradiction, anything
exfalso and absurd let a contradiction prove any goal.
In this course 4 / 11
From False, anything follows. Lean states this as False.elim : False → C for any proposition C. The rule is sound precisely because False has no proofs, so it can never be used on a real one.
exfalso turns whatever goal you have into False. Reach for it when the goal has nothing to do with your hypotheses and the hypotheses contradict each other. After exfalso the goal is ⊢ False, and the previous lesson takes over.
absurd hp hnp does both steps at once: given a proof and its negation it produces a proof of any proposition. The worked example uses it to conclude something plainly false about a number, which is legitimate, because the assumptions it was handed can never both hold.
Prefer exfalso when you want the shape of the argument visible in the proof, and absurd when the contradiction is already sitting in front of you.
Worked example
example (n : Nat) (h : n = 3) (hn : ¬ (n = 3)) : n = 100 := by
exact absurd h hnThe conclusion is false for almost every n, and the proof is still correct: the two hypotheses cannot both hold, so the theorem never applies to anything. Your exercise proves an abstract Q the same way, but with the two steps written out.
Contradictory hypotheses prove any goal: exfalso then derive False, or absurd hp hnp in one move.
Prove Q from the contradictory hypotheses hp and hnp.
Suggested steps
- Replace the goal by False, or use absurd directly
- Derive the contradiction from hp and hnp
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct