A proof by cases divides a task into separate cases, and proves each one leads to the desired conclusion.
Task
Given the following fact about a real number $x$,
$$(x=3)\lor(x=-3)$$
our task is to show
$$x^{2}=9$$
The symbol $\lor$ means “logical or”. The statement $P \lor Q$ means either $P$ is true, or $Q$ is true, or possibly even both are true.
Statements of the form $P \lor Q$ are called disjunctions.
Maths
Our aim is to show $x^{2}=9$ follows from the hypothesis $(x=3) \lor (x=-3)$.
This hypothesis tells us that either $x=3$ is true, or $x=-3$ is true. We don't know which, so we have to consider both cases, and show the conclusion follows from each case.
The following illustrates this.
Let's write a proof by cases, making clear each step.
$$\begin{align}(x=3)&\lor(x=-3)&&\text{given fact}\tag{1}\label{7.1}\\&&&\\\text{case }x=3&&&\text{using fact }(\ref{7.1})\tag{2}\label{7.2}\\x^{2}&=(3)^{2}&&\text{using case }(\ref{7.2})\\&=9&&\\&&&\\\text{case }x=-3&&&\text{using fact }(\ref{7.1})\tag{3}\label{7.3}\\x^{2}&=(-3)^{2}&&\text{using case }(\ref{7.3})\\&=9&&\\&&&\text{}\\(x=3)\lor(x=-3)&\implies x^{2}=9&&\text{}\tag*{\(\Box\)}\end{align}$$
The given fact (1) splits into two cases, $x=3$ and $x=-3$.- The first case (2) is $x=3$. We want to prove something about $x^{2}$. This case gives us $x^{2}=(3)^{2}$, leading to the conclusion $x^{2}=9$.
- The second case (3) is $x=-3$. This gives us $x^{2}=(-3)^{2}$, also leading to the conclusion $x^{2}=9$.
The two possibilities $x=3$ and $x=-3$ are sufficient to fully cover the hypothesis $(x=3)\lor(x=-3)$. There is no third possibility.
We have shown that, given the hypothesis, $x^{2}$ is indeed always $9$.
Code
The following Lean program proves $x^{2}=9$ follows from $(x=3)\lor(x=-3)$.
-- 07 - Proof by Cases
import Mathlib.Tactic
example {x : ℤ} (h : x = 3 v x = -3) : x^2 = 9 := by
obtain ha | hb := h
· calc
x^2 = (3)^2 := by rw [ha]
_ = 9 := by norm_num
· calc
x^2 = (-3)^2 := by rw [hb]
_ = 9 := by norm_num
The proof header is no different to the ones we've seen before, setting out the variable type, the hypothesis, and the proof objective. The hypothesis is a disjunction, and uses the letter v to denote “logical or”.
The next line is new. The obtain ha | hb := h splits the disjunction hypothesis h into ha and hb. These new hypotheses correspond to the two cases.
The Infoview will show that ha : x = 3 and hb : x = -3.
We now need to show that each case, with ha and hb as hypotheses, leads to the desired conclusion . The two calc sections, one after the other, do exactly this.
In the first calc section, we start with x^2 because that is what we want to prove something about. We use the newly created hypothesis ha : x = 3 to justify x^2 = (3)^2, and then show this is 9 by simple arithmetic.
The second calc section is almost exactly the same, but uses the hypothesis for second case hb : x = -3.
Notice the calc sections have a dot preceding them, · calc. This focussing dot is considered good style when writing sub-proofs within a larger proof. They help us see, at a glance, the structure of the proof. In additional, the Infoview restricts information to the current goal. You can enter the focussing dot by typing \. and your Lean-enabled editor should turn it into a focussing dot.
Infoview
Placing the cursor before obtain shows only one goal, the overall proof goal.
1 goal
x : ℤ
h : x = 3 v x = -3
⊢ x ^ 2 = 9
Moving the cursor after the obtain instruction, just before the first · calc, shows the two sub-goals and their respective hypotheses ha and hb.
2 goals
case inl
x : ℤ
ha : x = 3
⊢ x ^ 2 = 9
case inr
x : ℤ
hb : x = -3
⊢ x ^ 2 = 9
Moving the cursor past the focussing dot, placing it just before calc, shows only the hypothesis relevant to the first case.
1 goal
case inl
x : ℤ
ha : x = 3
⊢ x ^ 2 = 9
Easy Exercise
Write a Lean program to prove $x^{2}-3x+2=0$, given
$$(x=1)\lor(x=2)$$
where $x$ is a real number.
In your proof create two cases $x=1$ and $x=2$ from the given hypothesis $(x=1) \lor (x=2)$.
