We've just seen how a lemma can be applied to a proof goal.
Here we'll see how lemmas can be applied to hypotheses too.
Task
Given a natural number $n<5$, show that
$$n \neq 5$$
This is the very same task as the previous post.
Maths
We're going to use the same lemma we used in the previous chapter. For natural numbers $a$ and $b$,
$$a<b\implies a\ne b$$
Previously we considered the proof goal $n\ne5$, and used this lemma to say that proving $n<5$ was a sufficient.
This time we'll consider the hypothesis $n<5$, and say that $n\ne5$ follows directly as a result of that lemma.
The following diagram makes clear this difference. We can see the lemma builds half a bridge from our hypothesis. Do compare it to the diagram from the previous post.
Let's write a proof that applies the lemma to the hypothesis.
$$\begin{align}n&<5&&\text{hypothesis}\tag{1}\label{14.1}\\n&\neq5&&\text{proof objective }\tag{2}\label{14.2}\\&&&\\a<b&\implies a\neq b&&\text{existing lemma}\tag{3}\label{14.3}\\&&&\\n&\ne5&&\text{lemma }(\ref{14.3})\text{ applied to }(\ref{14.1})\tag{4}\label{14.4}\\&&&\\n<5&\implies n\neq5&&\text{by lemma }(\ref{14.3})\tag*{\(\Box\)}\end{align}$$
Again, this may look a little over-done, 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$.
- The lemma's antecedent $a<b$ matches our hypothesis (1), which immediately gives us $n\ne5$.
Code
The following Lean program proves that a natural number $n \ne 5$, given $n < 5$.
-- 14 - Lemma: Not Equal from Less Than
import Mathlib.Tactic
example {n : ℕ} (h : n < 5) : n ≠ 5 := by
apply ne_of_lt at h
exact h
The Lean proof is almost exacty the same as the previous post's proof.
The only difference is the lemma ne_of_lt is pointed at the hypothesis h by adding at h.
This small change is significant. It changes the hypothesis h from h : n < 5 to h : n ≠ 5, as we'll see in the Infoview.
This new hypothesis exactly matches the proof goal, so exact h works just as before to complete the proof.
Infoview
Placing the cursor before apply ne_of_lt at h shows the original hypothesis.
n : ℕ
h : n < 5
⊢ n ≠ 5
Moving the cursor to the beginning of the next line after apply ne_of_lt at h shows the hypothesis has been replaced.
n : ℕ
h : n ≠ 5
⊢ n ≠ 5
Easy Exercise
Write a Lean program to prove $n\ne5$, given $n>5$, where $n$ is a natural number.
Use the same the lemma for “not equal from greater than” you found for the last post's exercise, and apply it to the hypothesis.