Reason from alternatives
cases h with | inl hp | inr hq handles both possibilities.
In this course 2 / 11
h : P ∨ Q says one of the two holds and refuses to say which. To use it you must handle both possibilities, so a proof that consumes a disjunction splits into two.
cases h with creates one branch per constructor: | inl hp => where hp : P, and | inr hq => where hq : Q. The tactics of a branch go on the following lines, indented under the =>. Both branches have to close the same goal.
Inside a branch you know more than you did outside it. In inl you hold a proof of P; in inr a proof of Q. Gaining that knowledge is the whole reason to split.
This is called elimination: the disjunction is consumed by covering its cases, the way obtain consumed a conjunction. Introduction builds a connective, elimination spends one.
Worked example
example (A B : Prop) (h : A ∨ B) : B ∨ A := by
cases h with
| inl ha =>
right
exact ha
| inr hb =>
left
exact hbThe goal here is itself a disjunction, so each branch ends with a choice: knowing A holds, the new goal B ∨ A is proven on the right. Your exercise has a plain goal R instead, and each branch has an implication ready to produce it.
cases h with | inl hp => … | inr hq => … proves a goal from P ∨ Q by covering both possibilities.
Prove R from h : P ∨ Q, using hpr in one branch and hqr in the other.
Suggested steps
- Split on the disjunction
- Handle the inl branch with hpr
- Handle the inr branch with hqr
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