# 2. Proofs with structure

The proofs by calculation of Chapter 1 were all, from a certain point of view, one-step proofs. In this chapter we gradually introduce the ingredients for multi-step proofs. These include establishing “intermediate” facts which get referred back to later, invoking named lemmas previously proved by yourself or other people, and taking apart complicated mathematical statements which have been built up from simpler ones using the logical symbols \(\lor\), \(\land\) and \(\exists\).

This chapter also introduces the key interactivity feature of the Lean language:
the live-updating *infoview* keeping track of your current hypotheses and goals.

The work of this chapter continues (after a break) in Chapter 4.

## 2.1. Intermediate steps

### 2.1.1. Example

Every proof we’ve seen so far has been a single calculation. More typically, though, a proof will have a more complex structure, with facts established at an early stage which are not used immediately, but instead brought in later.

For example, here’s the algebra problem from Example 1.3.3.

Problem

Let \(a\) and \(b\) be real numbers and suppose that \(a-5b=4\) and \(b+2=3\). Show that \(a=9\).

We previously solved it by a single long calculation,

But another way to express the solution – maybe more natural, and closer to how you might have learned to solve it in high school – is to first solve for \(b\), and then substitute that in to help solve for \(a\).

Solution

Since \(b+2=3\), we have \(b=1\). Therefore

This is the first time we have seen a proof with words. The sentence

Since \(b+2=3\), we have \(b=1\).

is a use of the reasoning discussed in Section 1.5: The fact \(b=1\) is deduced from the hypothesis \(b+2=3\) by mentally subtracting 2 from both sides, and this is considered sufficiently obvious that we don’t explain the reasoning apart from indicating which of the hypotheses is being invoked.

We have now added one more fact, \(b=1\), to our list of known facts in this problem, and we carry out a calculational proof in which this fact is used (it is substituted, together with \(a-5b=4\), at the step \((a - 5b) + 5b = 4 + 5 \cdot 1\)). The word “Therefore” (synonyms: “Thus”, “So”) introduces this calculational proof; its meaning is that the fact just proved will be used in the reasoning which follows.

Here is how this argument looks in Lean. We state \(b=1\) with the keyword `have hb`

. This is
immediately followed by the reasoning to justify this fact: adding/subtracting something from the
hypothesis \(b+2=3\), which in this problem is named `h2`

. Then we give a calculational
proof as usual, in which the fact \(b=1\) (under the name `hb`

) gets used at some point.

```
example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 := by
have hb : b = 1 := by addarith [h2]
calc
a = a - 5 * b + 5 * b := by ring
_ = 4 + 5 * 1 := by rw [h1, hb]
_ = 9 := by ring
```

It’s not so hard to understand this proof step by step by reading the Lean code. But Lean actually
provides a powerful tool to help us understand multi-step proofs: the *Lean Infoview* window, which
we will now use for the first time. Let’s walk through what the infoview can tell us as we work
through this problem.

Put your cursor at the start of the line

have hb : b = 1

and look at the Lean Infoview window. We see this:

a b : ℝ h1 : a - 5 * b = 4 h2 : b + 2 = 3 ⊢ a = 9

This is simply a vertically-displayed version of the problem we started with:

example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 :=

It lists all the variables and hypotheses given to us in the problem, and, next to the symbol

`⊢`

, it displays our*goal*: to show`a = 9`

.Next, move your cursor to the start of the lines

calc a = (a - 5 * b) + 5 * b := by ring

The newly-proved fact

`hb`

, that`b = 1`

, has been added to the list of hypotheses in the infoview.a b : ℝ h1 : a - 5 * b = 4 h2 : b + 2 = 3 hb : b = 1 ⊢ a = 9

Finally, move your cursor to the start of the line below the last line of code,

_ = 9 := by ring

The infoview now displays no tasks for us. Instead it displays the message

No goals

which serves as a visual confirmation that the

`calc`

block solved the goal, thus completing the problem.

### 2.1.2. Example

Here’s another example of reasoning in which we establish an intermediate statement before the main proof.

Problem

Let \(m\) and \(n\) be integers, and suppose that \(m+3\le 2n-1\) and \(n\le 5\). Show that \(m\le 6\).

Solution

We have that

so \(m \le 6\).

Here, the intermediate step is the fact \(m+3\le 9\). This can be read off by looking at the calculational proof following the text

We have that

The top left expression in the calculation is \(m+3\), the bottom right expression is \(9\), and the sequence of relations \(\le\), \(\le\), \(=\) at the steps in between together establish the relation \(\le\) between \(m+3\) and \(9\).

We discussed in Example 2.1.1 the meaning of “therefore”/”thus”/”so”. Here the text

so \(m \le 6\).

tells us that the fact just proved (\(m+3\le 9\)) implies that \(m \le 6\), by a proof which is too straightforward to require further details; in this case it’s another example of the add/subtract-from-both-sides reasoning discussed in Section 1.5.

Here is the same proof in Lean. A calculation block which is being used to establish an
intermediate step is introduced and named by `have`

:

```
example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by
have h3 :=
calc
m + 3 ≤ 2 * n - 1 := by rel [h1]
_ ≤ 2 * 5 - 1 := by rel [h2]
_ = 9 := by numbers
addarith [h3]
```

Notice that, right at the beginning of the final line

```
addarith [h3]
```

the goal state (as displayed in the infoview) is

```
m n : ℤ
h1 : m + 3 ≤ 2 * n - 1
h2 : n ≤ 5
h3 : m + 3 ≤ 9
⊢ m ≤ 6
```

The fact \(m + 3 ≤ 9\), which was established by the calc block and given the name `h3`

, is
now available as an additional fact to use in future steps, and indeed it is used in the next step
(`addarith [h3]`

).

### 2.1.3. Example

Let’s redo another example, this time Example 1.4.2. The problem was:

Problem

Let \(r\) and \(s\) be rational numbers, and suppose that \(s+3\geq r\) and \(s+r \leq 3\). Show that \(r\leq 3\).

We did it before by a single, clever, calculation, but the following solution, though longer, might be easier to come up with.

Solution

From \(s + 3 \geq r\) we have \(r \leq 3 + s\), and from \(s + r \leq 3\) we have \(r \leq 3 - s\). Therefore

There are two intermediate steps in this problem: proving that \(r \leq 3 + s\) and that \(r \leq 3 - s\).

Exercise: Here is a Lean setup for this problem, with the stated intermediate intermediate steps (not yet justified), and the outline of the stated calculational proof as the final step. Fill in all the sorries. Also, try to predict what the infoview will display at each position in the proof, and then compare your prediction with reality.

```
example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 := by
have h3 : r ≤ 3 + s := by sorry -- justify with one tactic
have h4 : r ≤ 3 - s := by sorry -- justify with one tactic
calc
r = (r + r) / 2 := by sorry -- justify with one tactic
_ ≤ (3 - s + (3 + s)) / 2 := by sorry -- justify with one tactic
_ = 3 := by sorry -- justify with one tactic
```

### 2.1.4. Example

The next problem features a new form of reasoning.

Problem

Let \(t\) be a real number, and suppose that \(t^2=3t\) and \(t \geq 1\). Show that in fact \(t\geq 2\).

Solution

We have that

so \(t=3\). Thus \(t\geq 2\).

The first step of this proof is a calculation establishing the intermediate statement \(t\cdot t=3t\). Then, with the phrase

so \(t=3\)

we establish another intermediate statement, \(t=3\), by cancelling \(t\) from the left and right sides of \(t\cdot t=3t\). Finally, we deduce the goal, \(t=3\).

In Lean, cancellation reasoning is done with the `cancel`

tactic. In the proof below, you will
see that before the line `cancel t at h3`

the goal state contains the hypothesis

```
h3 : t * t = 3 * t
```

and after that line it has been modified to

```
h3 : t = 3
```

Here is the full proof in Lean.

```
example {t : ℝ} (h1 : t ^ 2 = 3 * t) (h2 : t ≥ 1) : t ≥ 2 := by
have h3 :=
calc t * t = t ^ 2 := by ring
_ = 3 * t := by rw [h1]
cancel t at h3
addarith [h3]
```

There is a mathematical subtlety here. You can only cancel a common factor from both
sides of an equation if that common factor is known to be nonzero. In this problem, Lean can deduce
that the common factor, `t`

, is nonzero. Why?

### 2.1.5. Example

Here’s another problem in which we establish an intermediate fact and then simplify it.

Problem

Let \(a\) and \(b\) be real numbers, and suppose that \(a ^ 2 = b ^ 2 + 1\) and that \(a\) is nonnegative. Show that \(a \geq 1\).

Solution

We have that

so \(a\geq 1\).

The deduction from \(a ^ 2 \geq 1 ^ 2\) that \(a \geq 1\) is again something that the
`cancel`

tactic can do. Notice that Lean is silently checking the condition for this to be
valid (that \(a\geq 0\)). Check that if you delete the hypothesis `h2 : a ≥ 0`

then the
cancellation step fails in Lean.

```
example {a b : ℝ} (h1 : a ^ 2 = b ^ 2 + 1) (h2 : a ≥ 0) : a ≥ 1 := by
have h3 :=
calc
a ^ 2 = b ^ 2 + 1 := by rw [h1]
_ ≥ 1 := by extra
_ = 1 ^ 2 := by ring
cancel 2 at h3
```

### 2.1.6. Example

We conclude the section with some exercises translating prose proofs into Lean proofs. The difficult part with these problems is to pick out, from the text, what the intermediate statements are.

First, we redo one more example, this time Example 1.4.1. The problem was:

Problem

Let \(x\) and \(y\) be integers, and suppose that \(x + 3 \le 2\) and \(y + 2x\geq 3\). Show that \(y>3\).

Here is a solution which uses an intermediate step.

Solution

Since \(x + 3 \le 2\), we have \(x \leq -1\). So

Exercise: Identify the intermediate step, and express this solution in Lean.

```
example {x y : ℤ} (hx : x + 3 ≤ 2) (hy : y + 2 * x ≥ 3) : y > 3 := by
sorry
```

### 2.1.7. Example

This next one is mathematically a little harder.

Problem

Let \(a\) and \(b\) be real numbers and suppose that \(-b \le a \le b\). Show that \(a ^ 2 \le b ^ 2\).

Solution

By the first part of the hypothesis, \(0 \le b + a\), and by the second part of the hypothesis, \(0 \le b - a\).

Therefore \((b + a)(b - a)\) is nonnegative, so

Exercise: Identify the two intermediate steps, and express this solution in Lean. (Note that Lean is a little more powerful here than the human reader: you do not need to give any Lean translation of the step

Therefore \((b + a)(b - a)\) is nonnegative,

instead Lean will figure this out by itself at the point where this is needed.)

```
example (a b : ℝ) (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2 := by
sorry
```

### 2.1.8. Example

Problem

Let \(a\) and \(b\) be real numbers and suppose that \(a \le b\). Show that \(a ^ 3 \le b ^ 3\).

Notice that we are not assuming that \(a\) and \(b\) be positive, so our easier tricks for the behaviour of inequalities under multiplication/powers do not apply.

Solution

Since \(a \le b\), we have \(0 \le b - a\).

Therefore \(\frac{(b - a)\left[(b - a)^2+3(b+a)^2\right]}{4}\) is nonnegative, so

Exercise: Identify the intermediate step, and express this solution in Lean.

```
example (a b : ℝ) (h : a ≤ b) : a ^ 3 ≤ b ^ 3 := by
sorry
```

### 2.1.9. Exercises

Let \(x\) be a rational number whose square is 4, and which is greater than 1. Show that \(x=2\).

Suggested steps: Prove that \(x(x+2)=2(x+2)\), then cancel to deduce that \(x=2\).

example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by sorry

Let \(n\) be an integer satisfying \(n^2+4=4n\). Prove that \(n=2\).

Suggested steps: Prove that \((n-2)^2=0\), cancel the square to deduce that \(n-2=0\), then finish off.

example {n : ℤ} (hn : n ^ 2 + 4 = 4 * n) : n = 2 := by sorry

Let \(x\) and \(y\) be rational numbers, and suppose that \(xy=1\) and \(x \ge 1\). Show that \(y \le 1\).

Suggested steps: Prove that \(0<xy\), cancel \(x\) to deduce that \(0<y\), then give a calculation to prove the goal.

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by sorry

## 2.2. Invoking lemmas

### 2.2.1. Example

Here’s a style of problem we haven’t seen before, in which the goal is a *disequality*,
\(x\ne 1\), rather than an equality (\(=\)) or inequality (\(\le\), \(<\),
\(\ge\), \(>\)).

Problem

Let \(x\) be a rational number, and suppose that \(3x=2\). Show that \(x\ne 1\).

Solution

It suffices to prove that \(x< 1\). Indeed,

What happened in this problem? We used a piece of “general knowledge”, that if one number is
strictly smaller than another then they can’t be the same. Or at least, this feels like general
knowledge – just common sense! – but really it is a *lemma*: a fact that has been proved already
1
by us or someone else, and which we are allowed to invoke in our proof.

When working in Lean, if we want to invoke a lemma in this way, we need to call it out by name.
Someone earlier, in the big Lean mathematical library, has proved this fact and named it
`ne_of_lt`

: 2

```
lemma ne_of_lt {a b : ℚ} (h : a < b) : a ≠ b :=
```

We can invoke this lemma in our problem using the Lean `apply`

tactic. At the start of our work
on the problem,

```
example {x : ℚ} (hx : 3 * x = 2) : x ≠ 1 := by
```

our goal state looks like this:

```
x : ℚ
hx : 3 * x = 2
⊢ x ≠ 1
```

When we `apply`

the lemma, with our cursor at the end of this line,

```
example {x : ℚ} (hx : 3 * x = 2) : x ≠ 1 := by
apply ne_of_lt
```

the goal state has changed to this:

```
x : ℚ
hx : 3 * x = 2
⊢ x < 1
```

So `apply ne_of_lt`

changes (only) the goal: it transforms the goal `x ≠ 1`

into the goal
`x < 1`

, which we can then solve by our usual methods for inequalities.

```
example {x : ℚ} (hx : 3 * x = 2) : x ≠ 1 := by
apply ne_of_lt
calc
x = 3 * x / 3 := by ring
_ = 2 / 3 := by rw [hx]
_ < 1 := by numbers
```

Comparing the text proof and the Lean proof, you will notice that the phrasing in invoking the lemma is rather different. In text, I said,

It suffices to prove that \(x< 1\). Indeed, ….

That is, I effectively stated what the new goal would be, and left the reader to figure out what piece of general knowledge I used to make this change to the goal. In Lean, I don’t need to state what the new goal is, because my reader can find this out for herself by inspecting the goal state. But I do need to explicitly mention the name of the lemma,

```
apply ne_of_lt
```

because “it’s general knowledge!” is not a precise enough justification for Lean to find it.

### 2.2.2. Example

Here’s a similar problem, in which I will prove a disequality by showing the left-hand side is
*larger*, rather than (as in the previous problem) *smaller*.

Problem

Let \(y\) be a real number. Show that \(y ^ 2 + 1\ne 0\).

Solution

It suffices to prove that \(0 < y ^ 2 + 1\), which is clear since squares are nonnegative.

Exercise: Express the solution to this problem in Lean.

```
example {y : ℝ} : y ^ 2 + 1 ≠ 0 := by
sorry
```

Use the lemma `ne_of_gt`

:

```
lemma ne_of_gt {a b : ℝ} (h : a > b) : a ≠ b :=
```

### 2.2.3. Example

Problem

Let \(a\) and \(b\) be real numbers, and suppose that \(a^2+b^2=0\). Show that \(a ^ 2 = 0\).

Solution

It suffices to prove that both \(a ^ 2 \le 0\) and \(a ^ 2 ≥ 0\). The second is clear since squares are nonnegative. For the first,

In Lean use this lemma, the “antisymmetry of the \(\le\) relation”:

```
lemma le_antisymm {a b : α} (h1 : a ≤ b) (h2 : b ≤ a) : a = b :=
```

Here is the full proof in Lean.

```
example {a b : ℝ} (h1 : a ^ 2 + b ^ 2 = 0) : a ^ 2 = 0 := by
apply le_antisymm
calc
a ^ 2 ≤ a ^ 2 + b ^ 2 := by extra
_ = 0 := h1
extra
```

Notice that after applying the lemma, the infoview shows *two* goals!

```
2 goals
a b : ℝ
h1 : a ^ 2 + b ^ 2 = 0
⊢ a ^ 2 ≤ 0
a b : ℝ
h1 : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ a ^ 2
```

This mathematically is not surprising, since the lemma had two preconditions, both of which we need to justify. Anyway, having multiple goals is perfectly possible in Lean – there can be many goals at any one time, and the mechanism is simply that any code you write acts on the first goal on the list (until it’s resolved, then work starts on the second goal, etc).

### 2.2.4. Exercises

Let \(m\) be an integer for which \(m + 1=5\). Show that \(3m\ne 6\).

You may wish to use the fact that two numbers are not equal if the first is greater than the second (you’ll need the lemma

`ne_of_gt`

, as in Example 2.2.2).example {m : ℤ} (hm : m + 1 = 5) : 3 * m ≠ 6 := by sorry

Let \(s\) be a rational number for which \(3s ≤ -6\) and \(2s \ge -4\). Show that \(s=-2\).

You will probably use the lemma

`le_antisymm`

, stating if \(x\le y\) and \(x\ge y\) then \(x = y\).example {s : ℚ} (h1 : 3 * s ≤ -6) (h2 : 2 * s ≥ -4) : s = -2 := by sorry

Footnotes

- 1
In this case, as a consequence of the definition of the relation \(<\) on the rational numbers.

- 2
Here

`ne`

stands for “not equal”,`lt`

stands for “less than”, and the`of`

means that we are deducing a`ne`

statement from a`lt`

statement. The standard Lean mathematical library has many such naming conventions, but you don’t need to follow them; you can call your own lemmas`foo`

and`banana`

if you like.

## 2.3. “Or” and proof by cases

### 2.3.1. Example

In mathematics, the word “or” (denoted \(\lor\) as a logical symbol) can connect two statements. For example, here is a problem in which the hypothesis is an “or”-statement.

Problem

Let \(x\) and \(y\) be real numbers and suppose that either \(x=1\) or \(y=-1\). Show that \(xy+x=y + 1\).

The hypothesis

\(x=1\) or \(y=-1\)

tells us that at least one of the alternatives \(x=1\), \(y=-1\) must occur (and possibly
both, but this needs no special consideration). So a solution to this problem simply involves
considering these two alternatives in turn. This is called a *proof by cases*.

Solution

If \(x=1\), then

and if \(y=-1\) then

In Lean, an “or”-statement is represented using the logical symbol `∨`

. At the start of
this problem, the infoview displays one task, with `h`

as the “or”-statement hypothesis, and the
goal as proving that \(xy+x=y + 1\).

```
x y : ℝ
h : x = 1 ∨ y = -1
⊢ x * y + x = y + 1
```

To consider in turn the two cases represented by an “or”-statement, we use the tactic `obtain`

.
After applying this tactic, the infoview now displays two simpler tasks. The goal in each task is
still to prove that \(xy+x=y + 1\), but the hypothesis has changed: to the left alternative,
`x = 1`

, in the first task, and to the right alternative, `y = -1`

, in the second task.

```
x y : ℝ
hx : x = 1
⊢ x * y + x = y + 1
x y : ℝ
hy : y = -1
⊢ x * y + x = y + 1
```

We can then solve these simpler tasks one by one, giving a calculational proof of each.

```
example {x y : ℝ} (h : x = 1 ∨ y = -1) : x * y + x = y + 1 := by
obtain hx | hy := h
calc
x * y + x = 1 * y + 1 := by rw [hx]
_ = y + 1 := by ring
calc
x * y + x = x * -1 + x := by rw [hy]
_ = -1 + 1 := by ring
_ = y + 1 := by rw [hy]
```

### 2.3.2. Example

More commonly, you will give a proof by cases for a problem in which there is no hypothesis directly structured as an “or”-statement. Instead, you will create such a hypothesis yourself, by setting up and proving an intermediate statement which is an “or”-statement.

Problem

Let \(n\) be any natural number. Show that \(n ^ 2 \ne 2\).

In this problem, we will case-split on the “or”-statement

\(n \le 1\) or \(2 \le n\).

On paper this can be stated without a proof, although really it comes as the application of a lemma about the natural numbers: in general, either \(n\) is less than or equal to one natural number or it’s greater than or equal to the next one. The solution to the problem is easy after this case-split.

Solution

We consider separately the cases \(n \le 1\) and \(2 \le n\).

**Case 1** (\(n \le 1\)): It suffices to prove that \(n ^ 2 < 2\). Indeed,

**Case 2** (\(2 \le n\)): It suffices to prove that \(n ^ 2 > 2\). Indeed,

In Lean, we set up this “or”-statement explicitly as an intermediate fact, the application of a lemma,

```
lemma le_or_succ_le (a b : ℕ) : a ≤ b ∨ b + 1 ≤ a :=
```

We have not previously invoked lemmas in this way. The syntax uses `have`

,

```
have hn := le_or_succ_le n 1
```

and after this line of code, the infoview displays the or-statement we want:

```
hn : n ≤ 1 ∨ 2 ≤ n
```

After establishing the intermediate fact, we case-split on that fact, and are left with two tasks corresponding to the two cases:

```
n : ℕ
hn : n ≤ 1
⊢ n ^ 2 ≠ 2
n : ℕ
hn : 2 ≤ n
⊢ n ^ 2 ≠ 2
```

Exercise: The first case has been written up in Lean. Fill in the details of the second case.

```
example {n : ℕ} : n ^ 2 ≠ 2 := by
have hn := le_or_succ_le n 1
obtain hn | hn := hn
apply ne_of_lt
calc
n ^ 2 ≤ 1 ^ 2 := by rel [hn]
_ < 2 := by numbers
sorry
```

### 2.3.3. Example

So far we have discussed how to deal with an “or”-statement appearing in a hypothesis. Let us turn to how to deal with an “or”-statement appearing in a goal. This is quite easy: you have to prove one or the other of the alternatives in the “or”-statement, so just announce which one you expect to work, and then prove it.

Problem

Let \(x\) be a real number for which \(2x+1=5\). Show that either \(x=1\) or \(x=2\).

Solution

We will show \(x=2\). Indeed,

In Lean, use the tactic `right`

to announce you will be proving the right alternative of the goal
(or `left`

for the left one). This changes the goal displayed in the infoview: from

```
⊢ x = 1 ∨ x = 2
```

before the tactic application to

```
⊢ x = 2
```

afterwards.

```
example {x : ℝ} (hx : 2 * x + 1 = 5) : x = 1 ∨ x = 2 := by
right
calc
x = (2 * x + 1 - 1) / 2 := by ring
_ = (5 - 1) / 2 := by rw [hx]
_ = 2 := by numbers
```

### 2.3.4. Example

Let’s do an example which features both these styles of logical reasoning. We solve a quadratic equation; this is a classic situation where the result has an “or” in it. We will get to use the following lemma: if the product of two numbers is zero, then one of them is zero.

Problem

Let \(x\) be a real number for which \(x^2-3x+2=0\). Show that either \(x=1\) or \(x=2\).

Solution

We have that

So either \(x-1=0\) or \(x-2=0\).

If \(x-1=0\), then \(x=1\).

If \(x-2=0\), then \(x=2\).

In this solution, the case division argument is written a little more casually than in previous examples. The phrases “If \(x-1=0\)” and “If \(x-2=0\)” silently introduce the two cases, and it is left to the reader to observe that \(x=1\) is the left alternative of “\(x=1\) or \(x=2\)”, which finishes the problem (similarly for the second case).

I have done the first part of the Lean argument: writing up the calculation which establishes that
\((x-1)(x-2)=0\), then calling on the lemma `eq_zero_or_eq_zero_of_mul_eq_zero`

to turn this
into an “or” hypothesis. The goal state now looks like this, with both an “or” hypothesis and an
“or” goal.

```
x : ℝ
hx : x ^ 2 - 3 * x + 2 = 0
h1 : (x - 1) * (x - 2) = 0
h2 : x - 1 = 0 ∨ x - 2 = 0
⊢ x = 1 ∨ x = 2
```

Exercise: Fill in the rest of the Lean version of the argument.

```
example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 := by
have h1 :=
calc
(x - 1) * (x - 2) = x ^ 2 - 3 * x + 2 := by ring
_ = 0 := by rw [hx]
have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
sorry
```

### 2.3.5. Example

In Example 2.3.2 we showed that no natural number squares to 2. It is also true that no integer squares to 2, but since order laws are more complicated when negative numbers are involved, the proof is more complicated, requiring cases within cases.

Problem

Let \(n\) be any integer. Show that \(n ^ 2 \ne 2\).

Solution

We consider separately the cases \(n \le 0\) and \(1 \le n\).

**Case 1** (\(n \le 0\)): In this case we have \(0 \le -n\).
We consider separately the cases \(-n \le 1\) and \(2 \le -n\).

**Case 1(i)** (\(-n \le 1\)): It suffices to prove that \(n ^ 2 < 2\). Indeed,

**Case 1(ii)** (\(2 \le -n\)): It suffices to prove that \(n ^ 2 > 2\). Indeed,

**Case 2** (\(1 \le n\)): We consider separately the cases \(n \le 1\) and \(2 \le n\).

**Case 2(i)** (\(n \le 1\)): It suffices to prove that \(n ^ 2 < 2\). Indeed,

**Case 2(ii)** (\(2 \le n\)): It suffices to prove that \(n ^ 2 > 2\). Indeed,

When a proof becomes this complicated, you may find it helpful to mark the start of each new
sub-proof with the symbol `·`

, as follows.

```
example {n : ℤ} : n ^ 2 ≠ 2 := by
have hn0 := le_or_succ_le n 0
obtain hn0 | hn0 := hn0
· have : 0 ≤ -n := by addarith [hn0]
have hn := le_or_succ_le (-n) 1
obtain hn | hn := hn
· apply ne_of_lt
calc
n ^ 2 = (-n) ^ 2 := by ring
_ ≤ 1 ^ 2 := by rel [hn]
_ < 2 := by numbers
· apply ne_of_gt
calc
(2:ℤ) < 2 ^ 2 := by numbers
_ ≤ (-n) ^ 2 := by rel [hn]
_ = n ^ 2 := by ring
· have hn := le_or_succ_le n 1
obtain hn | hn := hn
· apply ne_of_lt
calc
n ^ 2 ≤ 1 ^ 2 := by rel [hn]
_ < 2 := by numbers
· apply ne_of_gt
calc
(2:ℤ) < 2 ^ 2 := by numbers
_ ≤ n ^ 2 := by rel [hn]
```

We record this theorem for future use under the name `sq_ne_two`

.

### 2.3.6. Exercises

Let \(x\) be a rational number and suppose that \(x=4\) or \(x=-4\). Show that \(x^2+1=17\).

example {x : ℚ} (h : x = 4 ∨ x = -4) : x ^ 2 + 1 = 17 := by sorry

Let \(x\) be a real number and suppose that either \(x=1\) or \(x=2\). Show that \(x^2-3x+2=0\).

example {x : ℝ} (h : x = 1 ∨ x = 2) : x ^ 2 - 3 * x + 2 = 0 := by sorry

Let \(t\) be a rational number and suppose that \(t=-2\) or \(t=3\). Show that \(t^2-t-6=0\).

example {t : ℚ} (h : t = -2 ∨ t = 3) : t ^ 2 - t - 6 = 0 := by sorry

Let \(x\) and \(y\) be real numbers and suppose that \(x=2\) or \(y=-2\). Show that \(x^2+2x=2y+4\).

example {x y : ℝ} (h : x = 2 ∨ y = -2) : x * y + 2 * x = 2 * y + 4 := by sorry

Let \(s\) and \(t\) be rational numbers for which \(s = 3 - t\). Show that either \(s + t = 3\) or \(s + t = 5\).

example {s t : ℚ} (h : s = 3 - t) : s + t = 3 ∨ s + t = 5 := by sorry

Let \(a\) and \(b\) be rational numbers for which \(a + 2b < 0\). Show that either \(b < a / 2\) or \(b < -a/2\).

example {a b : ℚ} (h : a + 2 * b < 0) : b < a / 2 ∨ b < - a / 2 := by sorry

Let \(x\) and \(y\) be real numbers for which \(y = 2x+1\). Show that either \(x<y/2\) or \(x>y/2\).

example {x y : ℝ} (h : y = 2 * x + 1) : x < y / 2 ∨ x > y / 2 := by sorry

Let \(x\) be a real number for which \(x^2+2x-3=0\). Show that either \(x=-3\) or \(x=1\).

You will probably use the same lemma as in Example 2.3.4.

example {x : ℝ} (hx : x ^ 2 + 2 * x - 3 = 0) : x = -3 ∨ x = 1 := by sorry

Let \(a\) and \(b\) be real numbers for which \(a^2+2b^2=3ab\). Show that either \(a=b\) or \(a=2b\).

You will probably use the same lemma as in Example 2.3.4.

example {a b : ℝ} (hab : a ^ 2 + 2 * b ^ 2 = 3 * a * b) : a = b ∨ a = 2 * b := by sorry

Let \(t\) be a real number for which \(t^3=t^2\). Show that either \(t=1\) or \(t=0\).

You will probably use the same lemma as in Example 2.3.4, as well as the

`cancel`

tactic.example {t : ℝ} (ht : t ^ 3 = t ^ 2) : t = 1 ∨ t = 0 := by sorry

Let \(n\) be any natural number. Show that \(n ^ 2 \ne 7\).

You will probably use the same lemma as in Example 2.3.2.

example {n : ℕ} : n ^ 2 ≠ 7 := by sorry

Let \(x\) be any integer. Show that \(2x \ne 3\).

You will probably use the same lemma as in Example 2.3.2.

example {x : ℤ} : 2 * x ≠ 3 := by sorry

Let \(t\) be any integer. Show that \(5t \ne 18\).

You will probably use the same lemma as in Example 2.3.2.

example {t : ℤ} : 5 * t ≠ 18 := by sorry

Let \(m\) be any natural number. Show that \(m ^ 2 +4m\ne 46\).

You will probably use the same lemma as in Example 2.3.2.

example {m : ℕ} : m ^ 2 + 4 * m ≠ 46 := by sorry

## 2.4. “And”

### 2.4.1. Example

In mathematics, the word “and” (denoted \(\land\) as a logical symbol), like “or”, can connect two statements. For example, here is a problem in which the hypothesis is an “and”-statement.

Problem

Let \(x\) and \(y\) be integers and suppose that \(2x-y=4\) and \(y-x+1=2\). Prove that \(x=5\).

In fact, we studied this problem before, in Example 1.3.6. Then, we considered the problem as having two separate hypotheses:

\(2x-y=4\)

\(y-x+1=2\)

but now for the sake of argument we’re considering it as having a single hypothesis:

\(2x-y=4\) and \(y-x+1=2\).

The distinction is pretty pedantic, and invisible in the text. In Lean, it’s more visible: we
might find ourselves in a situation with a hypothesis which explicitly features the `∧`

symbol,
like

```
x y : ℤ
h : 2 * x - y = 4 ∧ y - x + 1 = 2
⊢ x = 5
```

In such a situation, the tactic `obtain`

will split up an “and” hypothesis into its constituent
parts,

```
x y : ℤ
h1 : 2 * x - y = 4
h2 : y - x + 1 = 2
⊢ x = 5
```

and then the problem can be solved accessing each of these parts separately, as needed. In this case we have effectively brought the problem back to the setup of Example 1.3.6.

```
example {x y : ℤ} (h : 2 * x - y = 4 ∧ y - x + 1 = 2) : x = 5 := by
obtain ⟨h1, h2⟩ := h
calc
x = 2 * x - y + (y - x + 1) - 1 := by ring
_ = 4 + 2 - 1 := by rw [h1, h2]
_ = 5 := by ring
```

### 2.4.2. Example

“And” hypotheses turn up relatively rarely in the wild. One situation in which one might occur is when a single hypothesis has two natural consequences, which are paired together in a lemma. For example, if \(x^2 \le y^2\) for some positive number \(y\), then one can draw the conclusion \(-y \le x \le y\), which is shorthand (recall Example 1.4.4) for “\(-y\leq x\) and \(x\le y\).”

Problem

Let \(p\) be a rational number for which \(p^2\le 8\). Show that \(p\ge -5\).

Solution

We have that

and 3 is positive, so \(-3\le p\le 3\). Thus

In Lean, we use the lemma `abs_le_of_sq_le_sq'`

for this argument. This lemma was added to Lean’s
library by a Fordham student, Ben Davidson. Note the `∧`

in the conclusion of the lemma statement.

```
theorem abs_le_of_sq_le_sq' {x y : ℚ} (h1 : x ^ 2 ≤ y ^ 2) (h2 : 0 ≤ y) :
-y ≤ x ∧ x ≤ y :=
```

Exercise: I have written up in Lean the part of the proof which gets us to the intermediate fact
`hp' : -3 ≤ p ∧ p ≤ 3`

. Deal with this “and” hypothesis and then finish the proof in Lean.

```
example {p : ℚ} (hp : p ^ 2 ≤ 8) : p ≥ -5 := by
have hp' : -3 ≤ p ∧ p ≤ 3
· apply abs_le_of_sq_le_sq'
calc
p ^ 2 ≤ 9 := by addarith [hp]
_ = 3 ^ 2 := by numbers
numbers
sorry
```

Note a new piece of Lean syntax in the above proof: a line like

```
have hp' : -3 ≤ p ∧ p ≤ 3
```

without a justification will cause Lean to ask you for that justification – that is, a new goal will appear, the goal of proving that statement.

```
2 goals
p : ℚ
hp : p ^ 2 ≤ 8
⊢ -3 ≤ p ∧ p ≤ 3
p : ℚ
hp : p ^ 2 ≤ 8
hp' : -3 ≤ p ∧ p ≤ 3
⊢ p ≥ -5
```

After you complete the proof (as I did here),
you are back to where you were before except that the fact `hp'`

is now a fully-justified
intermediate fact, available for use.

### 2.4.3. Example

It also sometimes happens that the goal of a problem features an “and” statement. For example, you might be given a system of simultaneous equations, and asked to determine the values of all the variables appearing. Here’s a system of simultaneous equations we saw before in Example 1.3.3, but the problem statement has been tweaked to ask us to find the values of both \(a\) and \(b\).

Problem

Let \(a\) and \(b\) be real numbers and suppose that \(a-5b=4\) and \(b+2=3\). Show that \(a=9\) and \(b=1\).

One way to solve such a problem is to establish the two facts asked for completely independently:

Solution

We have,

and since \(b+2=3\), we have \(b=1\).

In Lean, we write this proof using the `constructor`

tactic, which takes a problem in which the
goal is an “and” statement,

```
a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
⊢ a = 9 ∧ b = 1
```

and reduces it two simpler tasks, one for each part of the “and”.

```
a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
⊢ a = 9
a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
⊢ b = 1
```

We then write up Lean proofs for these two tasks, one after the other.

```
example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 ∧ b = 1 := by
constructor
· calc
a = 4 + 5 * b := by addarith [h1]
_ = -6 + 5 * (b + 2) := by ring
_ = -6 + 5 * 3 := by rw [h2]
_ = 9 := by ring
· addarith [h2]
```

Alternatively, there might be an intermediate fact which you wish to note and then use in both parts of the proof. For example, you might want to first solve for \(b\), and then use that to shorten the work of solving for \(a\).

Solution

Since \(b+2=3\), we have \(b=1\). Therefore

It is typically left to the reader to check that both parts of the desired goal, \(a=9\) and \(b=1\), are established somewhere along the way.

Here is how this proof looks in Lean. The important observation is that if there is something you
want to use in both parts of the proof (here, the fact \(b=1\)), then this must be established
before the tactic `constructor`

is used. When the tactic `constructor`

is used, all facts
established so far become available for both of the two tasks created:

```
a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
hb : b = 1
⊢ a = 9
a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
hb : b = 1
⊢ b = 1
```

```
example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 ∧ b = 1 := by
have hb : b = 1 := by addarith [h2]
constructor
· calc
a = 4 + 5 * b := by addarith [h1]
_ = 4 + 5 * 1 := by rw [hb]
_ = 9 := by ring
· apply hb
```

### 2.4.4. Example

One more example with an “and” in the goal.

Problem

Let \(a\) and \(b\) be real numbers and suppose that \(a^2+b^2=0\). Show that \(a=0\) and \(b=0\).

Solution

We first show that \(a^2=0\). \((\star)\) Indeed,

and also since squares are nonnegative \(a^2\geq 0\).

By \((\star)\), \(a=0\). Also by \((\star)\),

so \(b=0\).

Part of this problem might feel familiar. The proof of the intermediate goal, \(a^2=0\), is a repeat of Example 2.2.3.

Here is the problem statement in Lean, together with a proof of the intermediate goal \(a^2=0\)
copied from Example 2.2.3. Fill in the rest of the proof. The tactic
`cancel`

will be helpful to deduce that quantities are zero when their squares are known to be
zero.

```
example {a b : ℝ} (h1 : a ^ 2 + b ^ 2 = 0) : a = 0 ∧ b = 0 := by
have h2 : a ^ 2 = 0
· apply le_antisymm
calc
a ^ 2 ≤ a ^ 2 + b ^ 2 := by extra
_ = 0 := by rw [h1]
extra
sorry
```

### 2.4.5. Exercises

Let \(a\) and \(b\) be rational numbers and suppose that \(a \le 1\) and \(a + b \le 3\). Show that \(2a+b \le 4\).

example {a b : ℚ} (H : a ≤ 1 ∧ a + b ≤ 3) : 2 * a + b ≤ 4 := by sorry

Let \(r\) and \(s\) be real numbers and suppose that \(r + s \le 1\) and \(r - s \le 5\). Show that \(2r \le 6\).

example {r s : ℝ} (H : r + s ≤ 1 ∧ r - s ≤ 5) : 2 * r ≤ 6 := by sorry

Let \(m\) and \(n\) be integers and suppose that \(n \le 8\) and \(m + 5 \le n\). Show that \(m \le 3\).

example {m n : ℤ} (H : n ≤ 8 ∧ m + 5 ≤ n) : m ≤ 3 := by sorry

Let \(p\) be an integer and suppose that \(p + 2 \ge 9\). Show that \(p^2\geq 49\) and \(7 \le p\).

example {p : ℤ} (hp : p + 2 ≥ 9) : p ^ 2 ≥ 49 ∧ 7 ≤ p := by sorry

Let \(a\) be a rational number and suppose that \(a - 1 \ge 5\). Show that \(a \ge 6\) and \(3a \ge 10\).

example {a : ℚ} (h : a - 1 ≥ 5) : a ≥ 6 ∧ 3 * a ≥ 10 := by sorry

Let \(x\) and \(y\) be rational numbers and suppose that \(x + y = 5\) and \(x + 2y = 7\). Show that \(x=3\) and \(y=2\).

example {x y : ℚ} (h : x + y = 5 ∧ x + 2 * y = 7) : x = 3 ∧ y = 2 := by sorry

Let \(a\) and \(b\) be real numbers and suppose that \(ab=a=b\). Show that either \(a=b=0\) or \(a=b=1\).

You will probably need the lemma

`eq_zero_or_eq_zero_of_mul_eq_zero`

proved in Example 2.3.4.example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) : a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by sorry

## 2.5. Existence proofs

### 2.5.1. Example

This section covers the *existential quantifier*, the logical concept expressed in English as

There exists … such that ….

For example, here is a problem in which a hypothesis features an existential quantifier.

Problem

Let \(a\) be a rational number, and suppose that there exists a rational number \(b\), such that \(a=b^2+1\). Show that \(a>0\).

The hypothesis “there exists a rational number \(b\), such that \(a=b^2+1\)” can be broken
down immediately to actually get our hands on the *witness* for the existential: a rational number
\(b\) satisfying \(a=b^2+1\) (there might be more than one, but this will just choose one
witness). Then we can do a regular calculational proof which involves the witness \(b\).

Solution

Let \(b\) be a rational number such that \(a=b^2+1\). We have,

The logical symbol for an existential is \(\exists\). In Lean, the tactic `obtain`

is used to
break up an existential hypothesis into a witness and a hypothesis about that witness. The syntax
is the same as the syntax for breaking apart an “and” (see Section 2.4).

```
example {a : ℚ} (h : ∃ b : ℚ, a = b ^ 2 + 1) : a > 0 := by
obtain ⟨b, hb⟩ := h
calc
a = b ^ 2 + 1 := hb
_ > 0 := by extra
```

In this problem, the goal view is initially

```
a : ℚ
h : ∃ b, a = b ^ 2 + 1
⊢ a > 0
```

After the use of the `obtain`

tactic, the existential is broken apart, so the witness appears
separately on the variable list and can be accessed in the succeeding proof:

```
a b : ℚ
hb : a = b ^ 2 + 1
⊢ a > 0
```

### 2.5.2. Example

Here’s another problem with an existential hypothesis, “there exists a real number \(a\), such that \(at<0\)”. As before we break it apart and then follow earlier methods.

Problem

Let \(t\) be a real number, and suppose that there exists a real number \(a\), such that \(at<0\). Show that \(t\ne 0\).

Solution

Let \(x\) be a real number such that \(xt<0\). We consider separately the cases \(x\le 0\) and \(0<x\).

**Case 1** (\(x \le 0\)): We have \(0<(-x)t\) and \(0 \le -x\), so we have that
\(0 < t\), and so \(t\ne 0\).

**Case 2** (\(0<x\)): We have that

and \(0 \le x\), so \(0 < -t\), so \(t<0\), so \(t\ne 0\),

Here is a partial solution in Lean (using `obtain`

for the first step to break apart the
existential, and then again later to perform the case division). Case 2 is missing; do that
yourself.

```
example {t : ℝ} (h : ∃ a : ℝ, a * t < 0) : t ≠ 0 := by
obtain ⟨x, hxt⟩ := h
have H := le_or_gt x 0
obtain hx | hx := H
· have hxt' : 0 < (-x) * t := by addarith [hxt]
have hx' : 0 ≤ -x := by addarith [hx]
cancel -x at hxt'
apply ne_of_gt
apply hxt'
· sorry
```

### 2.5.3. Example

To prove a problem in which the goal has an existential, you need to provide a witness yourself, and then verify that your proposed witness works.

Problem

Show that there exists an integer \(n\), such that \(12n=84\).

Solution

The integer \(7\) has this property. Indeed, \(12 \cdot 7=84\).

In Lean the tactic `use`

is used to state what you have chosen as the witness.

```
example : ∃ n : ℤ, 12 * n = 84 := by
use 7
numbers
```

In this problem, the goal was initially

```
⊢ ∃ n : ℤ, 12 * n = 84
```

but after the tactic `use 7`

the goal has changed to checking that the proposed witness, 7,
works.

```
⊢ 12 * 7 = 84
```

This is what `numbers`

checks.

### 2.5.4. Example

Often, it requires some creativity to come up with a witness for an existential goal. The rest of this section consists of practice coming up with witnesses.

Problem

Let \(x\) be a real number. Show that there exists a real number \(y\), such that \(y>x\).

Solution

The real number \(x + 1\) has this property. Indeed, \(x+1>x\).

```
example (x : ℝ) : ∃ y : ℝ, y > x := by
use x + 1
extra
```

### 2.5.5. Example

Problem

Show that there exist integers \(m\) and \(n\), such that \(m^2-n^2=11\).

Solution

We can take \(m=6\), \(n=5\). Indeed,

```
example : ∃ m n : ℤ, m ^ 2 - n ^ 2 = 11 := by
sorry
```

### 2.5.6. Example

Sometimes you may wish to leave out the sentence “We can take …” explicitly stating what the witness is. In this case you should be extra pedantic about verifying the desired properties exactly in the form they are stated.

Problem

Let \(a\) be an integer. Show that there exist integers \(m\) and \(n\), such that \(m^2-n^2=2a+1\).

Solution

In Lean, you still have to use `use`

to state the witnesses.

```
example (a : ℤ) : ∃ m n : ℤ, m ^ 2 - n ^ 2 = 2 * a + 1 := by
sorry
```

### 2.5.7. Example

Problem

Let \(p\) and \(q\) be real numbers, and suppose \(p<q\). Show that there exists a real number \(x\), such that \(p<x<q\).

Solution

We will show that \(\frac{p+q}{2}\) has this property. Indeed,

and

```
example {p q : ℝ} (h : p < q) : ∃ x, p < x ∧ x < q := by
sorry
```

### 2.5.8. Example

I remember once going to see him [Ramanujan] when he was lying ill at Putney. I had ridden in taxi cab number 1729 and remarked that the number seemed to me rather a dull one, and that I hoped it was not an unfavorable omen. “No,” he replied, “it is a very interesting number; it is the smallest number expressible as the sum of two cubes in two different ways.”

—G. H. Hardy,

Ramanujan: Twelve lectures on subjects suggested by his life and work

Problem

Show that there exist natural numbers \(a\), \(b\), \(c\) and \(d\), such that \(a^3+b^3=1729=c^3+d^3\), but \(a\ne c\) and \(a\ne d\). 3

Solution

\(1^3+12^3=1729=9^3+10^3\), but \(1\ne 9\) and \(1\ne 10\).

```
example : ∃ a b c d : ℕ,
a ^ 3 + b ^ 3 = 1729 ∧ c ^ 3 + d ^ 3 = 1729 ∧ a ≠ c ∧ a ≠ d := by
use 1, 12, 9, 10
constructor
numbers
constructor
numbers
constructor
numbers
numbers
```

### 2.5.9. Exercises

Show that there exists a rational number \(t\), such that \(t^2=1.69\).

example : ∃ t : ℚ, t ^ 2 = 1.69 := by sorry

Show that there exist integers \(m\) and \(n\), such that \(m^2+n^2=85\).

example : ∃ m n : ℤ, m ^ 2 + n ^ 2 = 85 := by sorry

Show that there exists a real number \(x\), such that \(x<0\) and \(x^2<1\).

example : ∃ x : ℝ, x < 0 ∧ x ^ 2 < 1 := by sorry

Show that there exist natural numbers \(a\) and \(b\), such that \(2 ^ a = 5b+1\).

example : ∃ a b : ℕ, 2 ^ a = 5 * b + 1 := by sorry

Let \(x\) be a rational number. Show that there exists a rational number \(y\), such that \(y^2>x\).

example (x : ℚ) : ∃ y : ℚ, y ^ 2 > x := by sorry

Let \(t\) be a real number, and suppose that there exists a real number \(a\), such that \(at+1<a+t\). Show that \(t\ne 1\).

As in Example 2.5.2, I used the lemma

`le_or_gt`

, which says that if \(s\) and \(t\) are real numbers then either \(s \le t\) or \(t < s\); it can be a useful case division.example {t : ℝ} (h : ∃ a : ℝ, a * t + 1 < a + t) : t ≠ 1 := by sorry

Let \(m\) be an integer, and suppose that there exists an integer \(a\), such that \(2a=m\). Show that \(m\ne 5\).

example {m : ℤ} (h : ∃ a, 2 * a = m) : m ≠ 5 := by sorry

Let \(n\) be an integer. Show that there exists an integer \(a\), such that \(2a^3 ≥ na+7\).

example {n : ℤ} : ∃ a, 2 * a ^ 3 ≥ n * a + 7 := by sorry

Let \(a\), \(b\) and \(c\) be real numbers, and suppose that \(a\le b+c\), \(b\le a+c\) and \(c\le a+b\). Show that there exist nonnegative real numbers \(x\), \(y\) and \(z\) such that \(a=y+z\), \(b=x+z\) and \(c=x+y\).

example {a b c : ℝ} (ha : a ≤ b + c) (hb : b ≤ a + c) (hc : c ≤ a + b) : ∃ x y z, x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y := by sorry

Footnotes

- 3
Example adapted from Hammack, Book of Proof, Section 7.3.