In addition to definitions, like Odd and Even, Mathlib also contains lemmas and theorems we can use.
We'll see how to use a lemma to support a simple disequality proof.
Task
Given a natural number $n<5$, show that
$$n \neq 5$$
The expression $n \ne 5$ is a disequality, whereas the hypothesis n<5 is an inequality.
Maths
It is common knowledge that, given two natural numbers $a$ and $b$, if $a<b$ is true, then we can say $a\ne b$.
That common knowledge might seem too trivial to fuss over, but we'll think of it as a small lemma.
If we can show $n<5$, then we can conclude $n \ne 5$, using that lemma.
Let's write a proof that uses this lemma.
$$\begin{align}n&<5&&\text{hypothesis}\tag{1}\label{13.1}\\n&\neq5&&\text{proof objective }\tag{2}\label{13.2}\\&&&\\a<b&\implies a\neq b&&\text{existing lemma}\tag{3}\label{13.3}\\&&&\\n&<5&&\text{sufficient goal, by lemma }(\ref{13.3})\tag{4}\label{13.4}\\&&&\\n&<5&&\text{using }(\ref{13.1})\tag{5}\label{13.5}\\&&&\\n<5&\implies n\neq5&&\text{by lemma }(\ref{13.3})\tag*{\(\Box\)}\end{align}$$
This may look a little over-cooked, but the small steps will help us write a Lean proof.
We start with the hypothesis $n<5$, and our proof objective $n\ne5$.
We know about a lemma (3) applicable to natural numbers, that if $a<b$ then $a\ne b$. So if we can prove $n<5$ then we can conclude $n\ne5$.
This changes our proof goal from $n\ne5$ to $n<5$.
To prove $n<5$ is easy because we're given it by hypothesis (1]). So $n<5$, and by lemma (3) we finally conclude $n\ne5$.
Code
The following Lean program proves that a natural number $n \ne 5$, given $n < 5$.
-- 13 - Lemma: Not Equal from Less Than
import Mathlib.Tactic
example {n : ℕ} (h: n < 5): n ≠ 5 := by
apply ne_of_lt
exact h
The proof header declares n as a natural number, establishes the hypothesis h: n < 5, and specifies the proof objective n ≠ 5.
The apply instruction applies a lemma or theorem to the current goal, usually resulting in a change in goal.
Here, it applies a lemma named ne_of_lt, which means “not equal from less than”. It allows us to prove the current “not equal” goal by instead proving a “less than” goal.
The Infoview will show that apply ne_of_lt does indeed change the current proof goal from n ≠ 5 to n < 5.
The current goal is now n < 5. We could use apply h to resolve the goal, but since the goal matches exactly the hypothesis h, we can instead use the instruction exact h.
Notice that exact is applying a hypothesis here, not a lemma from Mathlib. The difference is not significant because both hypotheses and lemmas state facts.
We could have used a calc section to prove n < 5 but in this case a multi-line calc section, although familiar, is not warranted.
It may be helpful to correlate this new code back to the maths proof. Here apply ne_of_lt corresponds to line (4) of the maths proof, and exact h corresponds to line (5).
Apply & Exact
We can use apply wherever we use exact. The benefit of exact is that it is stricter than apply.
The hypothesis or lemma must exactly match the current goal, and if a misunderstanding has led to that not being true, it will be exposed immediately.
Infoview
Placing the cursor before apply ne_of_lt shows the original proof goal.
n : ℕ
h : n < 5
⊢ n ≠ 5
Moving the cursor to the beginning of the next line after apply ne_of_lt shows the goal has indeed changed.
n : ℕ
h : n < 5
⊢ n < 5
Lemmas & Theorems
The distinction between what is called a lemma or a theorem in Mathlib is not precise. Ultimately it doesn't matter as both are used in the same way.
Searching for suitable lemmas and theorems in Mathlib is currently not ideal. Many do conform to a naming convention, which helps. The exercise at the end provides a opportunity to practice finding a lemma using the naming convention.
Easy Exercise
Write a Lean program to prove $n\ne5$, given $n>5$, where $n$ is a natural number.
The proof will be almost exactly the same as this chapter's example, except the lemma will be “not equal from greater than”.
Work out the required lemma's Mathlib name fom the naming convention, or search the online Lean documentation to find it.
