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 → abs 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 → abs x < ε → abs y < ε → abs (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 abs 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:

lemma my_lemma : ∀ x y ε : ℝ,
  0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε :=
sorry

section
  variables a b δ : ℝ
  variables (h₀ : 0 < δ) (h₁ : δ ≤ 1)
  variables (ha : abs a < δ) (hb : abs 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.

lemma my_lemma2 : ∀ {x y ε : ℝ},
  0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε :=
sorry

section
  variables a b δ : ℝ
  variables (h₀ : 0 < δ) (h₁ : δ ≤ 1)
  variables (ha : abs a < δ) (hb : abs 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 abs (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 intros tactic. Take a look at what it does in this example:

lemma my_lemma3 : ∀ {x y ε : ℝ},
  0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε :=
begin
  intros x y ε epos ele1 xlt ylt,
  sorry
end

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 intros 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:

lemma my_lemma4 : ∀ {x y ε : ℝ},
  0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε :=
begin
  intros x y ε epos ele1 xlt ylt,
  calc
    abs (x * y) = abs x * abs y : sorry
    ... ≤ abs x * ε             : sorry
    ... < 1 * ε                 : sorry
    ... = ε                     : sorry
end

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 tab completion. 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, fn_ub f a and fn_lb 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 fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a
def fn_lb (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x

In the next example, λ x, f x + g x is a name for the function that maps x to f x + g x. Computer scientists refer to this as “lambda abstraction,” whereas a mathematician might describe it as the function \(x \mapsto f(x) + g(x)\).

example (hfa : fn_ub f a) (hgb : fn_ub g b) :
  fn_ub (λ x, f x + g x) (a + b) :=
begin
  intro x,
  dsimp,
  apply add_le_add,
  apply hfa,
  apply hgb
end

Applying intro to the goal fn_ub (λ x, f x + g x) (a + b) forces Lean to unfold the definition of fn_ub and introduce x for the universal quantifier. The goal is then (λ (x : ℝ), f x + g x) x ≤ a + b. But applying (λ 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 fn_ub in the hypotheses. Try carrying out similar proofs of these:

example (hfa : fn_lb f a) (hgb : fn_lb g b) :
  fn_lb (λ x, f x + g x) (a + b) :=
sorry

example (nnf : fn_lb f 0) (nng : fn_lb g 0) :
  fn_lb (λ x, f x * g x) 0 :=
sorry

example (hfa : fn_ub f a) (hfb : fn_ub g b)
    (nng : fn_lb g 0) (nna : 0 ≤ a) :
  fn_ub (λ x, f x * g x) (a * b) :=
sorry

Even though we have defined fn_ub and fn_lb 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 fn_ub_add at that level of generality, it will apply in all these instances.

variables {α : Type*} {R : Type*} [ordered_cancel_add_comm_monoid R]

#check @add_le_add

def fn_ub' (f : α → R) (a : R) : Prop := ∀ x, f x ≤ a

theorem fn_ub_add {f g : α → R} {a b : R}
    (hfa : fn_ub' f a) (hgb : fn_ub' g b) :
  fn_ub' (λ x, f x + g x) (a + b) :=
λ 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

Proving statements about monotonicity involves using intros 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 (λ x, f x + g x) :=
begin
  intros a b aleb,
  apply add_le_add,
  apply mf aleb,
  apply mg aleb
end

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 λ a b aleb, .... This is analogous to the way that a lambda abstraction like λ x, x^2 describes a function by temporarily naming an object, x, and then using it to describe a value. So the intros 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 (λ x, f x + g x) :=
λ a b aleb, add_le_add (mf aleb) (mg aleb)

Here is a useful trick: if you start writing the proof term λ 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 (λ x, c * f x) :=
sorry

example (mf : monotone f) (mg : monotone g) :
  monotone (λ 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 fn_even (f : ℝ → ℝ) : Prop := ∀ x, f x = f (-x)
def fn_odd (f : ℝ → ℝ) : Prop := ∀ x, f x = - f (-x)

example (ef : fn_even f) (eg : fn_even g) : fn_even (λ x, f x + g x) :=
begin
  intro x,
  calc
    (λ x, f x + g x) x = f x + g x       : rfl
                    ... = f (-x) + g (-x) : by rw [ef, eg]
end

example (of : fn_odd f) (og : fn_odd g) : fn_even (λ x, f x * g x) :=
sorry

example (ef : fn_even f) (og : fn_odd g) : fn_odd (λ x, f x * g x) :=
sorry

example (ef : fn_even f) (og : fn_odd g) : fn_even (λ x, f (g x)) :=
sorry

The first proof can be shortened using dsimp or change to get rid of the lambda. But you can check that the subsequent rw won’t work unless we get rid of the lambda 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 rudimentary set theory. Lean’s logical foundation imposes the restriction that when we talk about sets, we are always talking about sets of elements of some 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 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.

variables {α : Type*} (r s t : set α)

example : s ⊆ s :=
by { intros x xs, exact xs }

theorem subset.refl : s ⊆ s := λ x xs, xs

theorem subset.trans : r ⊆ s → s ⊆ t → r ⊆ t :=
sorry

Just as we defined fn_ub for functions, we can define set_ub 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.

variables {α : Type*} [partial_order α]
variables (s : set α) (a b : α)

def set_ub (s : set α) (a : α) := ∀ x, x ∈ s → x ≤ a

example (h : set_ub s a) (h' : a ≤ b) : set_ub 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.

open function

example (c : ℝ) : injective (λ x, x + c) :=
begin
  intros x₁ x₂ h',
  exact (add_left_inj c).mp h',
end

example {c : ℝ} (h : c ≠ 0) : injective (λ x, c * x) :=
sorry

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

variables {α : Type*} {β : Type*} {γ : Type*}
variables {g : β → γ} {f : α → β}

example (injg : injective g) (injf : injective f) :
  injective (λ x, g (f x)) :=
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 :=
begin
  use 5 / 2,
  norm_num
end

Alternatively, we can use Lean’s anonyomous constructor notation to construct the proof.

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

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 fn_ub f a and fn_lb 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 fn_ub (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a
def fn_lb (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x

def fn_has_ub (f : ℝ → ℝ) := ∃ a, fn_ub f a
def fn_has_lb (f : ℝ → ℝ) := ∃ a, fn_lb f a

We can use the theorem fn_ub_add from the last section to prove that if f and g have upper bounds, then so does λ x, f x + g x.

variables {f g : ℝ → ℝ}

example (ubf : fn_has_ub f) (ubg : fn_has_ub g) :
  fn_has_ub (λ x, f x + g x) :=
begin
  cases ubf with a ubfa,
  cases ubg with b ubfb,
  use a + b,
  apply fn_ub_add ubfa ubfb
end

The cases tactic unpacks the information in the existential quantifier. Given the hypothesis ubf that there is an upper bound for f, cases adds a new variable for an upper bound to the context, together with the hypothesis that it has the given property. The with clause allows us to specify the names we want Lean to use. 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 pattern 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 pattern 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 : fn_has_lb f) (lbg : fn_has_lb g) :
  fn_has_lb (λ x, f x + g x) :=
sorry

example {c : ℝ} (ubf : fn_has_ub f) (h : c ≥ 0):
  fn_has_ub (λ x, c * f x) :=
sorry

The task of unpacking information in a hypothesis is so important that Lean and mathlib provide a number of ways to do it. A cousin of the cases tactic, rcases, is more flexible in that it allows us to unpack nested data. (The “r” stands for “recursive.”) In the with clause for unpacking an existential quantifier, we name the object and the hypothesis by presenting them as a pattern ⟨a, h⟩ that rcases then tries to match. The rintro tactic (which can also be written rintros) is a combination of intros and rcases. These examples illustrate their use:

example (ubf : fn_has_ub f) (ubg : fn_has_ub g) :
  fn_has_ub (λ x, f x + g x) :=
begin
  rcases ubf with ⟨a, ubfa⟩,
  rcases ubg with ⟨b, ubfb⟩,
  exact ⟨a + b, fn_ub_add ubfa ubfb⟩
end

example : fn_has_ub f → fn_has_ub g →
  fn_has_ub (λ x, f x + g x) :=
begin
  rintros ⟨a, ubfa⟩ ⟨b, ubfb⟩,
  exact ⟨a + b, fn_ub_add ubfa ubfb⟩
end

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

example : fn_has_ub f → fn_has_ub g →
  fn_has_ub (λ x, f x + g x) :=
λ ⟨a, ubfa⟩ ⟨b, ubfb⟩, ⟨a + b, fn_ub_add ubfa ubfb⟩

These are power-user moves, and there is no harm in favoring the use of cases until you are more comfortable with the existential quantifier. But we will come to learn that all of these tools, including cases, use, and the anonymous constructors, are like Swiss army knives when it comes to theorem proving. They can be used for a wide range of purposes, not just for unpacking exists statements.

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.

variables {α : Type*} [comm_ring α]

def sum_of_squares (x : α) := ∃ a b, x = a^2 + b^2

theorem sum_of_squares_mul {x y : α}
    (sosx : sum_of_squares x) (sosy : sum_of_squares y) :
  sum_of_squares (x * y) :=
begin
  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
end

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 the chapters to come, 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 sum_of_squares_mul' {x y : α}
    (sosx : sum_of_squares x) (sosy : sum_of_squares y) :
  sum_of_squares (x * y) :=
begin
  rcases sosx with ⟨a, b, rfl⟩,
  rcases sosy with ⟨c, d, rfl⟩,
  use [a*c - b*d, a*d + b*c],
  ring
end

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 :=
begin
  cases divab with d beq,
  cases divbc with e ceq,
  rw [ceq, beq],
  use (d * e), ring
end

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) :=
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 (λ x, x + c) :=
begin
  intro x,
  use x - c,
  dsimp, ring
end

Try this example yourself:

example {c : ℝ} (h : c ≠ 0) : surjective (λ x, c * x) :=
sorry

index:: field_simp, tactic ; field_simp

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 }

You can use the theorem div_mul_cancel. The next example uses a surjectivity hypothesis by applying it to a suitable value. Note that you can use cases with any expression, not just a hypothesis.

example {f : ℝ → ℝ} (h : surjective f) : ∃ x, (f x)^2 = 4 :=
begin
  cases h 2 with x hx,
  use x,
  rw hx,
  norm_num
end

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

variables {α : Type*} {β : Type*} {γ : Type*}
variables {g : β → γ} {f : α → β}

example (surjg : surjective g) (surjf : surjective f) :
  surjective (λ x, g (f x)) :=
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 :=
begin
  intro h',
  have : a < a,
    from lt_trans h h',
  apply lt_irrefl a this
end

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. Also, the from tactic is syntactic sugar for exact, providing a nice way to justify a have with 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 fn_has_ub defined in the last section, which says that a function has an upper bound.

example (h : ∀ a, ∃ x, f x > a) : ¬ fn_has_ub f :=
begin
  intros fnub,
  cases fnub with a fnuba,
  cases h a with x hx,
  have : f x ≤ a,
    from fnuba x,
  linarith
end

See if you can prove these in a similar way:

example (h : ∀ a, ∃ x, f x < a) : ¬ fn_has_lb f :=
sorry

example : ¬ fn_has_ub (λ 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 :=
sorry

example (h : a ≤ b) (h' : f b < f a) : ¬ monotone f :=
sorry

Remember that it is often convenient to use linarith when a goal follows from linear equations and inequalities that in the context.

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 :=
begin
  intro h,
  let f := λ x : ℝ, (0 : ℝ),
  have monof : monotone f,
  { sorry },
  have h' : f 1 ≤ f 0,
    from le_refl _,
  sorry
end

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 : ℝ → ℝ := λ (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 :=
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):

variables {α : Type*} (P : α → Prop) (Q : Prop)

example (h : ¬ ∃ x, P x) : ∀ x, ¬ P x :=
sorry

example (h : ∀ x, ¬ P x) : ¬ ∃ x, P x :=
sorry

example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x :=
sorry

example (h : ∃ x, ¬ P x) : ¬ ∀ x, P x :=
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, and, in general, you have to declare your intention of using such reasoning by adding the command open_locale classical to your file. With that command, we can use proof by contradiction to prove the third implication as follows.

open_locale classical

example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x :=
begin
  by_contradiction h',
  apply h,
  intro x,
  show P x,
  by_contradiction h'',
  exact h' ⟨x, h''⟩
end

Make sure you understand how this works. The by_contradiction tactic (also abbreviated to by_contra) 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_contradiction, while the reverse direction follows from the ordinary rules for negation.

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

example (h : Q) : ¬ ¬ Q :=
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 : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a :=
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) : fn_has_ub f :=
begin
  push_neg at h,
  exact h
end

example (h : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a :=
begin
  simp only [fn_has_ub, fn_ub] at h,
  push_neg at h,
  exact h
end

In the second example, we use Lean’s simplifier to expand the definitions of fn_has_ub and fn_ub. (We need to use simp rather than rw to expand fn_ub, 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 :=
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 : ¬ fn_has_ub f) : ∀ a, ∃ x, f x > a :=
begin
  contrapose! h,
  exact h
end

example (x : ℝ) (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 :=
begin
  contrapose! h,
  use x / 2,
  split; linarith
end

We have not yet explained the split 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 :=
begin
  exfalso,
  apply lt_irrefl 0 h
end

example (h : 0 < 0) : a > 37 :=
absurd h (lt_irrefl 0)

example (h : 0 < 0) : a > 37 :=
begin
  have h' : ¬ 0 < 0,
    from lt_irrefl 0,
  contradiction
end

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 Bi-implication

You have already seen that the conjunction symbol, ∧, is used to express “and.” The split 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 :=
begin
  split,
  { assumption },
  intro h,
  apply h₁,
  rw h
end

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₀, λ h, h₁ (by rw h)⟩

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

Using a conjunction instead of proving one involves unpacking the proofs of the two parts. You can uses the cases tactic for that, as well as rcases, rintros, or a pattern-matching lambda, 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 :=
begin
  cases h with h₀ h₁,
  contrapose! h₁,
  exact le_antisymm h₀ h₁
end

example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬ y ≤ x :=
begin
  rintros ⟨h₀, h₁⟩ h',
  exact h₁ (le_antisymm h₀ h')
end

example {x y : ℝ} : x ≤ y ∧ x ≠ y → ¬ y ≤ x :=
λ ⟨h₀, h₁⟩ h', h₁ (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 :=
begin
  intro h',
  apply h.right,
  exact le_antisymm h.left h'
end

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬ y ≤ x :=
λ 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, rintros, 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 :=
begin
  rintros ⟨z, xltz, zlty⟩,
  exact lt_trans xltz zlty
end

example (x y : ℝ) : (∃ z : ℝ, x < z ∧ z < y) → x < y :=
λ ⟨z, xltz, zlty⟩, lt_trans xltz zlty

You can also use the use tactic:

example : ∃ x : ℝ, 2 < x ∧ x < 4 :=
begin
  use 5 / 2,
  split; norm_num
end

example : ∃ m n : ℕ,
  4 < m ∧ m < n ∧ n < 10 ∧ nat.prime m ∧ nat.prime n :=
begin
  use [5, 7],
  norm_num
end

example {x y : ℝ} : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x :=
begin
  rintros ⟨h₀, h₁⟩,
  use [h₀, λ h', h₁ (le_antisymm h₀ h')]
end

In the first example, the semicolon after the split 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 split or angle brackets, just as you would if you were proving a conjunction.

example {x y : ℝ} (h : x ≤ y) : ¬ y ≤ x ↔ x ≠ y :=
begin
  split,
  { contrapose!,
    rintro rfl,
    reflexivity },
  contrapose!,
  exact le_antisymm h
end

example {x y : ℝ} (h : x ≤ y) : ¬ y ≤ x ↔ x ≠ y :=
⟨λ h₀ h₁, h₀ (by rw h₁), λ 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 :=
begin
  have h' : x^2 = 0,
  { sorry },
  exact pow_eq_zero h'
end

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 abs x < y by the equivalent expression - y < x ∧ x < y, and in the one after that we use dvd_gcd_iff to replace an expression of the form m ∣ gcd n k by the equivalent expression m ∣ n ∧ m ∣ k.

example (x y : ℝ) : abs (x + 3) < 5 → -8 < x ∧ x < 2 :=
begin
  rw abs_lt,
  intro h,
  split; linarith
end

example : 3 ∣ gcd 6 15 :=
begin
  rw dvd_gcd_iff,
  split; norm_num
end

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 }

example : ¬ monotone (λ x : ℝ, -x) :=
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:

variables {α : Type*} [partial_order α]
variables a b : α

example : a < b ↔ a ≤ b ∧ a ≠ b :=
begin
  rw lt_iff_le_not_le,
  sorry
end

Beyond logical operations, you should not need anything more than le_refl and le_antisymm. Then 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. You do not need anything more than le_refl and le_trans. 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.

variables {α : Type*} [preorder α]
variables a b c : α

example : ¬ a < a :=
begin
  rw lt_iff_le_not_le,
  sorry
end

example : a < b → b < c → a < c :=
begin
  simp only [lt_iff_le_not_le],
  sorry
end

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.

variables {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 a case distinction that is implicit or explicit in the assumptions and the data. The cases tactic allows us to make use of a hypothesis of the form A ∨ B. In contrast to the use of cases with conjunction or an existential quantifier, here the cases 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 cases 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 < abs y → x < y ∨ x < -y :=
begin
  cases 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
end

The absolute value function is defined in such a way that we can immediately prove that x ≥ 0 implies abs x = x (this is the theorem abs_of_nonneg) and x < 0 implies abs 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. 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 my_abs

theorem le_abs_self (x : ℝ) : x ≤ abs x :=
sorry

theorem neg_le_abs_self (x : ℝ) : -x ≤ abs x :=
sorry

theorem abs_add (x y : ℝ) : abs (x + y) ≤ abs x + abs y :=
sorry

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

theorem lt_abs : x < abs y ↔ x < y ∨ x < -y :=
sorry

theorem abs_lt : abs x < y ↔ - y < x ∧ x < y :=
sorry

You can also use rcases and rintros with 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 :=
begin
  rcases lt_trichotomy x 0 with xlt | xeq | xgt,
  { left, exact xlt },
  { contradiction },
  right, exact xgt
end

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 :=
begin
  rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩,
  { rw [mul_assoc],
    apply dvd_mul_right },
  rw [mul_comm, mul_assoc],
  apply dvd_mul_right
end

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 :=
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 :=
sorry

example {x y : ℝ} (h : x^2 = y^2) : x = y ∨ x = -y :=
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:

variables {R : Type*} [comm_ring R] [is_domain R]
variables (x y : R)

example (h : x^2 = 1) : x = 1 ∨ x = -1 :=
sorry

example (h : x^2 = y^2) : x = y ∨ x = -y :=
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 domain instead of an integral_domain.

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 classical.em P : P ∨ ¬ P. The name em is short for “excluded middle.”

example (P : Prop) : ¬ ¬ P → P :=
begin
  intro h,
  cases classical.em P,
  { assumption },
  contradiction
end

You can shorten classical.em to em by opening the classical namespace with the command open classical. Alternatively, you can use the by_cases tactic. The open_locale classical command guarantees that Lean can make implicit use of the law of the excluded middle.

open_locale classical

example (P : Prop) : ¬ ¬ P → P :=
begin
  intro h,
  by_cases h' : P,
  { assumption },
  contradiction
end

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 :=
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 converges_to (s : ℕ → ℝ) (a : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, abs (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 : (λ x y : ℝ, (x + y)^2) = (λ 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 : ℝ) : abs a = abs (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 :=
begin
  convert (mul_lt_mul_right _).2 h,
  { rw [one_mul] },
  exact lt_trans zero_lt_one h
end

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 converges_to_const (a : ℝ) : converges_to (λ x : ℕ, a) a :=
begin
  intros ε εpos,
  use 0,
  intros n nge, dsimp,
  rw [sub_self, abs_zero],
  apply εpos
end

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 λ 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 λ 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 converges_to_add {s t : ℕ → ℝ} {a b : ℝ}
  (cs : converges_to s a) (ct : converges_to t b):
converges_to (λ n, s n + t n) (a + b) :=
begin
  intros ε εpos, dsimp,
  have ε2pos : 0 < ε / 2,
  { linarith },
  cases cs (ε / 2) ε2pos with Ns hs,
  cases ct (ε / 2) ε2pos with Nt ht,
  use max Ns Nt,
  sorry
end

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 abs (s n + t n - (a + b)) is equal to abs ((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 λ 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 converges_to_mul_const {s : ℕ → ℝ} {a : ℝ}
    (c : ℝ) (cs : converges_to s a) :
  converges_to (λ n, c * s n) (c * a) :=
begin
  by_cases h : c = 0,
  { convert converges_to_const 0,
    { ext, rw [h, zero_mul] },
    rw [h, zero_mul] },
  have acpos : 0 < abs c,
    from abs_pos.mpr h,
  sorry
end

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_converges_to {s : ℕ → ℝ} {a : ℝ}
    (cs : converges_to s a) :
  ∃ N b, ∀ n, N ≤ n → abs (s n) < b :=
begin
  cases cs 1 zero_lt_one with N h,
  use [N, abs a + 1],
  sorry
end

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 λ 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.

lemma aux {s t : ℕ → ℝ} {a : ℝ}
    (cs : converges_to s a) (ct : converges_to t 0) :
  converges_to (λ n, s n * t n) 0 :=
begin
  intros ε εpos, dsimp,
  rcases exists_abs_le_of_converges_to cs with ⟨N₀, B, h₀⟩,
  have Bpos : 0 < B,
    from lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _)),
  have pos₀ : ε / B > 0,
    from div_pos εpos Bpos,
  cases ct _ pos₀ with N₁ h₁,
  sorry
end

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

theorem converges_to_mul {s t : ℕ → ℝ} {a b : ℝ}
    (cs : converges_to s a) (ct : converges_to t b):
  converges_to (λ n, s n * t n) (a * b) :=
begin
  have h₁ : converges_to (λ n, s n * (t n - b)) 0,
  { apply aux cs,
    convert converges_to_add ct (converges_to_const (-b)),
    ring },
  convert (converges_to_add h₁ (converges_to_mul_const b cs)),
  { ext, ring },
  ring
end

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 converges_to_unique {s : ℕ → ℝ} {a b : ℝ}
    (sa : converges_to s a) (sb : converges_to s b) :
  a = b :=
begin
  by_contradiction abne,
  have : abs (a - b) > 0,
  { sorry },
  let ε := abs (a - b) / 2,
  have εpos : ε > 0,
  { change abs (a - b) / 2 > 0, linarith },
  cases sa ε εpos with Na hNa,
  cases sb ε εpos with Nb hNb,
  let N := max Na Nb,
  have absa : abs (s N - a) < ε,
  { sorry },
  have absb : abs (s N - b) < ε,
  { sorry },
  have : abs (a - b) < abs (a - b),
  { sorry },
  exact lt_irrefl _ this
end

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 α:

variables {α : Type*} [linear_order α]

def converges_to' (s : α → ℝ) (a : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, abs (s n - a) < ε

In a later chapter, 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.