16 - Writing Our Own Lemma

Mathlib has many lemmas and theorems for us to use. We can also write our own.

Here we'll create a small but convenient lemma about the natural numbers.

Task

If we pick a natural number $b$, then any other natural number $a$ must be less than or equal to $b$, or greater than or equal to $b+1$. 

The following illustrates this idea.

By the definition of natural numbers, $b+1$ is the successor of $b$, so we can be sure a is not in the “gap” from b to b+1.

Our task is to create a lemma for natural numbers $a$ and $b$ that says

$$\boxed{a\le b\;\lor\;b+1\le a}$$

Let's bring this to life with an example. If we say $b=7$, but leave $a$ unspecified, the lemma tells us that either $a\le7$ or $8\le a$, which makes sense.

Maths

To prove our lemma we'll try to make use of lemmas that also exist in Mathlib, not only to shorten the proof, but also to ease the transition to Lean.

\begin{align}a\le b\;&\lor\;b+1\le a&&\text{proof objective, }a,b\in\mathbb{N}\\&&&\\a\le b\;&\lor\;b<a&&\text{known lemma, }a,b\in\mathbb{N}\tag{1}\label{16.1}\\m+1\le n&\iff m<n&&\text{known lemma, }m,n\in\mathbb{N}\tag{2}\label{16.2}\\&&&\\a\le b\;&\lor\;b+1\le a&&\text{apply lemma }(\ref{16.2})\text{ to }(\ref{16.1})\tag*{\(\Box\)}\end{align}

Lemma (1) is already very close to our proof objective. It says that $a\le b\lor b<a$ for any natural numbers $a$ and $b$. 

Lemma (2) says that $m+1\le n$ is equivalent to $m<n$, for natural numbers $m$ and $n$. It lets us rewrite $b<a$ as $b+1\le a$, which immediately gives us the proof objective.

Both lemmas (1) and (2) exist in Mathlib.

Code

The following Lean code creates a lemma that says either $a\le b$ or $b+1\le a$, for $a,b\in\mathbb{N}$. 

-- 16 - Writing Our Own Lemma

import Mathlib.Tactic

lemma Nat.le_or_succ_le (a b: ℕ): a ≤ b ∨ b + 1 ≤ a := by
  rw [Nat.add_one_le_iff]
  exact le_or_lt a b

example {c : ℕ} :  c ≤ 2 ∨ 3 ≤ c  := by
  exact Nat.le_or_succ_le c 2

The lemma header starts with lemma Nat.le_or_succ_le to tell Lean we want to create a new lemma named Nat.le_or_succ_le. 

The Nat. prefix is conventional for lemmas about natural numbers. The rest of the name le_or_succ_le tries to follow the naming convention to describe what the lemma is about. 

The Lean proofs we've previously explored started with example and no name. They can be thought of as anonymous lemmas, anonymous because there was no need to refer to them after they'd been proved.

The remainder of the header declares a and b as natural numbers, and states the lemma's proposal a ≤ b ∨ b + 1 ≤ a. The round brackets around the variables (a b : ℕ) require anyone using the lemma to always provide a and b as parameters.

Our lemma is proved in just two lines of code by making effective use of existing Mathlib lemmas:

• The first line of the proof rewrites the goal using a Mathlib lemma Nat.add_one_le_iff. Let's see its definition:

• 
  theorem add_one_le_iff : n + 1 ≤ m ↔ n < m :=

The rw tactic is akin to “find and replace”, so it looks at the goal a ≤ b ∨ b + 1 ≤ a and finds b + 1 ≤ a matches the left hand side of the Nat.add_one_le_iff lemma. The matched b + 1 ≤ a is  rewritten with the right hand side of the lemma b < a.

• As we'll see in the Infoview, the goal is now a ≤ b ∨ b < a.
• The final line of the proof applies another Mathlib lemma le_or_lt. Let's look at its definition:

• 
  lemma le_or_lt (a b : α) : a ≤ b ∨ b < a :=
  

  This lemma le_or_lt says that, given two numbers a and b, then a ≤ b ∨ b < a. This matches our current goal exactly, so we can use exact to resolve it and complete the proof.

Notice how the definition of the Mathlib lemma le_or_lt (a b : α) uses round brackets requiring us to provide a and b when we use it.

Infoview

Placing the cursor before rw [Nat.add_one_le_iff] shows the original proof goal.

⊢ a ≤ b ∨ b + 1 ≤ a

Moving the cursor to the start of the next line shows the rewritten goal.

⊢ a ≤ b ∨ b < a

Minimal Example

When writing your own lemmas, it is considerate to provide a minimal example showing how to use them. 

The provided example illustrates how to prove $c\le2\lor3\le c$ for any natural number $c$ using our lemma.  

With a set to c, and b set to 2, our lemma becomes c ≤ 2 ∨ 3 ≤ c. This matches the proof goal exactly, allowing us to use exact to complete the proof in one line.

---

Easy Exercise

Write a lemma for integers $a$ and $b$ that says

$$a\le b\;\lor\;b+1\le a$$

You can copy the provided lemma for natural numbers and modify it to work with integers. 

Create a minimal example illustrating how your lemma can prove the following for any integer $c$.

$$c\le-5\;\lor\;-4\le c$$

15 - Zero Product

Some lemmas are bidirectional implications. To apply them, we need to decide which of the two directions match our task.

Here we'll apply such a lemma to help solve an equation.

Task

Given the zero product

$$(p-1)\cdot(q-2)=0$$

show that

$$p=1\text{ or }q=2$$

where $p$ and $q$ are rational numbers.

Maths

It is common knowledge that the product of two numbers, $a$ and $b$, is zero, if and only if, one or the other is zero. 

We'll think of this as a lemma,

$$a\cdot b=0\iff(a=0)\lor(b=0)$$

A statement of the form $P\iff Q$ is equivalent to both of the following being true:

• $P\implies Q$
• $Q\implies P$

We say “$P$ is true if and only if $Q$ is true” or “$P$ is true iff $Q$ is true.”

So our lemma is equivalent to the following two statements:

• $a\cdot b=0\implies(a=0)\lor(b=0)$
• $(a=0)\lor(b=0)\implies a\cdot b=0$

The antecedent of the first matches our hypothesis $(p-1)\cdot(q-2)=0$, so applying it gives us a disjunction.

$$(p-1=0)\lor(q-2=0)$$

We could conclude $p=1$ or $q=2$ just by looking at this, but to write a Lean proof we'll need to plan out more detail.

$$\begin{align}(p-1)\cdot(q-2)&=0&&\text{hypothesis}\tag{1}\label{15.1}\\&&&\\a\cdot b=0&\iff(a=0)\lor(b=0)&&\text{existing lemma}\tag{2}\label{15.2}\\&&&\\(p-1=0)&\lor(q-2=0)&&\text{apply lemma }(\ref{15.2})\text{ to }(\ref{15.1})\tag{3}\label{15.3}\\&&&\\\text{case }p-1=0&&&\text{using }(\ref{15.3})\\p&=1&&\text{add 1 to both sides}\\&&&\\\text{case }q-2=0&&&\text{using }(\ref{15.3})\\q&=2&&\text{add 2 to both sides}\\&&&\\(p=1)&\lor(q=2)&&\text{conclusion}\tag*{\(\Box\)}\end{align}$$

The key step is applying the lemma (2) to the hypothesis (1) to derive a new intermediate result (3).

This intermediate result is a disjunction $(p-1=0)\lor(q-2=0)$, and so the proof proceeds as a proof by cases.

Code

The following Lean program proves that $p=1$ or $q=2$ given $(p-1)\cdot(q-2)=0$, where $p,q\in\mathbb{Q}$.

-- 15 - Using Lemmas: Multiplied Factors Equal Zero

import Mathlib.Tactic

example {p q : ℚ} (h : (p - 1) * (q - 2) = 0) : p = 1 ∨ q = 2 := by
  apply mul_eq_zero.mp at h
  obtain hp | hq := h
  · left
    linarith
  · right
    linarith

Mathlib has a lemma mul_eq_zero which expresses the idea we want to use, that $a\cdot b=0\iff(a=0)\lor(b=0)$. Let's take a look at its definition.

theorem mul_eq_zero : a * b = 0 ↔ a = 0 ∨ b = 0 :=

The first line of the proof applies mul_eq_zero to hypothesis h, but the lemma name has a .mp appended.

• Adding .mp to a bidirectional lemma selects the forward direction. 
• Adding .mpr to a bidirectional lemma selects the reverse direction.

The mp is “modus ponens”, terminology from the field of logic for the process of reaching a conclusion using an implication.

The Infoview will confirm the hypothesis has been replaced with the equivalent disjunction p - 1 = 0 ∨ q - 2 = 0.

The proof then proceeds as a proof by cases.

• The obtain instruction splits the hypotheses h into two cases, p - 1 = 0 and q - 2 = 0. We then use focussing dots to organise the sub-proofs for each of these cases.
• The first case uses left to state our intention to prove the left side of the disjunctive proof goal, p = 1. The linarith tactic can perform an “add a number to both sides” to justify the goal p = 1 from the current hypotheses, one of which is hp : p - 1 = 0.
• The second case is almost the same, but we use right to state our intention to prove the right side of the disjunctive proof goal, q = 2.

Both cases, p - 1 = 0 and q - 2 = 0, confirm the same disjunctive proof goal, so the proof is complete.

Replacing A Hypothesis?

In the maths proof we derived an intermediate result from the hypothesis, but in the Lean code the hypothesis was replaced.

Mathematically, the original hypothesis (1) always holds. The lemma allows us to derive an equivalent, but more useful, intermediate result (3). Because it is equivalent, we could replace the original hypothesis, but that's not how we write maths proofs.

In the Lean proof, the apply tactic does actually replace the original hypothesis. This is valid only because the new hypothesis is equivalent to the original. If we wanted to preserve the original hypothesis, we could use have to create a new intermediate result.

Infoview

Placing the cursor before apply mul_eq_zero.mp at h shows the original hypothesis.

h : (p - 1) * (q - 2) = 0

Moving the cursor to the beginning of the next line shows the hypothesis has been replaced.

h : p - 1 = 0 ∨ q - 2 = 0

---

Easy Exercise

Write a Lean program to prove $(p-1)\cdot(q-2)\ne0$ given $p-1\ne0$ and $q-2\ne0$, where $p$ and $q$ are rational numbers.

Use the lemma mul_ne_zero_iff. Look up the definition to understand what it says, then decide in which direction to apply it.

14 - Disquality Again

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.

Appendix A - Taxonomy

The following diagram is a simplified hierarchy of the objects in Lean (click to enlarge).

There are two top-level objects called universes, Type and Prop.

• Within the Type universe, there are sets, such as the familiar $\mathbb{N}$, $\mathbb{Z}$ and $\mathbb{R}$. Each of these sets has elements, such as 13.

• Within the Prop universe, there are propositions, such as Odd 13. Some of these propositions may have proofs. 

Under the top level universes, the second level objects are called types. The third level objects are called terms.

Unsurprising Example

When we write 13 : ℕ, we mean “13, the element of the set of natural numbers ℕ”. 

Using the terminology of Lean, 13 is a term of type ℕ.

Surprising Example

When we write h : Odd 13, we mean “h, the proof of the proposition Odd 13”. 

The proposition Odd 13 is a type, and proofs like h or by use 6; norm_num could be terms of this type. Rest assured, many people find this odd to begin with.

It may also seem surprising that h is a proof, because we've mostly talked about h as a hypothesis. When we use a hypothesis in a Lean proof, we are actually using the proof of a proposition.

13 - Disquality

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 is,

$$a<b\implies a\ne b$$

That common knowledge might seem too trivial to fuss over, but we'll think of it as a small lemma.

Looking at that lemma, we can see the conclusion $a\ne b$ matches our own proof objective $n\ne5$. So, if we can show $n<5$, then we can conclude $n \ne 5$, using that lemma.

The following diagram illustrates how this lemma builds half a bridge to our proof objective.

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$. 
• The lemma's conclusion matches our proof objective, 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 an 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.

12 - Odd & Even

In Part III we'll practise using lemmas and definitions in our proofs. 

There is a huge body of commonly agreed knowledge that mathematicians refer to in their own proofs. A large, and ever-growing, number of these lemmas, theorems, and definitions are encoded in the Mathlib library, ready for us to use in our own Lean proofs. 

We'll start by using the definition of an odd number.

Task

Show the integer 13 is odd.

Maths

To show 13 is odd, we need to show it meets the definition of odd.

An odd integer is of the form $2k+1$, where $k$ is an integer. 

In more mathematical phrasing; if there exists an integer $k$ such that $n=2k+1$, then $n$ is odd.

The task has become an existence proof. If we can find an integer $k$ such that $13=2k+1$, then we have shown 13 is odd.

Let's write out a step by step proof.

$$\begin{align}13&\text{ is odd}&&\text{proof objective }\\&&&\\\exists k\in\mathbb{Z}[n=2k+1]&\implies n\text{ is odd}&&\text{definition of odd}\tag{1}\label{12.1}\\&&&\\\exists k\in\mathbb{Z}[13=2k+1]&&&\text{sufficient goal, using }(\ref{12.1})\\&&&\\\text{use }k=6&&&\text{chosen example}\tag{2}\label{12.2}\\13&=2(6)+1&&\text{using }(\ref{12.2})\\&&&\\13=2(6)+1&\implies13\text{ is odd}&&\text{by definition }(\ref{12.1})\tag*{\(\Box\)}\end{align}$$

This may look a little laborious, but the detail will help us develop a Lean proof. . 

We start with the proof objective, to show $13$ is odd.

We then state the definition, that $n$ is odd if it can be written in the form $2k+1$, where $k$ is an integer. 

So, to show $13$ is odd, it is sufficient to show it can be written in the form $2k+1$. This gives us a new goal, to show there exists an integer $k$ such that $13=2k+1$.

We choose $k=6$, and confirm that $13=2(6)+1$. 

We have shown that $13$ can indeed be written in the form $2k+1$. And so, by the definition of odd, we have finally shown that $13$ is odd.

Code

The following Lean program proves the integer 13 is odd.

-- 12 - Definition: Odd Number

import Mathlib.Tactic

example : Odd (13: ℤ)  := by
  dsimp [Odd]
  use 6
  norm_num

The proof objective states that 13 is Odd. 

If we had simply written Odd 13 as the proof objective, 13 would be interpreted, by default, as a natural number. We write (13: ℤ) to specify 13 as an integer.

The idea of Odd is defined in Mathlib. The next line dsimp [Odd] expands that definition in the Infoview so we can see what it actually is. We'll see below the goal changes from being displayed as Odd 13, to ∃ k, 13 = 2 * k + 1, which we recognise as the definition of odd applied to 13.

The instruction dsimp has no effect on the proof itself. It only changes how Odd is displayed in the Infoview. 

After this point, the proof proceeds as a simple existence proof. 

The instruction use 6 tells Lean we want to try 6 for k. This changes the goal to 13 = 2 * 6 + 1. We resolve this goal by arithmetic, using the norm_num tactic. For such a simple and clear goal, there is no need for a multi-line calc section.

What is Odd?

The proof objective was written as Odd (13: ℤ). The intention is for this to be a statement saying 13 is an odd number.

How does this work?

The idea of Odd is defined in Mathlib as a function. A definition is distinct from a lemma, and Mathlib contains many of both. A lemma needs to be justified by proof, but a definition does not.

That function Odd takes one parameter, and outputs a proposition involving that parameter, which may or may not be true.

When applied to 13, the output is a proposition  ∃k such that 13 = 2*k + 1. This proposition is true because we can prove it.

If we applied Odd to 14, the output is a proposition ∃k such that 14 = 2*k + 1. This proposition is not true because there is no proof for it.

It is interesting to see the actual definition of Odd inside Mathlib:

def Odd (a : α) : Prop := ∃ k, a = 2 * k + 1

We can see how a is mapped to a proposition about a.

Infoview

The Infoview is particularly useful when working with definitions and existence proofs.

Placing the cursor before dsimp [Odd] shows the original proof goal.

⊢ Odd 13

Moving the cursor to the end of the line after dsimp [Odd] shows the goal is now displayed using the definition of Odd.

⊢ ∃ k, 13 = 2 * k + 1

Placing the cursor after use 6 shows the goal is now specific to k = 6.

⊢ ∃ k, 13 = 2 * 6 + 1

---

Easy Exercise

Write a Lean program to prove the integer 14 is even.

Your proof should use Mathlib's definition Even for even numbers. Use dsimp to see how the definition is applied to 14.

11 - Existence

The aim of an existence proof is simply to show something exists. 

Task

Show there exists a natural number n, such that

$$n^{2}+1=10$$

You may see this written in mathematical notation, where the symbol \exists  means “there exists”.

$$\exists n\in\mathbb{N}\;[n^{2}+1=10]$$

The essence of an existence proof is to demonstrate an object exists that satisfies any given conditions. Calculating, deriving, or even guessing, what that object is, is not the central point.

Maths

For our task, intuition tells us that $n$ can't be larger than $10$, and after some mental trial and error we find that $n=3$ works. We have found our example.

We don't need to justify how we arrived at our example. We only need to show it satisfies the condition $n^{2}+1=10$.

Let's write a proof, making clear each step. 

$$\begin{align}\exists n\in\mathbb{N}&[n^{2}+1=10]&&\text{proof objective}\\&&&\\\text{use }n=3&&&\text{chosen example}\tag{1}\label{11.1}\\n^{2}+1&=(3)^{2}+1&&\text{using }(\ref{11.1})\\&=10&&\text{by arithmetic }\tag*{\(\Box\)}\end{align}$$

We first state the proof objective, which includes the condition $n^{2}+1=10$ any example must meet.

We then choose $n=3$, and show by arithmetic that indeed $n^{2}+1=10$. 

Code

The following Lean program proves there exists a natural number $n$ such that $n^{2}+1=10$.

-- 11 - Existence proof

import Mathlib.Tactic

example : ∃ n: ℕ, n^2 + 1 = 10 := by
  use 3
  calc
    3^2 + 1 = 10 := by norm_num

The proof header is a little different from the ones we've looked at recently. Here there is no separate definition of variable types, and no hypothesis. The entire theorem is in the proof objective. 

The proof objective ∃ n: ℕ, n^2 + 1 = 10 says that there exists a natural number n, such that n^2 + 1 = 10.

The next step is to choose an example that meets this condition. The instruction use 3 tells Lean that we propose 3 as that example.

The infoview will confirm that use 3 changes the proof goal from ∃ n, n^2 + 1 = 10 to 3^2 + 1 = 10.

We can use a simple calc section to show by arithmetic that 3^2 + 1 is indeed 10.

Bad Example

Let's see what happens if we choose a bad example, say $n=4$. This means changing the code to use 4.

Placing the cursor after use 4 shows the proof goal.

⊢ 4 ^ 2 + 1 = 10

This goal is impossible to prove, because $17$ is not $10$.

Simpler Code

The following is a shorter version of our Lean program.

-- 11 - Existence proof

import Mathlib.Tactic

example : ∃ n: ℕ, n^2 + 1 = 10 := by
  use 3
  norm_num

The goal at the point of the previous calc section was ⊢ 3^2 + 1 = 10. This is simple enough to apply the norm_num tactic to prove. It doesn't really need a calc section, which is better suited to derivations that require several steps.

As with all programming, it is better to be clear and unambiguous than overly concise. This use of one-line tactics should only be done when the context is simple and clear for anyone reading your code, including your future self.

---

Easy Exercise

Write a Lean program to prove there exists a natural number greater than $5$.

In mathematical notation, the proof objective is as follows, and should translate into Lean code fairly directly.

$$\exists n\in\mathbb{N}\;[n>5]$$

As an optional extra challenge, try writing the proof in the concise form shown above.