# 3. Logic

In the last chapter, we dealt with equations, inequalities, and basic mathematical statements like “\(x\) divides \(y\).” Complex mathematical statements are built up from simple ones like these using logical terms like “and,” “or,” “not,” and “if … then,” “every,” and “some.” In this chapter, we show you how to work with statements that are built up in this way.

## 3.1. Implication and the Universal Quantifier

Consider the statement after the `#check`

:

```
#check ∀ x : ℝ, 0 ≤ x → |x| = x
```

In words, we would say “for every real number `x`

, if `0 ≤ x`

then
the absolute value of `x`

equals `x`

”.
We can also have more complicated statements like:

```
#check ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε
```

In words, we would say “for every `x`

, `y`

, and `ε`

,
if `0 < ε ≤ 1`

, the absolute value of `x`

is less than `ε`

,
and the absolute value of `y`

is less than `ε`

,
then the absolute value of `x * y`

is less than `ε`

.”
In Lean, in a sequence of implications there are
implicit parentheses grouped to the right.
So the expression above means
“if `0 < ε`

then if `ε ≤ 1`

then if `|x| < ε`

…”
As a result, the expression says that all the
assumptions together imply the conclusion.

You have already seen that even though the universal quantifier in this statement ranges over objects and the implication arrows introduce hypotheses, Lean treats the two in very similar ways. In particular, if you have proved a theorem of that form, you can apply it to objects and hypotheses in the same way. We will use as an example the following statement that we will help you to prove a bit later:

```
theorem my_lemma : ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
sorry
section
variable (a b δ : ℝ)
variable (h₀ : 0 < δ) (h₁ : δ ≤ 1)
variable (ha : |a| < δ) (hb : |b| < δ)
#check my_lemma a b δ
#check my_lemma a b δ h₀ h₁
#check my_lemma a b δ h₀ h₁ ha hb
end
```

You have also already seen that it is common in Lean to use curly brackets to make quantified variables implicit when they can be inferred from subsequent hypotheses. When we do that, we can just apply a lemma to the hypotheses without mentioning the objects.

```
theorem my_lemma2 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
sorry
section
variable (a b δ : ℝ)
variable (h₀ : 0 < δ) (h₁ : δ ≤ 1)
variable (ha : |a| < δ) (hb : |b| < δ)
#check my_lemma2 h₀ h₁ ha hb
end
```

At this stage, you also know that if you use
the `apply`

tactic to apply `my_lemma`

to a goal of the form `|a * b| < δ`

,
you are left with new goals that require you to prove
each of the hypotheses.

To prove a statement like this, use the `intro`

tactic.
Take a look at what it does in this example:

```
theorem my_lemma3 :
∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
intro x y ε epos ele1 xlt ylt
sorry
```

We can use any names we want for the universally quantified variables;
they do not have to be `x`

, `y`

, and `ε`

.
Notice that we have to introduce the variables
even though they are marked implicit:
making them implicit means that we leave them out when
we write an expression *using* `my_lemma`

,
but they are still an essential part of the statement
that we are proving.
After the `intro`

command,
the goal is what it would have been at the start if we
listed all the variables and hypotheses *before* the colon,
as we did in the last section.
In a moment, we will see why it is sometimes necessary to
introduce variables and hypotheses after the proof begins.

To help you prove the lemma, we will start you off:

```
theorem my_lemma4 :
∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
intro x y ε epos ele1 xlt ylt
calc
|x * y| = |x| * |y| := sorry
_ ≤ |x| * ε := sorry
_ < 1 * ε := sorry
_ = ε := sorry
```

Finish the proof using the theorems
`abs_mul`

, `mul_le_mul`

, `abs_nonneg`

,
`mul_lt_mul_right`

, and `one_mul`

.
Remember that you can find theorems like these using
Ctrl-space completion (or Cmd-space completion on a Mac).
Remember also that you can use `.mp`

and `.mpr`

or `.1`

and `.2`

to extract the two directions
of an if-and-only-if statement.

Universal quantifiers are often hidden in definitions,
and Lean will unfold definitions to expose them when necessary.
For example, let’s define two predicates,
`FnUb f a`

and `FnLb f a`

,
where `f`

is a function from the real numbers to the real
numbers and `a`

is a real number.
The first says that `a`

is an upper bound on the
values of `f`

,
and the second says that `a`

is a lower bound
on the values of `f`

.

```
def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, f x ≤ a
def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, a ≤ f x
```

In the next example, `fun x ↦ f x + g x`

is the
function that maps `x`

to `f x + g x`

. Going from the expression `f x + g x`

to this function is called a lambda abstraction in type theory.

```
example (hfa : FnUb f a) (hgb : FnUb g b) : FnUb (fun x ↦ f x + g x) (a + b) := by
intro x
dsimp
apply add_le_add
apply hfa
apply hgb
```

Applying `intro`

to the goal `FnUb (fun x ↦ f x + g x) (a + b)`

forces Lean to unfold the definition of `FnUb`

and introduce `x`

for the universal quantifier.
The goal is then `(fun (x : ℝ) ↦ f x + g x) x ≤ a + b`

.
But applying `(fun x ↦ f x + g x)`

to `x`

should result in `f x + g x`

,
and the `dsimp`

command performs that simplification.
(The “d” stands for “definitional.”)
You can delete that command and the proof still works;
Lean would have to perform that contraction anyhow to make
sense of the next `apply`

.
The `dsimp`

command simply makes the goal more readable
and helps us figure out what to do next.
Another option is to use the `change`

tactic
by writing `change f x + g x ≤ a + b`

.
This helps make the proof more readable,
and gives you more control over how the goal is transformed.

The rest of the proof is routine.
The last two `apply`

commands force Lean to unfold the definitions
of `FnUb`

in the hypotheses.
Try carrying out similar proofs of these:

```
example (hfa : FnLb f a) (hgb : FnLb g b) : FnLb (fun x ↦ f x + g x) (a + b) :=
sorry
example (nnf : FnLb f 0) (nng : FnLb g 0) : FnLb (fun x ↦ f x * g x) 0 :=
sorry
example (hfa : FnUb f a) (hgb : FnUb g b) (nng : FnLb g 0) (nna : 0 ≤ a) :
FnUb (fun x ↦ f x * g x) (a * b) :=
sorry
```

Even though we have defined `FnUb`

and `FnLb`

for functions
from the reals to the reals,
you should recognize that the definitions and proofs are much
more general.
The definitions make sense for functions between any two types
for which there is a notion of order on the codomain.
Checking the type of the theorem `add_le_add`

shows that it holds
of any structure that is an “ordered additive commutative monoid”;
the details of what that means don’t matter now,
but it is worth knowing that the natural numbers, integers, rationals,
and real numbers are all instances.
So if we prove the theorem `fnUb_add`

at that level of generality,
it will apply in all these instances.

```
variable {α : Type*} {R : Type*} [OrderedCancelAddCommMonoid R]
#check add_le_add
def FnUb' (f : α → R) (a : R) : Prop :=
∀ x, f x ≤ a
theorem fnUb_add {f g : α → R} {a b : R} (hfa : FnUb' f a) (hgb : FnUb' g b) :
FnUb' (fun x ↦ f x + g x) (a + b) := fun x ↦ add_le_add (hfa x) (hgb x)
```

You have already seen square brackets like these in Section Section 2.2, though we still haven’t explained what they mean. For concreteness, we will stick to the real numbers for most of our examples, but it is worth knowing that Mathlib contains definitions and theorems that work at a high level of generality.

For another example of a hidden universal quantifier,
Mathlib defines a predicate `Monotone`

,
which says that a function is nondecreasing in its arguments:

```
example (f : ℝ → ℝ) (h : Monotone f) : ∀ {a b}, a ≤ b → f a ≤ f b :=
@h
```

The property `Monotone f`

is defined to be exactly the expression
after the colon. We need to put the `@`

symbol before `h`

because
if we don’t,
Lean expands the implicit arguments to `h`

and inserts placeholders.

Proving statements about monotonicity
involves using `intro`

to introduce two variables,
say, `a`

and `b`

, and the hypothesis `a ≤ b`

.
To *use* a monotonicity hypothesis,
you can apply it to suitable arguments and hypotheses,
and then apply the resulting expression to the goal.
Or you can apply it to the goal and let Lean help you
work backwards by displaying the remaining hypotheses
as new subgoals.

```
example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x := by
intro a b aleb
apply add_le_add
apply mf aleb
apply mg aleb
```

When a proof is this short, it is often convenient
to give a proof term instead.
To describe a proof that temporarily introduces objects
`a`

and `b`

and a hypothesis `aleb`

,
Lean uses the notation `fun a b aleb ↦ ...`

.
This is analogous to the way that an expression
like `fun x ↦ x^2`

describes a function
by temporarily naming an object, `x`

,
and then using it to describe a value.
So the `intro`

command in the previous proof
corresponds to the lambda abstraction in the next proof term.
The `apply`

commands then correspond to building
the application of the theorem to its arguments.

```
example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x :=
fun a b aleb ↦ add_le_add (mf aleb) (mg aleb)
```

Here is a useful trick: if you start writing
the proof term `fun a b aleb ↦ _`

using
an underscore where the rest of the
expression should go,
Lean will flag an error,
indicating that it can’t guess the value of that expression.
If you check the Lean Goal window in VS Code or
hover over the squiggly error marker,
Lean will show you the goal that the remaining
expression has to solve.

Try proving these, with either tactics or proof terms:

```
example {c : ℝ} (mf : Monotone f) (nnc : 0 ≤ c) : Monotone fun x ↦ c * f x :=
sorry
example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f (g x) :=
sorry
```

Here are some more examples.
A function \(f\) from \(\Bbb R\) to
\(\Bbb R\) is said to be *even* if
\(f(-x) = f(x)\) for every \(x\),
and *odd* if \(f(-x) = -f(x)\) for every \(x\).
The following example defines these two notions formally
and establishes one fact about them.
You can complete the proofs of the others.

```
def FnEven (f : ℝ → ℝ) : Prop :=
∀ x, f x = f (-x)
def FnOdd (f : ℝ → ℝ) : Prop :=
∀ x, f x = -f (-x)
example (ef : FnEven f) (eg : FnEven g) : FnEven fun x ↦ f x + g x := by
intro x
calc
(fun x ↦ f x + g x) x = f x + g x := rfl
_ = f (-x) + g (-x) := by rw [ef, eg]
example (of : FnOdd f) (og : FnOdd g) : FnEven fun x ↦ f x * g x := by
sorry
example (ef : FnEven f) (og : FnOdd g) : FnOdd fun x ↦ f x * g x := by
sorry
example (ef : FnEven f) (og : FnOdd g) : FnEven fun x ↦ f (g x) := by
sorry
```

The first proof can be shortened using `dsimp`

or `change`

to get rid of the lambda abstraction.
But you can check that the subsequent `rw`

won’t work
unless we get rid of the lambda abstraction explicitly,
because otherwise it cannot find the patterns `f x`

and `g x`

in the expression.
Contrary to some other tactics, `rw`

operates on the syntactic level,
it won’t unfold definitions or apply reductions for you
(it has a variant called `erw`

that tries a little harder in this
direction, but not much harder).

You can find implicit universal quantifiers all over the place, once you know how to spot them.

Mathlib includes a good library for manipulating sets. Recall that Lean does not
use foundations based on set theory, so here the word set has its mundane meaning
of a collection of mathematical objects of some given type `α`

.
If `x`

has type `α`

and `s`

has type `Set α`

, then `x ∈ s`

is a proposition
that asserts that `x`

is an element of `s`

. If `y`

has some different type `β`

then the
expression `y ∈ s`

makes no sense. Here “makes no sense” means “has no type hence Lean does not
accept it as a well-formed statement”. This contrasts with Zermelo-Fraenkel set theory for instance
where `a ∈ b`

is a well-formed statement for every mathematical objects `a`

and `b`

.
For instance `sin ∈ cos`

is a well-formed statement in ZF. This defect of set theoretic
foundations is an important motivation for not using it in a proof assistant which is meant to assist
us by detecting meaningless expressions. In Lean `sin`

has type `ℝ → ℝ`

and `cos`

has type
`ℝ → ℝ`

which is not equal to `Set (ℝ → ℝ)`

, even after unfolding definitions, so the statement
`sin ∈ cos`

makes no sense.
One can also use Lean to work on set theory itself. For instance the independence of the continuum
hypothesis from the axioms of Zermelo-Fraenkel has been formalized in Lean. But such a meta-theory
of set theory is completely beyond the scope of this book.

If `s`

and `t`

are of type `Set α`

,
then the subset relation `s ⊆ t`

is defined to mean
`∀ {x : α}, x ∈ s → x ∈ t`

.
The variable in the quantifier is marked implicit so that
given `h : s ⊆ t`

and `h' : x ∈ s`

,
we can write `h h'`

as justification for `x ∈ t`

.
The following example provides a tactic proof and a proof term
justifying the reflexivity of the subset relation,
and asks you to do the same for transitivity.

```
variable {α : Type*} (r s t : Set α)
example : s ⊆ s := by
intro x xs
exact xs
theorem Subset.refl : s ⊆ s := fun x xs ↦ xs
theorem Subset.trans : r ⊆ s → s ⊆ t → r ⊆ t := by
sorry
```

Just as we defined `FnUb`

for functions,
we can define `SetUb s a`

to mean that `a`

is an upper bound on the set `s`

,
assuming `s`

is a set of elements of some type that
has an order associated with it.
In the next example, we ask you to prove that
if `a`

is a bound on `s`

and `a ≤ b`

,
then `b`

is a bound on `s`

as well.

```
variable {α : Type*} [PartialOrder α]
variable (s : Set α) (a b : α)
def SetUb (s : Set α) (a : α) :=
∀ x, x ∈ s → x ≤ a
example (h : SetUb s a) (h' : a ≤ b) : SetUb s b :=
sorry
```

We close this section with one last important example.
A function \(f\) is said to be *injective* if for
every \(x_1\) and \(x_2\),
if \(f(x_1) = f(x_2)\) then \(x_1 = x_2\).
Mathlib defines `Function.Injective f`

with
`x₁`

and `x₂`

implicit.
The next example shows that, on the real numbers,
any function that adds a constant is injective.
We then ask you to show that multiplication by a nonzero
constant is also injective, using the lemma name in the example as a source
of inspiration. Recall you should use Ctrl-space completion after guessing the beginning of
a lemma name.

```
open Function
example (c : ℝ) : Injective fun x ↦ x + c := by
intro x₁ x₂ h'
exact (add_left_inj c).mp h'
example {c : ℝ} (h : c ≠ 0) : Injective fun x ↦ c * x := by
sorry
```

Finally, show that the composition of two injective functions is injective:

```
variable {α : Type*} {β : Type*} {γ : Type*}
variable {g : β → γ} {f : α → β}
example (injg : Injective g) (injf : Injective f) : Injective fun x ↦ g (f x) := by
sorry
```

## 3.2. The Existential Quantifier

The existential quantifier, which can be entered as `\ex`

in VS Code,
is used to represent the phrase “there exists.”
The formal expression `∃ x : ℝ, 2 < x ∧ x < 3`

in Lean says
that there is a real number between 2 and 3.
(We will discuss the conjunction symbol, `∧`

, in Section 3.4.)
The canonical way to prove such a statement is to exhibit a real number
and show that it has the stated property.
The number 2.5, which we can enter as `5 / 2`

or `(5 : ℝ) / 2`

when Lean cannot infer from context that we have
the real numbers in mind, has the required property,
and the `norm_num`

tactic can prove that it meets the description.

There are a few ways we can put the information together.
Given a goal that begins with an existential quantifier,
the `use`

tactic is used to provide the object,
leaving the goal of proving the property.

```
example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
use 5 / 2
norm_num
```

You can give the `use`

tactic proofs as well as data:

```
example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
have h1 : 2 < (5 : ℝ) / 2 := by norm_num
have h2 : (5 : ℝ) / 2 < 3 := by norm_num
use 5 / 2, h1, h2
```

In fact, the `use`

tactic automatically tries to use available assumptions as well.

```
example : ∃ x : ℝ, 2 < x ∧ x < 3 := by
have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num
use 5 / 2
```

Alternatively, we can use Lean’s *anonymous constructor* notation
to construct a proof of an existential quantifier.

```
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3 := by norm_num
⟨5 / 2, h⟩
```

Notice that there is no `by`

; here we are giving an explicit proof term.
The left and right angle brackets,
which can be entered as `\<`

and `\>`

respectively,
tell Lean to put together the given data using
whatever construction is appropriate
for the current goal.
We can use the notation without going first into tactic mode:

```
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
⟨5 / 2, by norm_num⟩
```

So now we know how to *prove* an exists statement.
But how do we *use* one?
If we know that there exists an object with a certain property,
we should be able to give a name to an arbitrary one
and reason about it.
For example, remember the predicates `FnUb f a`

and `FnLb f a`

from the last section,
which say that `a`

is an upper bound or lower bound on `f`

,
respectively.
We can use the existential quantifier to say that “`f`

is bounded”
without specifying the bound:

```
def FnUb (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, f x ≤ a
def FnLb (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, a ≤ f x
def FnHasUb (f : ℝ → ℝ) :=
∃ a, FnUb f a
def FnHasLb (f : ℝ → ℝ) :=
∃ a, FnLb f a
```

We can use the theorem `FnUb_add`

from the last section
to prove that if `f`

and `g`

have upper bounds,
then so does `fun x ↦ f x + g x`

.

```
variable {f g : ℝ → ℝ}
example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
rcases ubf with ⟨a, ubfa⟩
rcases ubg with ⟨b, ubgb⟩
use a + b
apply fnUb_add ubfa ubgb
```

The `rcases`

tactic unpacks the information
in the existential quantifier.
The annotations like `⟨a, ubfa⟩`

, written with the
same angle brackets as the anonymous constructors,
are known as *patterns*, and they describe the information
that we expect to find when we unpack the main argument.
Given the hypothesis `ubf`

that there is an upper bound
for `f`

,
`rcases ubf with ⟨a, ubfa⟩`

adds a new variable `a`

for an upper bound to the context,
together with the hypothesis `ubfa`

that it has the given property.
The goal is left unchanged;
what *has* changed is that we can now use
the new object and the new hypothesis
to prove the goal.
This is a common method of reasoning in mathematics:
we unpack objects whose existence is asserted or implied
by some hypothesis, and then use it to establish the existence
of something else.

Try using this method to establish the following.
You might find it useful to turn some of the examples
from the last section into named theorems,
as we did with `fn_ub_add`

,
or you can insert the arguments directly
into the proofs.

```
example (lbf : FnHasLb f) (lbg : FnHasLb g) : FnHasLb fun x ↦ f x + g x := by
sorry
example {c : ℝ} (ubf : FnHasUb f) (h : c ≥ 0) : FnHasUb fun x ↦ c * f x := by
sorry
```

The “r” in `rcases`

stands for “recursive,” because it allows
us to use arbitrarily complex patterns to unpack nested data.
The `rintro`

tactic
is a combination of `intro`

and `rcases`

:

```
example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x := by
rintro ⟨a, ubfa⟩ ⟨b, ubgb⟩
exact ⟨a + b, fnUb_add ubfa ubgb⟩
```

In fact, Lean also supports a pattern-matching fun in expressions and proof terms:

```
example : FnHasUb f → FnHasUb g → FnHasUb fun x ↦ f x + g x :=
fun ⟨a, ubfa⟩ ⟨b, ubgb⟩ ↦ ⟨a + b, fnUb_add ubfa ubgb⟩
```

The task of unpacking information in a hypothesis is
so important that Lean and Mathlib provide a number of
ways to do it. For example, the `obtain`

tactic provides suggestive syntax:

```
example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
obtain ⟨a, ubfa⟩ := ubf
obtain ⟨b, ubgb⟩ := ubg
exact ⟨a + b, fnUb_add ubfa ubgb⟩
```

Think of the first `obtain`

instruction as matching the “contents” of `ubf`

with the given pattern and assigning the components to the named variables.
`rcases`

and `obtain`

are said to `destruct`

their arguments, though
there is a small difference in that `rcases`

clears `ubf`

from the context
when it is done, whereas it is still present after `obtain`

.

Lean also supports syntax that is similar to that used in other functional programming languages:

```
example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
cases ubf
case intro a ubfa =>
cases ubg
case intro b ubgb =>
exact ⟨a + b, fnUb_add ubfa ubgb⟩
example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
cases ubf
next a ubfa =>
cases ubg
next b ubgb =>
exact ⟨a + b, fnUb_add ubfa ubgb⟩
example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by
match ubf, ubg with
| ⟨a, ubfa⟩, ⟨b, ubgb⟩ =>
exact ⟨a + b, fnUb_add ubfa ubgb⟩
example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x :=
match ubf, ubg with
| ⟨a, ubfa⟩, ⟨b, ubgb⟩ =>
⟨a + b, fnUb_add ubfa ubgb⟩
```

In the first example, if you put your cursor after `cases ubf`

,
you will see that the tactic produces a single goal, which Lean has tagged
`intro`

. (The particular name chosen comes from the internal name for
the axiomatic primitive that builds a proof of an existential statement.)
The `case`

tactic then names the components. The second example is similar,
except using `next`

instead of `case`

means that you can avoid mentioning
`intro`

. The word `match`

in the last two examples highlights that
what we are doing here is what computer scientists call “pattern matching.”
Notice that the third proof begins by `by`

, after which the tactic version
of `match`

expects a tactic proof on the right side of the arrow.
The last example is a proof term: there are no tactics in sight.

For the rest of this book, we will stick to `rcases`

, `rintros`

, and `obtain`

,
as the preferred ways of using an existential quantifier.
But it can’t hurt to see the alternative syntax, especially if there is
a chance you will find yourself in the company of computer scientists.

To illustrate one way that `rcases`

can be used,
we prove an old mathematical chestnut:
if two integers `x`

and `y`

can each be written as
a sum of two squares,
then so can their product, `x * y`

.
In fact, the statement is true for any commutative
ring, not just the integers.
In the next example, `rcases`

unpacks two existential
quantifiers at once.
We then provide the magic values needed to express `x * y`

as a sum of squares as a list to the `use`

statement,
and we use `ring`

to verify that they work.

```
variable {α : Type*} [CommRing α]
def SumOfSquares (x : α) :=
∃ a b, x = a ^ 2 + b ^ 2
theorem sumOfSquares_mul {x y : α} (sosx : SumOfSquares x) (sosy : SumOfSquares y) :
SumOfSquares (x * y) := by
rcases sosx with ⟨a, b, xeq⟩
rcases sosy with ⟨c, d, yeq⟩
rw [xeq, yeq]
use a * c - b * d, a * d + b * c
ring
```

This proof doesn’t provide much insight,
but here is one way to motivate it.
A *Gaussian integer* is a number of the form \(a + bi\)
where \(a\) and \(b\) are integers and \(i = \sqrt{-1}\).
The *norm* of the Gaussian integer \(a + bi\) is, by definition,
\(a^2 + b^2\).
So the norm of a Gaussian integer is a sum of squares,
and any sum of squares can be expressed in this way.
The theorem above reflects the fact that norm of a product of
Gaussian integers is the product of their norms:
if \(x\) is the norm of \(a + bi\) and
\(y\) in the norm of \(c + di\),
then \(xy\) is the norm of \((a + bi) (c + di)\).
Our cryptic proof illustrates the fact that
the proof that is easiest to formalize isn’t always
the most perspicuous one.
In Section 6.3,
we will provide you with the means to define the Gaussian
integers and use them to provide an alternative proof.

The pattern of unpacking an equation inside an existential quantifier
and then using it to rewrite an expression in the goal
comes up often,
so much so that the `rcases`

tactic provides
an abbreviation:
if you use the keyword `rfl`

in place of a new identifier,
`rcases`

does the rewriting automatically (this trick doesn’t work
with pattern-matching lambdas).

```
theorem sumOfSquares_mul' {x y : α} (sosx : SumOfSquares x) (sosy : SumOfSquares y) :
SumOfSquares (x * y) := by
rcases sosx with ⟨a, b, rfl⟩
rcases sosy with ⟨c, d, rfl⟩
use a * c - b * d, a * d + b * c
ring
```

As with the universal quantifier, you can find existential quantifiers hidden all over if you know how to spot them. For example, divisibility is implicitly an “exists” statement.

```
example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by
rcases divab with ⟨d, beq⟩
rcases divbc with ⟨e, ceq⟩
rw [ceq, beq]
use d * e; ring
```

And once again, this provides a nice setting for using
`rcases`

with `rfl`

.
Try it out in the proof above.
It feels pretty good!

Then try proving the following:

```
example (divab : a ∣ b) (divac : a ∣ c) : a ∣ b + c := by
sorry
```

For another important example, a function \(f : \alpha \to \beta\)
is said to be *surjective* if for every \(y\) in the
codomain, \(\beta\),
there is an \(x\) in the domain, \(\alpha\),
such that \(f(x) = y\).
Notice that this statement includes both a universal
and an existential quantifier, which explains
why the next example makes use of both `intro`

and `use`

.

```
example {c : ℝ} : Surjective fun x ↦ x + c := by
intro x
use x - c
dsimp; ring
```

Try this example yourself using the theorem `mul_div_cancel₀`

.:

```
example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
sorry
```

At this point, it is worth mentioning that there is a tactic, `field_simp`

,
that will often clear denominators in a useful way.
It can be used in conjunction with the `ring`

tactic.

```
example (x y : ℝ) (h : x - y ≠ 0) : (x ^ 2 - y ^ 2) / (x - y) = x + y := by
field_simp [h]
ring
```

The next example uses a surjectivity hypothesis
by applying it to a suitable value.
Note that you can use `rcases`

with any expression,
not just a hypothesis.

```
example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, f x ^ 2 = 4 := by
rcases h 2 with ⟨x, hx⟩
use x
rw [hx]
norm_num
```

See if you can use these methods to show that the composition of surjective functions is surjective.

```
variable {α : Type*} {β : Type*} {γ : Type*}
variable {g : β → γ} {f : α → β}
example (surjg : Surjective g) (surjf : Surjective f) : Surjective fun x ↦ g (f x) := by
sorry
```

## 3.3. Negation

The symbol `¬`

is meant to express negation,
so `¬ x < y`

says that `x`

is not less than `y`

,
`¬ x = y`

(or, equivalently, `x ≠ y`

) says that
`x`

is not equal to `y`

,
and `¬ ∃ z, x < z ∧ z < y`

says that there does not exist a `z`

strictly between `x`

and `y`

.
In Lean, the notation `¬ A`

abbreviates `A → False`

,
which you can think of as saying that `A`

implies a contradiction.
Practically speaking, this means that you already know something
about how to work with negations:
you can prove `¬ A`

by introducing a hypothesis `h : A`

and proving `False`

,
and if you have `h : ¬ A`

and `h' : A`

,
then applying `h`

to `h'`

yields `False`

.

To illustrate, consider the irreflexivity principle `lt_irrefl`

for a strict order,
which says that we have `¬ a < a`

for every `a`

.
The asymmetry principle `lt_asymm`

says that we have
`a < b → ¬ b < a`

. Let’s show that `lt_asymm`

follows
from `lt_irrefl`

.

```
example (h : a < b) : ¬b < a := by
intro h'
have : a < a := lt_trans h h'
apply lt_irrefl a this
```

This example introduces a couple of new tricks.
First, when you use `have`

without providing
a label,
Lean uses the name `this`

,
providing a convenient way to refer back to it.
Because the proof is so short, we provide an explicit proof term.
But what you should really be paying attention to in this
proof is the result of the `intro`

tactic,
which leaves a goal of `False`

,
and the fact that we eventually prove `False`

by applying `lt_irrefl`

to a proof of `a < a`

.

Here is another example, which uses the
predicate `FnHasUb`

defined in the last section,
which says that a function has an upper bound.

```
example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by
intro fnub
rcases fnub with ⟨a, fnuba⟩
rcases h a with ⟨x, hx⟩
have : f x ≤ a := fnuba x
linarith
```

Remember that it is often convenient to use `linarith`

when a goal follows from linear equations and
inequalities that in the context.

See if you can prove these in a similar way:

```
example (h : ∀ a, ∃ x, f x < a) : ¬FnHasLb f :=
sorry
example : ¬FnHasUb fun x ↦ x :=
sorry
```

Mathlib offers a number of useful theorems for relating orders and negations:

```
#check (not_le_of_gt : a > b → ¬a ≤ b)
#check (not_lt_of_ge : a ≥ b → ¬a < b)
#check (lt_of_not_ge : ¬a ≥ b → a < b)
#check (le_of_not_gt : ¬a > b → a ≤ b)
```

Recall the predicate `Monotone f`

,
which says that `f`

is nondecreasing.
Use some of the theorems just enumerated to prove the following:

```
example (h : Monotone f) (h' : f a < f b) : a < b := by
sorry
example (h : a ≤ b) (h' : f b < f a) : ¬Monotone f := by
sorry
```

We can show that the first example in the last snippet
cannot be proved if we replace `<`

by `≤`

.
Notice that we can prove the negation of a universally
quantified statement by giving a counterexample.
Complete the proof.

```
example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
intro h
let f := fun x : ℝ ↦ (0 : ℝ)
have monof : Monotone f := by sorry
have h' : f 1 ≤ f 0 := le_refl _
sorry
```

This example introduces the `let`

tactic,
which adds a *local definition* to the context.
If you put the cursor after the `let`

command,
in the goal window you will see that the definition
`f : ℝ → ℝ := fun x ↦ 0`

has been added to the context.
Lean will unfold the definition of `f`

when it has to.
In particular, when we prove `f 1 ≤ f 0`

with `le_refl`

,
Lean reduces `f 1`

and `f 0`

to `0`

.

Use `le_of_not_gt`

to prove the following:

```
example (x : ℝ) (h : ∀ ε > 0, x < ε) : x ≤ 0 := by
sorry
```

Implicit in many of the proofs we have just done
is the fact that if `P`

is any property,
saying that there is nothing with property `P`

is the same as saying that everything fails to have
property `P`

,
and saying that not everything has property `P`

is equivalent to saying that something fails to have property `P`

.
In other words, all four of the following implications
are valid (but one of them cannot be proved with what we explained so
far):

```
variable {α : Type*} (P : α → Prop) (Q : Prop)
example (h : ¬∃ x, P x) : ∀ x, ¬P x := by
sorry
example (h : ∀ x, ¬P x) : ¬∃ x, P x := by
sorry
example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
sorry
example (h : ∃ x, ¬P x) : ¬∀ x, P x := by
sorry
```

The first, second, and fourth are straightforward to
prove using the methods you have already seen.
We encourage you to try it.
The third is more difficult, however,
because it concludes that an object exists
from the fact that its nonexistence is contradictory.
This is an instance of *classical* mathematical reasoning.
We can use proof by contradiction
to prove the third implication as follows.

```
example (h : ¬∀ x, P x) : ∃ x, ¬P x := by
by_contra h'
apply h
intro x
show P x
by_contra h''
exact h' ⟨x, h''⟩
```

Make sure you understand how this works.
The `by_contra`

tactic
allows us to prove a goal `Q`

by assuming `¬ Q`

and deriving a contradiction.
In fact, it is equivalent to using the
equivalence `not_not : ¬ ¬ Q ↔ Q`

.
Confirm that you can prove the forward direction
of this equivalence using `by_contra`

,
while the reverse direction follows from the
ordinary rules for negation.

```
example (h : ¬¬Q) : Q := by
sorry
example (h : Q) : ¬¬Q := by
sorry
```

Use proof by contradiction to establish the following,
which is the converse of one of the implications we proved above.
(Hint: use `intro`

first.)

```
example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
sorry
```

It is often tedious to work with compound statements with
a negation in front,
and it is a common mathematical pattern to replace such
statements with equivalent forms in which the negation
has been pushed inward.
To facilitate this, Mathlib offers a `push_neg`

tactic,
which restates the goal in this way.
The command `push_neg at h`

restates the hypothesis `h`

.

```
example (h : ¬∀ a, ∃ x, f x > a) : FnHasUb f := by
push_neg at h
exact h
example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
dsimp only [FnHasUb, FnUb] at h
push_neg at h
exact h
```

In the second example, we use dsimp to
expand the definitions of `FnHasUb`

and `FnUb`

.
(We need to use `dsimp`

rather than `rw`

to expand `FnUb`

,
because it appears in the scope of a quantifier.)
You can verify that in the examples above
with `¬∃ x, P x`

and `¬∀ x, P x`

,
the `push_neg`

tactic does the expected thing.
Without even knowing how to use the conjunction
symbol,
you should be able to use `push_neg`

to prove the following:

```
example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by
sorry
```

Mathlib also has a tactic, `contrapose`

,
which transforms a goal `A → B`

to `¬B → ¬A`

.
Similarly, given a goal of proving `B`

from
hypothesis `h : A`

,
`contrapose h`

leaves you with a goal of proving
`¬A`

from hypothesis `¬B`

.
Using `contrapose!`

instead of `contrapose`

applies `push_neg`

to the goal and the relevant
hypothesis as well.

```
example (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by
contrapose! h
exact h
example (x : ℝ) (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by
contrapose! h
use x / 2
constructor <;> linarith
```

We have not yet explained the `constructor`

command
or the use of the semicolon after it,
but we will do that in the next section.

We close this section with
the principle of *ex falso*,
which says that anything follows from a contradiction.
In Lean, this is represented by `False.elim`

,
which establishes `False → P`

for any proposition `P`

.
This may seem like a strange principle,
but it comes up fairly often.
We often prove a theorem by splitting on cases,
and sometimes we can show that one of
the cases is contradictory.
In that case, we need to assert that the contradiction
establishes the goal so we can move on to the next one.
(We will see instances of reasoning by cases in
Section 3.5.)

Lean provides a number of ways of closing a goal once a contradiction has been reached.

```
example (h : 0 < 0) : a > 37 := by
exfalso
apply lt_irrefl 0 h
example (h : 0 < 0) : a > 37 :=
absurd h (lt_irrefl 0)
example (h : 0 < 0) : a > 37 := by
have h' : ¬0 < 0 := lt_irrefl 0
contradiction
```

The `exfalso`

tactic replaces the current goal with
the goal of proving `False`

.
Given `h : P`

and `h' : ¬ P`

,
the term `absurd h h'`

establishes any proposition.
Finally, the `contradiction`

tactic tries to close a goal
by finding a contradiction in the hypotheses,
such as a pair of the form `h : P`

and `h' : ¬ P`

.
Of course, in this example, `linarith`

also works.

## 3.4. Conjunction and Iff

You have already seen that the conjunction symbol, `∧`

,
is used to express “and.”
The `constructor`

tactic allows you to prove a statement of
the form `A ∧ B`

by proving `A`

and then proving `B`

.

```
example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by
constructor
· assumption
intro h
apply h₁
rw [h]
```

In this example, the `assumption`

tactic
tells Lean to find an assumption that will solve the goal.
Notice that the final `rw`

finishes the goal by
applying the reflexivity of `≤`

.
The following are alternative ways of carrying out
the previous examples using the anonymous constructor
angle brackets.
The first is a slick proof-term version of the
previous proof,
which drops into tactic mode at the keyword `by`

.

```
example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y :=
⟨h₀, fun h ↦ h₁ (by rw [h])⟩
example {x y : ℝ} (h₀ : x ≤ y) (h₁ : ¬y ≤ x) : x ≤ y ∧ x ≠ y :=
have h : x ≠ y := by
contrapose! h₁
rw [h₁]
⟨h₀, h⟩
```

*Using* a conjunction instead of proving one involves unpacking the proofs of the
two parts.
You can use the `rcases`

tactic for that,
as well as `rintro`

or a pattern-matching `fun`

,
all in a manner similar to the way they are used with
the existential quantifier.

```
example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
rcases h with ⟨h₀, h₁⟩
contrapose! h₁
exact le_antisymm h₀ h₁
example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬y ≤ x := by
rintro ⟨h₀, h₁⟩ h'
exact h₁ (le_antisymm h₀ h')
example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬y ≤ x :=
fun ⟨h₀, h₁⟩ h' ↦ h₁ (le_antisymm h₀ h')
```

In analogy to the `obtain`

tactic, there is also a pattern-matching `have`

:

```
example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
have ⟨h₀, h₁⟩ := h
contrapose! h₁
exact le_antisymm h₀ h₁
```

In contrast to `rcases`

, here the `have`

tactic leaves `h`

in the context.
And even though we won’t use them, once again we have the computer scientists’
pattern-matching syntax:

```
example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
cases h
case intro h₀ h₁ =>
contrapose! h₁
exact le_antisymm h₀ h₁
example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
cases h
next h₀ h₁ =>
contrapose! h₁
exact le_antisymm h₀ h₁
example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
match h with
| ⟨h₀, h₁⟩ =>
contrapose! h₁
exact le_antisymm h₀ h₁
```

In contrast to using an existential quantifier,
you can also extract proofs of the two components
of a hypothesis `h : A ∧ B`

by writing `h.left`

and `h.right`

,
or, equivalently, `h.1`

and `h.2`

.

```
example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
intro h'
apply h.right
exact le_antisymm h.left h'
example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x :=
fun h' ↦ h.right (le_antisymm h.left h')
```

Try using these techniques to come up with various ways of proving of the following:

```
example {m n : ℕ} (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬n ∣ m :=
sorry
```

You can nest uses of `∃`

and `∧`

with anonymous constructors, `rintro`

, and `rcases`

.

```
example : ∃ x : ℝ, 2 < x ∧ x < 4 :=
⟨5 / 2, by norm_num, by norm_num⟩
example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y := by
rintro ⟨z, xltz, zlty⟩
exact lt_trans xltz zlty
example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y :=
fun ⟨z, xltz, zlty⟩ ↦ lt_trans xltz zlty
```

You can also use the `use`

tactic:

```
example : ∃ x : ℝ, 2 < x ∧ x < 4 := by
use 5 / 2
constructor <;> norm_num
example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by
use 5
use 7
norm_num
example {x y : ℝ} : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬y ≤ x := by
rintro ⟨h₀, h₁⟩
use h₀
exact fun h' ↦ h₁ (le_antisymm h₀ h')
```

In the first example, the semicolon after the `constructor`

command tells Lean to use the
`norm_num`

tactic on both of the goals that result.

In Lean, `A ↔ B`

is *not* defined to be `(A → B) ∧ (B → A)`

,
but it could have been,
and it behaves roughly the same way.
You have already seen that you can write `h.mp`

and `h.mpr`

or `h.1`

and `h.2`

for the two directions of `h : A ↔ B`

.
You can also use `cases`

and friends.
To prove an if-and-only-if statement,
you can uses `constructor`

or angle brackets,
just as you would if you were proving a conjunction.

```
example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by
constructor
· contrapose!
rintro rfl
rfl
contrapose!
exact le_antisymm h
example {x y : ℝ} (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y :=
⟨fun h₀ h₁ ↦ h₀ (by rw [h₁]), fun h₀ h₁ ↦ h₀ (le_antisymm h h₁)⟩
```

The last proof term is inscrutable. Remember that you can use underscores while writing an expression like that to see what Lean expects.

Try out the various techniques and gadgets you have just seen in order to prove the following:

```
example {x y : ℝ} : x ≤ y ∧ ¬y ≤ x ↔ x ≤ y ∧ x ≠ y :=
sorry
```

For a more interesting exercise, show that for any
two real numbers `x`

and `y`

,
`x^2 + y^2 = 0`

if and only if `x = 0`

and `y = 0`

.
We suggest proving an auxiliary lemma using
`linarith`

, `pow_two_nonneg`

, and `pow_eq_zero`

.

```
theorem aux {x y : ℝ} (h : x ^ 2 + y ^ 2 = 0) : x = 0 :=
have h' : x ^ 2 = 0 := by sorry
pow_eq_zero h'
example (x y : ℝ) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 :=
sorry
```

In Lean, bi-implication leads a double-life.
You can treat it like a conjunction and use its two
parts separately.
But Lean also knows that it is a reflexive, symmetric,
and transitive relation between propositions,
and you can also use it with `calc`

and `rw`

.
It is often convenient to rewrite a statement to
an equivalent one.
In the next example, we use `abs_lt`

to
replace an expression of the form `|x| < y`

by the equivalent expression `- y < x ∧ x < y`

,
and in the one after that we use `Nat.dvd_gcd_iff`

to replace an expression of the form `m ∣ Nat.gcd n k`

by the equivalent expression `m ∣ n ∧ m ∣ k`

.

```
example (x : ℝ) : |x + 3| < 5 → -8 < x ∧ x < 2 := by
rw [abs_lt]
intro h
constructor <;> linarith
example : 3 ∣ Nat.gcd 6 15 := by
rw [Nat.dvd_gcd_iff]
constructor <;> norm_num
```

See if you can use `rw`

with the theorem below
to provide a short proof that negation is not a
nondecreasing function. (Note that `push_neg`

won’t
unfold definitions for you, so the `rw [Monotone]`

in
the proof of the theorem is needed.)

```
theorem not_monotone_iff {f : ℝ → ℝ} : ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y := by
rw [Monotone]
push_neg
rfl
example : ¬Monotone fun x : ℝ ↦ -x := by
sorry
```

The remaining exercises in this section are designed
to give you some more practice with conjunction and
bi-implication. Remember that a *partial order* is a
binary relation that is transitive, reflexive, and
antisymmetric.
An even weaker notion sometimes arises:
a *preorder* is just a reflexive, transitive relation.
For any pre-order `≤`

,
Lean axiomatizes the associated strict pre-order by
`a < b ↔ a ≤ b ∧ ¬ b ≤ a`

.
Show that if `≤`

is a partial order,
then `a < b`

is equivalent to `a ≤ b ∧ a ≠ b`

:

```
variable {α : Type*} [PartialOrder α]
variable (a b : α)
example : a < b ↔ a ≤ b ∧ a ≠ b := by
rw [lt_iff_le_not_le]
sorry
```

Beyond logical operations, you do not need
anything more than `le_refl`

and `le_trans`

.
Show that even in the case where `≤`

is only assumed to be a preorder,
we can prove that the strict order is irreflexive
and transitive.
In the second example,
for convenience, we use the simplifier rather than `rw`

to express `<`

in terms of `≤`

and `¬`

.
We will come back to the simplifier later,
but here we are only relying on the fact that it will
use the indicated lemma repeatedly, even if it needs
to be instantiated to different values.

```
variable {α : Type*} [Preorder α]
variable (a b c : α)
example : ¬a < a := by
rw [lt_iff_le_not_le]
sorry
example : a < b → b < c → a < c := by
simp only [lt_iff_le_not_le]
sorry
```

## 3.5. Disjunction

The canonical way to prove a disjunction `A ∨ B`

is to prove
`A`

or to prove `B`

.
The `left`

tactic chooses `A`

,
and the `right`

tactic chooses `B`

.

```
variable {x y : ℝ}
example (h : y > x ^ 2) : y > 0 ∨ y < -1 := by
left
linarith [pow_two_nonneg x]
example (h : -y > x ^ 2 + 1) : y > 0 ∨ y < -1 := by
right
linarith [pow_two_nonneg x]
```

We cannot use an anonymous constructor to construct a proof
of an “or” because Lean would have to guess
which disjunct we are trying to prove.
When we write proof terms we can use
`Or.inl`

and `Or.inr`

instead
to make the choice explicitly.
Here, `inl`

is short for “introduction left” and
`inr`

is short for “introduction right.”

```
example (h : y > 0) : y > 0 ∨ y < -1 :=
Or.inl h
example (h : y < -1) : y > 0 ∨ y < -1 :=
Or.inr h
```

It may seem strange to prove a disjunction by proving one side
or the other.
In practice, which case holds usually depends on a case distinction
that is implicit or explicit in the assumptions and the data.
The `rcases`

tactic allows us to make use of a hypothesis
of the form `A ∨ B`

.
In contrast to the use of `rcases`

with conjunction or an
existential quantifier,
here the `rcases`

tactic produces *two* goals.
Both have the same conclusion, but in the first case,
`A`

is assumed to be true,
and in the second case,
`B`

is assumed to be true.
In other words, as the name suggests,
the `rcases`

tactic carries out a proof by cases.
As usual, we can tell Lean what names to use for the hypotheses.
In the next example, we tell Lean
to use the name `h`

on each branch.

```
example : x < |y| → x < y ∨ x < -y := by
rcases le_or_gt 0 y with h | h
· rw [abs_of_nonneg h]
intro h; left; exact h
. rw [abs_of_neg h]
intro h; right; exact h
```

Notice that the pattern changes from `⟨h₀, h₁⟩`

in the case of
a conjunction to `h₀ | h₁`

in the case of a disjunction.
Think of the first pattern as matching against data the contains
*both* an `h₀`

and a `h₁`

, whereas second pattern, with the bar,
matches against data that contains *either* an `h₀`

or `h₁`

.
In this case, because the two goals are separate, we have chosen
to use the same name, `h`

, in each case.

The absolute value function is defined in such a way
that we can immediately prove that
`x ≥ 0`

implies `|x| = x`

(this is the theorem `abs_of_nonneg`

)
and `x < 0`

implies `|x| = -x`

(this is `abs_of_neg`

).
The expression `le_or_gt 0 x`

establishes `0 ≤ x ∨ x < 0`

,
allowing us to split on those two cases.

Lean also supports the computer scientists’ pattern-matching
syntax for disjunction. Now the `cases`

tactic is more attractive,
because it allows us to name each `case`

, and name the hypothesis
that is introduced closer to where it is used.

```
example : x < |y| → x < y ∨ x < -y := by
cases le_or_gt 0 y
case inl h =>
rw [abs_of_nonneg h]
intro h; left; exact h
case inr h =>
rw [abs_of_neg h]
intro h; right; exact h
```

The names `inl`

and `inr`

are short for “intro left” and “intro right,”
respectively. Using `case`

has the advantage is that you can prove the
cases in either order; Lean uses the tag to find the relevant goal.
If you don’t care about that, you can use `next`

, or `match`

,
or even a pattern-matching `have`

.

```
example : x < |y| → x < y ∨ x < -y := by
cases le_or_gt 0 y
next h =>
rw [abs_of_nonneg h]
intro h; left; exact h
next h =>
rw [abs_of_neg h]
intro h; right; exact h
example : x < |y| → x < y ∨ x < -y := by
match le_or_gt 0 y with
| Or.inl h =>
rw [abs_of_nonneg h]
intro h; left; exact h
| Or.inr h =>
rw [abs_of_neg h]
intro h; right; exact h
```

In the case of the `match`

, we need to use the full names
`Or.inl`

and `Or.inr`

of the canonical ways to prove a disjunction.
In this textbook, we will generally use `rcases`

to split on the
cases of a disjunction.

Try proving the triangle inequality using the two first two theorems in the next snippet. They are given the same names they have in Mathlib.

```
namespace MyAbs
theorem le_abs_self (x : ℝ) : x ≤ |x| := by
sorry
theorem neg_le_abs_self (x : ℝ) : -x ≤ |x| := by
sorry
theorem abs_add (x y : ℝ) : |x + y| ≤ |x| + |y| := by
sorry
```

In case you enjoyed these (pun intended) and you want more practice with disjunction, try these.

```
theorem lt_abs : x < |y| ↔ x < y ∨ x < -y := by
sorry
theorem abs_lt : |x| < y ↔ -y < x ∧ x < y := by
sorry
```

You can also use `rcases`

and `rintro`

with nested disjunctions.
When these result in a genuine case split with multiple goals,
the patterns for each new goal are separated by a vertical bar.

```
example {x : ℝ} (h : x ≠ 0) : x < 0 ∨ x > 0 := by
rcases lt_trichotomy x 0 with xlt | xeq | xgt
· left
exact xlt
· contradiction
. right; exact xgt
```

You can still nest patterns and use the `rfl`

keyword
to substitute equations:

```
example {m n k : ℕ} (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by
rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩
· rw [mul_assoc]
apply dvd_mul_right
. rw [mul_comm, mul_assoc]
apply dvd_mul_right
```

See if you can prove the following with a single (long) line.
Use `rcases`

to unpack the hypotheses and split on cases,
and use a semicolon and `linarith`

to solve each branch.

```
example {z : ℝ} (h : ∃ x y, z = x ^ 2 + y ^ 2 ∨ z = x ^ 2 + y ^ 2 + 1) : z ≥ 0 := by
sorry
```

On the real numbers, an equation `x * y = 0`

tells us that `x = 0`

or `y = 0`

.
In Mathlib, this fact is known as `eq_zero_or_eq_zero_of_mul_eq_zero`

,
and it is another nice example of how a disjunction can arise.
See if you can use it to prove the following:

```
example {x : ℝ} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
sorry
example {x y : ℝ} (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
sorry
```

Remember that you can use the `ring`

tactic to help
with calculations.

In an arbitrary ring \(R\), an element \(x\) such
that \(x y = 0\) for some nonzero \(y\) is called
a *left zero divisor*,
an element \(x\) such
that \(y x = 0\) for some nonzero \(y\) is called
a *right zero divisor*,
and an element that is either a left or right zero divisor
is called simply a *zero divisor*.
The theorem `eq_zero_or_eq_zero_of_mul_eq_zero`

says that the real numbers have no nontrivial zero divisors.
A commutative ring with this property is called an *integral domain*.
Your proofs of the two theorems above should work equally well
in any integral domain:

```
variable {R : Type*} [CommRing R] [IsDomain R]
variable (x y : R)
example (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
sorry
example (h : x ^ 2 = y ^ 2) : x = y ∨ x = -y := by
sorry
```

In fact, if you are careful, you can prove the first
theorem without using commutativity of multiplication.
In that case, it suffices to assume that `R`

is
a `Ring`

instead of an `CommRing`

.

Sometimes in a proof we want to split on cases
depending on whether some statement is true or not.
For any proposition `P`

, we can use
`em P : P ∨ ¬ P`

.
The name `em`

is short for “excluded middle.”

```
example (P : Prop) : ¬¬P → P := by
intro h
cases em P
· assumption
. contradiction
```

Alternatively, you can use the `by_cases`

tactic.

```
example (P : Prop) : ¬¬P → P := by
intro h
by_cases h' : P
· assumption
contradiction
```

Notice that the `by_cases`

tactic lets you
specify a label for the hypothesis that is
introduced in each branch,
in this case, `h' : P`

in one and `h' : ¬ P`

in the other.
If you leave out the label,
Lean uses `h`

by default.
Try proving the following equivalence,
using `by_cases`

to establish one direction.

```
example (P Q : Prop) : P → Q ↔ ¬P ∨ Q := by
sorry
```

## 3.6. Sequences and Convergence

We now have enough skills at our disposal to do some real mathematics.
In Lean, we can represent a sequence \(s_0, s_1, s_2, \ldots\) of
real numbers as a function `s : ℕ → ℝ`

.
Such a sequence is said to *converge* to a number \(a\) if for every
\(\varepsilon > 0\) there is a point beyond which the sequence
remains within \(\varepsilon\) of \(a\),
that is, there is a number \(N\) such that for every
\(n \ge N\), \(| s_n - a | < \varepsilon\).
In Lean, we can render this as follows:

```
def ConvergesTo (s : ℕ → ℝ) (a : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε
```

The notation `∀ ε > 0, ...`

is a convenient abbreviation
for `∀ ε, ε > 0 → ...`

, and, similarly,
`∀ n ≥ N, ...`

abbreviates `∀ n, n ≥ N → ...`

.
And remember that `ε > 0`

, in turn, is defined as `0 < ε`

,
and `n ≥ N`

is defined as `N ≤ n`

.

In this section, we’ll establish some properties of convergence.
But first, we will discuss three tactics for working with equality
that will prove useful.
The first, the `ext`

tactic,
gives us a way of proving that two functions are equal.
Let \(f(x) = x + 1\) and \(g(x) = 1 + x\)
be functions from reals to reals.
Then, of course, \(f = g\), because they return the same
value for every \(x\).
The `ext`

tactic enables us to prove an equation between functions
by proving that their values are the same
at all the values of their arguments.

```
example : (fun x y : ℝ ↦ (x + y) ^ 2) = fun x y : ℝ ↦ x ^ 2 + 2 * x * y + y ^ 2 := by
ext
ring
```

We’ll see later that `ext`

is actually more general, and also one can
specify the name of the variables that appear.
For instance you can try to replace `ext`

with `ext u v`

in the
above proof.
The second tactic, the `congr`

tactic,
allows us to prove an equation between two expressions
by reconciling the parts that are different:

```
example (a b : ℝ) : |a| = |a - b + b| := by
congr
ring
```

Here the `congr`

tactic peels off the `abs`

on each side,
leaving us to prove `a = a - b + b`

.

Finally, the `convert`

tactic is used to apply a theorem
to a goal when the conclusion of the theorem doesn’t quite match.
For example, suppose we want to prove `a < a * a`

from `1 < a`

.
A theorem in the library, `mul_lt_mul_right`

,
will let us prove `1 * a < a * a`

.
One possibility is to work backwards and rewrite the goal
so that it has that form.
Instead, the `convert`

tactic lets us apply the theorem
as it is,
and leaves us with the task of proving the equations that
are needed to make the goal match.

```
example {a : ℝ} (h : 1 < a) : a < a * a := by
convert (mul_lt_mul_right _).2 h
· rw [one_mul]
exact lt_trans zero_lt_one h
```

This example illustrates another useful trick: when we apply an expression with an underscore and Lean can’t fill it in for us automatically, it simply leaves it for us as another goal.

The following shows that any constant sequence \(a, a, a, \ldots\) converges.

```
theorem convergesTo_const (a : ℝ) : ConvergesTo (fun x : ℕ ↦ a) a := by
intro ε εpos
use 0
intro n nge
rw [sub_self, abs_zero]
apply εpos
```

Lean has a tactic, `simp`

, which can often save you the
trouble of carrying out steps like `rw [sub_self, abs_zero]`

by hand.
We will tell you more about it soon.

For a more interesting theorem, let’s show that if `s`

converges to `a`

and `t`

converges to `b`

, then
`fun n ↦ s n + t n`

converges to `a + b`

.
It is helpful to have a clear pen-and-paper
proof in mind before you start writing a formal one.
Given `ε`

greater than `0`

,
the idea is to use the hypotheses to obtain an `Ns`

such that beyond that point, `s`

is within `ε / 2`

of `a`

,
and an `Nt`

such that beyond that point, `t`

is within
`ε / 2`

of `b`

.
Then, whenever `n`

is greater than or equal to the
maximum of `Ns`

and `Nt`

,
the sequence `fun n ↦ s n + t n`

should be within `ε`

of `a + b`

.
The following example begins to implement this strategy.
See if you can finish it off.

```
theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ}
(cs : ConvergesTo s a) (ct : ConvergesTo t b) :
ConvergesTo (fun n ↦ s n + t n) (a + b) := by
intro ε εpos
dsimp -- this line is not needed but cleans up the goal a bit.
have ε2pos : 0 < ε / 2 := by linarith
rcases cs (ε / 2) ε2pos with ⟨Ns, hs⟩
rcases ct (ε / 2) ε2pos with ⟨Nt, ht⟩
use max Ns Nt
sorry
```

As hints, you can use `le_of_max_le_left`

and `le_of_max_le_right`

,
and `norm_num`

can prove `ε / 2 + ε / 2 = ε`

.
Also, it is helpful to use the `congr`

tactic to
show that `|s n + t n - (a + b)|`

is equal to
`|(s n - a) + (t n - b)|,`

since then you can use the triangle inequality.
Notice that we marked all the variables `s`

, `t`

, `a`

, and `b`

implicit because they can be inferred from the hypotheses.

Proving the same theorem with multiplication in place
of addition is tricky.
We will get there by proving some auxiliary statements first.
See if you can also finish off the next proof,
which shows that if `s`

converges to `a`

,
then `fun n ↦ c * s n`

converges to `c * a`

.
It is helpful to split into cases depending on whether `c`

is equal to zero or not.
We have taken care of the zero case,
and we have left you to prove the result with
the extra assumption that `c`

is nonzero.

```
theorem convergesTo_mul_const {s : ℕ → ℝ} {a : ℝ} (c : ℝ) (cs : ConvergesTo s a) :
ConvergesTo (fun n ↦ c * s n) (c * a) := by
by_cases h : c = 0
· convert convergesTo_const 0
· rw [h]
ring
rw [h]
ring
have acpos : 0 < |c| := abs_pos.mpr h
sorry
```

The next theorem is also independently interesting: it shows that a convergent sequence is eventually bounded in absolute value. We have started you off; see if you can finish it.

```
theorem exists_abs_le_of_convergesTo {s : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) :
∃ N b, ∀ n, N ≤ n → |s n| < b := by
rcases cs 1 zero_lt_one with ⟨N, h⟩
use N, |a| + 1
sorry
```

In fact, the theorem could be strengthened to assert
that there is a bound `b`

that holds for all values of `n`

.
But this version is strong enough for our purposes,
and we will see at the end of this section that it
holds more generally.

The next lemma is auxiliary: we prove that if
`s`

converges to `a`

and `t`

converges to `0`

,
then `fun n ↦ s n * t n`

converges to `0`

.
To do so, we use the previous theorem to find a `B`

that bounds `s`

beyond some point `N₀`

.
See if you can understand the strategy we have outlined
and finish the proof.

```
theorem aux {s t : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t 0) :
ConvergesTo (fun n ↦ s n * t n) 0 := by
intro ε εpos
dsimp
rcases exists_abs_le_of_convergesTo cs with ⟨N₀, B, h₀⟩
have Bpos : 0 < B := lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _))
have pos₀ : ε / B > 0 := div_pos εpos Bpos
rcases ct _ pos₀ with ⟨N₁, h₁⟩
sorry
```

If you have made it this far, congratulations! We are now within striking distance of our theorem. The following proof finishes it off.

```
theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ}
(cs : ConvergesTo s a) (ct : ConvergesTo t b) :
ConvergesTo (fun n ↦ s n * t n) (a * b) := by
have h₁ : ConvergesTo (fun n ↦ s n * (t n + -b)) 0 := by
apply aux cs
convert convergesTo_add ct (convergesTo_const (-b))
ring
have := convergesTo_add h₁ (convergesTo_mul_const b cs)
convert convergesTo_add h₁ (convergesTo_mul_const b cs) using 1
· ext; ring
ring
```

For another challenging exercise, try filling out the following sketch of a proof that limits are unique. (If you are feeling bold, you can delete the proof sketch and try proving it from scratch.)

```
theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ}
(sa : ConvergesTo s a) (sb : ConvergesTo s b) :
a = b := by
by_contra abne
have : |a - b| > 0 := by sorry
let ε := |a - b| / 2
have εpos : ε > 0 := by
change |a - b| / 2 > 0
linarith
rcases sa ε εpos with ⟨Na, hNa⟩
rcases sb ε εpos with ⟨Nb, hNb⟩
let N := max Na Nb
have absa : |s N - a| < ε := by sorry
have absb : |s N - b| < ε := by sorry
have : |a - b| < |a - b| := by sorry
exact lt_irrefl _ this
```

We close the section with the observation that our proofs can be generalized.
For example, the only properties that we have used of the
natural numbers is that their structure carries a partial order
with `min`

and `max`

.
You can check that everything still works if you replace `ℕ`

everywhere by any linear order `α`

:

```
variable {α : Type*} [LinearOrder α]
def ConvergesTo' (s : α → ℝ) (a : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |s n - a| < ε
```

In Section 9.1, we will see that Mathlib has mechanisms for dealing with convergence in vastly more general terms, not only abstracting away particular features of the domain and codomain, but also abstracting over different types of convergence.