$$ \newcommand{\setmin}{\mathbin{\backslash}} \newcommand{\symmdiff}{\mathbin{∆}} $$

8  Infinite Sets

8.1. Equinumerous Sets

Chapter 8 of HTPI begins by defining a set \(A\) to be equinumerous with a set \(B\) if there is a function \(f : A \to B\) that is one-to-one and onto. But in Lean, a function must go from a type to a type, not a set to a set. Thus, when we translate the HTPI definition into Lean’s language, we end up with a definition that tells us when one type is equinumerous with another. Throughout this chapter, we will use the letters U, V, … for types and A, B, … for sets, so we state the definition of equinumerous like this in Lean:

def equinum (U V : Type) : Prop :=
  ∃ (f : U → V), one_to_one f ∧ onto f

As in HTPI, we introduce the notation U ∼ V to indicate that U is equinumerous with V (to enter the symbol ∼, type \sim or \~).

notation:50  U:50 " ∼ " V:50 => equinum U V

Section 8.1 of HTPI begins the study of this concept with some examples. The first is a one-to-one, onto function from \(\mathbb{Z}^+\) to \(\mathbb{Z}\), which shows that \(\mathbb{Z}^+ \sim \mathbb{Z}\). We will modify this example slightly to make it a function fnz from Nat to Int:

def fnz (n : Nat) : Int := if 2 ∣ n then ↑(n / 2) else -↑((n + 1) / 2)

Note that, to get a result of type Int, coercion is necessary. We have specified that the coercion should be done after the computation of either n / 2 or (n + 1) / 2, with that computation being done using natural-number arithmetic. Checking a few values of this functions suggests a simple pattern:

#eval [fnz 0, fnz 1, fnz 2, fnz 3, fnz 4, fnz 5, fnz 6]
  --Answer: [0, -1, 1, -2, 2, -3, 3]

Perhaps the easiest way to prove that fnz is one-to-one and onto is to define a function that turns out to be its inverse. This time, in order to get the right type for the value of the function, we use the function Int.toNat to convert a nonnegative integer to a natural number.

def fzn (a : Int) : Nat :=
  if a ≥ 0 then 2 * Int.toNat a else 2 * Int.toNat (-a) - 1

#eval [fzn 0, fzn (-1), fzn 1, fzn (-2), fzn 2, fzn (-3), fzn 3]
  --Answer: [0, 1, 2, 3, 4, 5, 6]

To prove that fzn is the inverse of fnz, we begin by proving lemmas making it easier to compute the values of these functions

lemma fnz_even (k : Nat) : fnz (2 * k) = ↑k := by
  have h1 : 2 ∣ 2 * k := by
    apply Exists.intro k
    rfl
    done
  have h2 : 0 < 2 := by linarith
  show fnz (2 * k) = ↑k from
    calc fnz (2 * k)
      _ = ↑(2 * k / 2) := if_pos h1
      _ = ↑k := by rw [Nat.mul_div_cancel_left k h2]
  done

lemma fnz_odd (k : Nat) : fnz (2 * k + 1) = -↑(k + 1) := sorry

lemma fzn_nat (k : Nat) : fzn ↑k = 2 * k := by rfl

lemma fzn_neg_succ_nat (k : Nat) : fzn (-↑(k + 1)) = 2 * k + 1 := by rfl

Using these lemmas and reasoning by cases, it is straightforward to prove lemmas confirming that the composition of these functions, in either order, yields the identity function. The cases for the first lemma are based on an exercise from Section 6.1.

lemma fzn_fnz : fzn ∘ fnz = id := by
  apply funext        --Goal : ∀ (x : Nat), (fzn ∘ fnz) x = id x
  fix n : Nat
  rewrite [comp_def]  --Goal : fzn (fnz n) = id n
  have h1 : nat_even n ∨ nat_odd n := Exercise_6_1_16a1 n
  by_cases on h1
  · -- Case 1. h1 : nat_even n
    obtain (k : Nat) (h2 : n = 2 * k) from h1
    rewrite [h2, fnz_even, fzn_nat]
    rfl
    done
  · -- Case 2. h1 : nat_odd n
    obtain (k : Nat) (h2 : n = 2 * k + 1) from h1
    rewrite [h2, fnz_odd, fzn_neg_succ_nat]
    rfl
    done
  done

lemma fnz_fzn : fnz ∘ fzn = id  := sorry

By theorems from Chapter 5, it follows that both fnz and fzn are one-to-one and onto.

lemma fzn_one_one : one_to_one fzn := Theorem_5_3_3_1 fzn fnz fnz_fzn

lemma fzn_onto : onto fzn := Theorem_5_3_3_2 fzn fnz fzn_fnz

lemma fnz_one_one : one_to_one fnz := Theorem_5_3_3_1 fnz fzn fzn_fnz

lemma fnz_onto : onto fnz := Theorem_5_3_3_2 fnz fzn fnz_fzn

We conclude that Nat ∼ Int and Int ∼ Nat:

theorem N_equinum_Z : Nat ∼ Int :=
  Exists.intro fnz (And.intro fnz_one_one fnz_onto)

theorem Z_equinum_N : Int ∼ Nat :=
  Exists.intro fzn (And.intro fzn_one_one fzn_onto)

We’ll give one more example: a one-to-one, onto function fnnn from Nat × Nat to Nat, whose definition is modeled on a function from \(\mathbb{Z}^+ \times \mathbb{Z}^+\) to \(\mathbb{Z}^+\) in HTPI. The definition of fnnn will use numbers of the form k * (k + 1) / 2. These numbers are sometimes called triangular numbers, because they count the number of objects in a triangular grid with k rows.

def tri (k : Nat) : Nat := k * (k + 1) / 2

def fnnn (p : Nat × Nat) : Nat := tri (p.1 + p.2) + p.1

lemma fnnn_def (a b : Nat) : fnnn (a, b) = tri (a + b) + a := by rfl

#eval [fnnn (0, 0), fnnn (0, 1), fnnn (1, 0),
  fnnn (0, 2), fnnn (1, 1), fnnn (2, 0)]
  --Answer: [0, 1, 2, 3, 4, 5]

Two simple lemmas about tri, whose proofs we leave as exercises for you, help us prove the important properties of fnnn:

lemma tri_step (k : Nat) : tri (k + 1) = tri k + k + 1 := sorry

lemma tri_incr {j k : Nat} (h1 : j ≤ k) : tri j ≤ tri k := sorry

lemma le_of_fnnn_eq {a1 b1 a2 b2 : Nat}
    (h1 : fnnn (a1, b1) = fnnn (a2, b2)) : a1 + b1 ≤ a2 + b2 := by
  by_contra h2
  have h3 : a2 + b2 + 1 ≤ a1 + b1 := by linarith
  have h4 : fnnn (a2, b2) < fnnn (a1, b1) :=
    calc fnnn (a2, b2)
      _ = tri (a2 + b2) + a2 := by rfl
      _ < tri (a2 + b2) + (a2 + b2) + 1 := by linarith
      _ = tri (a2 + b2 + 1) := (tri_step _).symm
      _ ≤ tri (a1 + b1) := tri_incr h3
      _ ≤ tri (a1 + b1) + a1 := by linarith
      _ = fnnn (a1, b1) := by rfl
  linarith
  done

lemma fnnn_one_one : one_to_one fnnn := by
  fix (a1, b1) : Nat × Nat
  fix (a2, b2) : Nat × Nat
  assume h1 : fnnn (a1, b1) = fnnn (a2, b2)  --Goal : (a1, b1) = (a2, b2)
  have h2 : a1 + b1 ≤ a2 + b2 := le_of_fnnn_eq h1
  have h3 : a2 + b2 ≤ a1 + b1 := le_of_fnnn_eq h1.symm
  have h4 : a1 + b1 = a2 + b2 := by linarith
  rewrite [fnnn_def, fnnn_def, h4] at h1
    --h1 : tri (a2 + b2) + a1 = tri (a2 + b2) + a2
  have h6 : a1 = a2 := Nat.add_left_cancel h1
  rewrite [h6] at h4   --h4 : a2 + b1 = a2 + b2
  have h7 : b1 = b2 := Nat.add_left_cancel h4
  rewrite [h6, h7]
  rfl
  done

lemma fnnn_onto : onto fnnn := by
  define  --Goal : ∀ (y : Nat), ∃ (x : Nat × Nat), fnnn x = y
  by_induc
  · -- Base Case
    apply Exists.intro (0, 0)
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : ∃ (x : Nat × Nat), fnnn x = n
    obtain ((a, b) : Nat × Nat) (h1 : fnnn (a, b) = n) from ih
    by_cases h2 : b = 0
    · -- Case 1. h2 : b = 0
      apply Exists.intro (0, a + 1)
      show fnnn (0, a + 1) = n + 1 from
        calc fnnn (0, a + 1)
          _ = tri (0 + (a + 1)) + 0 := by rfl
          _ = tri (a + 1) := by ring
          _ = tri a + a + 1 := tri_step a
          _ = tri (a + 0) + a + 1 := by ring
          _ = fnnn (a, b) + 1 := by rw [h2, fnnn_def]
          _ = n + 1 := by rw [h1]
      done
    · -- Case 2. h2 : b ≠ 0
      obtain (k : Nat) (h3 : b = k + 1) from
        exists_eq_add_one_of_ne_zero h2
      apply Exists.intro (a + 1, k)
      show fnnn (a + 1, k) = n + 1 from
        calc fnnn (a + 1, k)
          _ = tri (a + 1 + k) + (a + 1) := by rfl
          _ = tri (a + (k + 1)) + a + 1 := by ring
          _ = tri (a + b) + a + 1 := by rw [h3]
          _ = fnnn (a, b) + 1 := by rfl
          _ = n + 1 := by rw [h1]
      done
    done
  done

theorem NxN_equinum_N : (Nat × Nat) ∼ Nat :=
  Exists.intro fnnn (And.intro fnnn_one_one fnnn_onto)

One of the most important theorems about the concept of equinumerosity is Theorem 8.1.3 in HTPI, which says that ∼ is reflexive, symmetric, and transitive. We’ll prove the three parts of this theorem separately. To prove that ∼ is reflexive, we use the identity function. (Recall from Section 5.1 that @id U is the identity function on the type U.)

lemma id_one_one (U : Type) : one_to_one (@id U) := by
  fix x1 : U; fix x2 : U
  assume h : id x1 = id x2
  show x1 = x2 from h
  done

lemma id_onto (U : Type) : onto (@id U) := by
  fix y : U              --Goal : ∃ (x : U), id x = y
  apply Exists.intro y   --Goal : id y = y
  rfl
  done

theorem Theorem_8_1_3_1 (U : Type) : U ∼ U := by
  apply Exists.intro id
  show one_to_one id ∧ onto id from And.intro (id_one_one U) (id_onto U)
  done

For symmetry, we use some theorems from Chapter 5 about inverses of functions:

theorem Theorem_8_1_3_2 {U V : Type}
    (h : U ∼ V) : V ∼ U := by
  obtain (f : U → V) (h1 : one_to_one f ∧ onto f) from h
  obtain (finv : V → U) (h2 : graph finv = inv (graph f)) from
    Theorem_5_3_1 f h1.left h1.right
  apply Exists.intro finv
  have h3 : finv ∘ f = id := Theorem_5_3_2_1 f finv h2
  have h4 : f ∘ finv = id := Theorem_5_3_2_2 f finv h2
  show one_to_one finv ∧ onto finv from
    And.intro (Theorem_5_3_3_1 finv f h4) (Theorem_5_3_3_2 finv f h3)
  done

Finally, for transitivity, we use theorems about composition of functions:

theorem Theorem_8_1_3_3 {U V W : Type}
    (h1 : U ∼ V) (h2 : V ∼ W) : U ∼ W := by
  obtain (f : U → V) (h3 : one_to_one f ∧ onto f) from h1
  obtain (g : V → W) (h4 : one_to_one g ∧ onto g) from h2
  apply Exists.intro (g ∘ f)
  show one_to_one (g ∘ f) ∧ onto (g ∘ f) from
    And.intro (Theorem_5_2_5_1 f g h3.left h4.left)
    (Theorem_5_2_5_2 f g h3.right h4.right)
  done

So far, we have only talked about types being equinumerous, but later in this chapter we are going to want to talk about sets being equinumerous. For example, it would be nice if we could give this proof:

theorem wishful_thinking?
    {U : Type} (A : Set U) : A ∼ A := Theorem_8_1_3_1 A

It seems like Lean shouldn’t accept this theorem; the notation ∼ was defined to apply to types, and in this theorem, A is a set, not a type. But if you enter this theorem into Lean, you will find that Lean accepts it! How is that possible?

We can find out what Lean thinks this theorem means by giving the command #check @wishful_thinking?. Lean’s response is:

@wishful_thinking? : ∀ {U : Type} (A : Set U), ↑A ∼ ↑A

Aha! The uparrows are the key to unlocking the mystery. As we know, uparrows in Lean represent coercions. So Lean must have coerced A into a type, so that it can be used with the ∼ notation. Although A is a set, ↑A is a type.

What is the type ↑A? Intuitively, you can think of the objects of type ↑A as the elements of A. Since A has type Set U, the elements of A are some, but perhaps not all, of the objects of type U; for this reason, ↑A is called a subtype of U.

However, this intuitive description can be misleading. The relationship between ↑A and U is actually similar to the relationship between Nat and Int. Recall that, although we think of the natural numbers as being contained in the integers, in Lean, the types Nat and Int are completely separate. If n has type Nat, then n is not an integer, but there is an integer that corresponds to n, and n can be coerced to that corresponding integer. Similarly, although we might think of ↑A as being contained in U, in fact the two types are completely separate. If a has type ↑A, then a does not have type U, but there is an object of type U that corresponds to a. That corresponding object is called the value of a, and it is denoted a.val. Furthermore, a can be coerced to a.val; using Lean’s notation for coercion, we can write ↑a = a.val.

If a has type ↑A, then not only is a.val an object of type U, but it is an element of A. Indeed, a supplies us with a proof of this fact. This proof is denoted a.property. In other words, we have a.property : a.val ∈ A. Indeed, you might think of any object a : ↑A as a bundle consisting of two pieces of data, a.val and a.property. Not only can we extract these two pieces of data from a by using the .val and .property notation, but we can go in the other direction. That is, if we have x : U and h : x ∈ A, then we can bundle these two pieces of data together to create an object of type ↑A. This object of type ↑A is denoted Subtype.mk x h. Thus, if a = Subtype.mk x h, then a has type ↑A, a.val = x, and a.property = h. We can make the creation of objects of type ↑A slightly simpler by introducing the following function:

def Subtype_elt {U : Type} {A : Set U} {x : U} (h : x ∈ A) : ↑A :=
  Subtype.mk x h

Note that the only nonimplicit argument of Subtype_elt is h. Thus, if we have h : x ∈ A, then Subtype_elt h is an object of type ↑A whose value is x.

There is one more important property of the type ↑A. For each element of A, there is only one corresponding object of type ↑A. That means that if a1 and a2 are two objects of type ↑A and a1.val = a2.val, then a1 = a2. We can think of this as an extensionality principle for subtypes. Recall that the extensionality principle for sets is called Set.ext, and it says that if two sets have the same elements, then they are equal. Similarly, the extensionality principle for subtypes is denoted Subtype.ext, and it says that if two objects of type ↑A have the same value, then they are equal. More precisely, if we have a1 a2 : ↑A, then Subtype.ext proves a.val = a2.val → a1 = a2. And just as we usually start a proof that two sets are equal with the tactic apply Set.ext, it is often useful to start a proof that two objects of type ↑A are equal with the tactic apply Subtype.ext.

Now that we know that the concept of equinumerosity can be applied not only to types but also to sets, we can use this idea to make a number of definitions. For any natural number \(n\), HTPI defines \(I_n\) to be the set \(\{1, 2, \ldots, n\}\), and then it defines a set to be finite if it is equinumerous with \(I_n\), for some \(n\). In Lean, it is a bit more convenient to use sets of the form \(\{0, 1, \ldots, n - 1\}\). With that small change, we can repeat the definitions of finite, denumerable, and countable in HTPI.

def I (n : Nat) : Set Nat := {k : Nat | k < n}

lemma I_def (k n : Nat) : k ∈ I n ↔ k < n := by rfl

def finite (U : Type) : Prop := ∃ (n : Nat), I n ∼ U

def denum (U : Type) : Prop := Nat ∼ U

lemma denum_def (U : Type) : denum U ↔ Nat ∼ U := by rfl

def ctble (U : Type) : Prop := finite U ∨ denum U

Note that in the definition of finite, I n ∼ U means ↑(I n) ∼ U, because I n is a set, not a type. But we will usually leave it to Lean to fill in such coercions when necessary.

Theorem 8.1.5 in HTPI gives two useful ways to characterize countable sets. The proof of the theorem in HTPI uses the fact that every set of natural numbers is countable. HTPI gives an intuitive explanation of why this is true, but of course in Lean an intuitive explanation won’t do. So before proving a version of Theorem 8.1.5, we sketch a proof that every set of natural numbers is countable.

Suppose A has type Set Nat. To prove that A is countable, we will define a function that numbers the elements of A by assigning the number 0 to the smallest element of A, 1 to the next element of A, 2 to the next, and so on. How do we tell which natural number should be assigned to any element m of A? Notice that if m is the smallest element of A, then there are 0 elements of A that are smaller than m; if it is the second smallest element of A, then there is 1 element of A that is smaller than m; and so on. In general, the number assigned to m should be the number of elements of A that are smaller than m. We therefore begin by defining a function num_elts_below A m that counts the number of elements of A that are smaller than any natural number m.

The definition of num_elts_below is recursive. The recursive step relates the number of elements of A below n + 1 to the number of elements below n. There are two possibilities: either n ∈ A and the number of elements below n + 1 is one larger than the number below n, or n ∉ A and the two numbers are the same. (This may remind you of the recursion we used to define num_rp_below in Chapter 7.)

def num_elts_below (A : Set Nat) (m : Nat) : Nat :=
  match m with
    | 0 => 0
    | n + 1 => **if n ∈ A then (num_elts_below A n) + 1::
                else num_elts_below A n

Unfortunately, this definition results in an error message: failed to synthesize Decidable (n ∈ A). Lean is complaining because it doesn’t know how to decide, in general, whether or not n ∈ A. As a result, if we asked it to evaluate num_elts_below A m, for some particular set A and natural number m, it wouldn’t know how to compute it. But this won’t be an issue for us; we want to use num_elts_below to prove theorems, but we’re never going to ask Lean to compute it. For reasons that we won’t explain here, we can get Lean to ignore this issue by adding the line open Classical at the top of our Lean file. This change leads to a new error, but this time the message is more helpful: failed to compile definition, consider marking it as 'noncomputable'. Following Lean’s advice, we finally get a definition that is acceptable to Lean:

open Classical

noncomputable def num_elts_below (A : Set Nat) (m : Nat) : Nat :=
  match m with
    | 0 => 0
    | n + 1 => if n ∈ A then (num_elts_below A n) + 1
                else num_elts_below A n

For example, if A = {1, 3, 4}, then num_elts_below A 0 = num_elts_below A 1 = 0, num_elts_below A 2 = num_elts_below A 3 = 1, num_elts_below A 4 = 2, and num_elt_below A m = 3 for every m ≥ 5. Notice that num_elts_below A is a function from Nat to Nat, but it is neither one-to-one nor onto. To make it useful for proving that A is countable, we’ll need to modify it.

Suppose f : U → V, but f is not one-to-one or onto. How can we modify f to get a function that is one-to-one or onto? We begin with the problem of getting a function that is onto. The range of f is the set of all y : V such that for some x : U, f x = y:

def range {U V : Type} (f : U → V) : Set V := {y : V | ∃ (x : U), f x = y}

(In the exercises, we ask you to show that this is the same as Ran (graph f).) Since every value of f is in range f, we can convert f into a function from U to range f (that is, from U to ↑(range f)), as follows:

lemma elt_range {U V : Type} (f : U → V) (x : U) : f x ∈ range f := by
  define                 --Goal : ∃ (x_1 : U), f x_1 = f x
  apply Exists.intro x
  rfl
  done

def func_to_range {U V : Type} (f : U → V) (x : U) : range f :=
  Subtype_elt (elt_range f x)

According to these definitions, func_to_range f is a function from U to ↑(range f); it is the same as f, except that each value of the function is converted to an object of type ↑(range f). And it is not hard to prove that this function is onto:

lemma ftr_def {U V : Type} (f : U → V) (x : U) :
    (func_to_range f x).val = f x := by rfl

lemma ftr_onto {U V : Type} (f : U → V) : onto (func_to_range f) := by
  fix y : range f              --y has type ↑(range f)
  have h1 : y.val ∈ range f := y.property
  define at h1                 --h1 : ∃ (x : U), f x = y.val
  obtain (x : U) (h2 : f x = y.val) from h1
  apply Exists.intro x         --Goal : func_to_range f x = y
  apply Subtype.ext            --Goal : (func_to_range f x).val = y.val
  rewrite [ftr_def, h2]
  rfl
  done

Is func_to_range f one-to-one? It turns out that if f is one-to-one, then so is func_to_range f, and therefore func_to_range f can be used to prove that U ∼ range f. Here are the proofs:

lemma ftr_one_one_of_one_one {U V : Type} {f : U → V}
    (h : one_to_one f) : one_to_one (func_to_range f) := by
  fix x1 : U; fix x2 : U
  assume h1 : func_to_range f x1 = func_to_range f x2
  have h2 : f x1 = f x2 :=
    calc f x1
      _ = (func_to_range f x1).val := (ftr_def f x1).symm
      _ = (func_to_range f x2).val := by rw [h1]
      _ = f x2 := ftr_def f x2
  show x1 = x2 from h x1 x2 h2
  done

theorem equinum_range {U V : Type} {f : U → V}
    (h : one_to_one f) : U ∼ range f := by
  apply Exists.intro (func_to_range f)
  show one_to_one (func_to_range f) ∧ onto (func_to_range f) from
    And.intro (ftr_one_one_of_one_one h) (ftr_onto f)
  done

We have seen that, given a function f : U → V, we can turn f into an onto function by replacing V with a subtype of V. (This is similar to an idea that is mentioned briefly in HTPI; see Exercise 23 in Section 5.2 of HTPI.) It is perhaps not surprising that we can sometimes turn f into a one-to-one function by replacing U with a subtype of U. If A has type Set U, then the restriction of f to A is a function from A to V. It has the same values as f, but only when applied to elements of A. (This idea is also mention in HTPI; see Exercise 7 in Section 5.2 of HTPI.) We can define the restriction of f to A in Lean as follows:

def func_restrict {U V : Type}
  (f : U → V) (A : Set U) (x : A) : V := f x.val

lemma fr_def {U V : Type} (f : U → V) (A : Set U) (x : A) :
    func_restrict f A x = f x.val := by rfl

Thus, func_restrict f A is a function from A to V (that is, from ↑A to V). Is it one-to-one? The answer is: sometimes. We will say that a function is one-to-one on A if it satisfies the definition of one-to-one when applied to elements of A:

def one_one_on {U V : Type} (f : U → V) (A : Set U) : Prop :=
  ∀ ⦃x1 x2 : U⦄, x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2

Notice that in this definition, we have used the same double braces for the quantified variables x1 and x2 that were used in the definition of “subset.” This means that x1 and x2 are implicit arguments, and therefore if we have h : one_one_on f A, ha1 : a1 ∈ A, ha2 : a2 ∈ A, and heq : f a1 = f a2, then h h1a h2a heq is a proof of a1 = a2. There is no need to specify that a1 and a2 are the values to be assigned to x1 and x2; Lean will figure that out for itself. (To type the double braces ⦃ and ⦄, type \{{ and \}}. There were cases in previous chapters where it would have been appropriate to use such implicit arguments, but we chose not to do so to avoid confusion. But by now you should be comfortable enough with Lean that you won’t be confused by this new complication.)

It is now not hard to show that if f is one-to-one on A, then func_restrict f A is one-to-one:

lemma fr_one_one_of_one_one_on {U V : Type} {f : U → V} {A : Set U}
    (h : one_one_on f A) : one_to_one (func_restrict f A) := by
  fix x1 : A; fix x2 : A                    --x1 and x2 have type ↑A
  assume h1 : func_restrict f A x1 = func_restrict f A x2
  rewrite [fr_def, fr_def] at h1            --h1 : f x1.val = f x2.val
  apply Subtype.ext                         --Goal : x1.val = x2.val
  show x1.val = x2.val from h x1.property x2.property h1
  done

Now we can combine our last two results: if f is one-to-one on A, then func_restrict f A is one-to-one, and therefore A is equinumerous with the range of func_restrict f A. And what is the range of func_restrict f A? It is just the image of A under f:

lemma elt_image {U V : Type} {A : Set U} {x : U}
    (f : U → V) (h : x ∈ A) : f x ∈ image f A := by
  define                   --Goal : ∃ x_1 ∈ A, f x_1 = f x
  apply Exists.intro x     --Goal : x ∈ A ∧ f x = f x
  apply And.intro h
  rfl
  done

lemma fr_range {U V : Type} (f : U → V) (A : Set U) :
    range (func_restrict f A) = image f A := by
  apply Set.ext
  fix y : V
  apply Iff.intro
  · -- (→)
    assume h1 : y ∈ range (func_restrict f A) --Goal : y ∈ image f A
    define at h1
    obtain (a : A) (h2 : func_restrict f A a = y) from h1
    rewrite [←h2, fr_def]                     --Goal : f a.val ∈ image f A
    show f a.val ∈ image f A from elt_image f a.property
    done
  · -- (←)
    assume h1 : y ∈ image f A         --Goal : y ∈ range (func_restrict f A)
    define at h1
    obtain (a : U) (h2 : a ∈ A ∧ f a = y) from h1
    set aA : A := Subtype_elt h2.left
    have h3 : func_restrict f A aA = f a := fr_def f A aA
    rewrite [←h2.right, ←h3]
    show func_restrict f A aA ∈ range (func_restrict f A) from
      elt_range (func_restrict f A) aA
    done
  done

Putting it all together, we have another theorem that helps us prove that sets are equinumerous:

theorem equinum_image {U V : Type} {A : Set U} {f : U → V}
    (h : one_one_on f A) : A ∼ image f A := by
  rewrite [←fr_range f A]          --Goal : A ∼ range (func_restrict f A)
  have h1 : one_to_one (func_restrict f A) :=
    fr_one_one_of_one_one_on h
  show A ∼ range (func_restrict f A) from equinum_range h1
  done

We now return to the problem of showing that if A has type Set Nat, then it is countable. Recall that we have defined a function num_elts_below A : Nat → Nat that counts the number of elements of A below any natural number. Although num_elts_below A is not one-to-one, it turns out that it is one-to-one on A. We use this fact to show that if A has an upper bound then it is finite, and if it doesn’t then it is denumerable. The details of the proof are somewhat long. We’ll skip some of them here, but you can find them in the HTPI Lean package.

lemma neb_one_one_on (A : Set Nat) :
    one_one_on (num_elts_below A) A := sorry

lemma neb_image_bdd {A : Set Nat} {m : Nat} (h : ∀ n ∈ A, n < m) :
    image (num_elts_below A) A = I (num_elts_below A m) := sorry

lemma bdd_subset_nat {A : Set Nat} {m : Nat}
    (h : ∀ n ∈ A, n < m) : I (num_elts_below A m) ∼ A := by
  have h2 : A ∼ image (num_elts_below A) A :=
    equinum_image (neb_one_one_on A)
  rewrite [neb_image_bdd h] at h2        --h2 : A ∼ I (num_elts_below A m)
  show I (num_elts_below A m) ∼ A from Theorem_8_1_3_2 h2
  done

lemma neb_unbdd_onto {A : Set Nat}
    (h : ∀ (m : Nat), ∃ n ∈ A, n ≥ m) :
    onto (func_restrict (num_elts_below A) A) := sorry
  
lemma unbdd_subset_nat {A : Set Nat}
    (h : ∀ (m : Nat), ∃ n ∈ A, n ≥ m) :
    denum A := by
  rewrite [denum_def]
  set f : A → Nat := func_restrict (num_elts_below A) A
  have h1 : one_to_one f :=
    fr_one_one_of_one_one_on (neb_one_one_on A)
  have h2 : onto f := neb_unbdd_onto h
  have h3 : A ∼ Nat := Exists.intro f (And.intro h1 h2)
  show Nat ∼ A from Theorem_8_1_3_2 h3
  done

theorem set_nat_ctble (A : Set Nat) : ctble A := by
  define          --Goal : finite A ∨ denum A
  by_cases h1 : ∃ (m : Nat), ∀ n ∈ A, n < m
  · -- Case 1. h1 : ∃ (m : Nat), ∀ n ∈ A, n < m
    apply Or.inl  --Goal : finite A
    obtain (m : Nat) (h2 : ∀ n ∈ A, n < m) from h1
    define
    apply Exists.intro (num_elts_below A m)
    show I (num_elts_below A m) ∼ A from bdd_subset_nat h2
    done
  · -- Case 2. h1 : ¬∃ (m : Nat), ∀ n ∈ A, n < m
    apply Or.inr  --Goal : denum A
    push_neg at h1
      --This tactic converts h1 to ∀ (m : Nat), ∃ n ∈ A, m ≤ n
    show denum A from unbdd_subset_nat h1
    done
  done

As a consequence of our last theorem, we will get another characterization of countability: a type is countable if and only if it is equinumerous with some set of natural numbers. A finite type is equinumerous with the set I n, for some natural number n. But what set of natural numbers is a denumerable type equinumerous with? The obvious choice is the set of all natural numbers. We might call it the universal set for the type Nat. It will be convenient to have notation for the universal set of any type. It is not hard to show that any type is equinumerous with its universal set. We leave one lemma for the proof as an exercise for you:

def Univ (U : Type) : Set U := {x : U | True}

lemma elt_univ {U : Type} (x : U) : x ∈ Univ U := by
  define   --Goal : True
  trivial
  done

lemma onto_iff_range_eq_univ {U V : Type} (f : U → V) :
    onto f ↔ range f = Univ V := sorry

lemma univ_equinum_type (U : Type) : Univ U ∼ U := by
  set f : U → U := id
  have h1 : one_to_one f := id_one_one U
  have h2 : onto f := id_onto U
  rewrite [onto_iff_range_eq_univ] at h2  --h2 : range f = Univ U
  have h3 : U ∼ range f := equinum_range h1
  rewrite [h2] at h3
  show Univ U ∼ U from Theorem_8_1_3_2 h3
  done

With this preparation, we can prove our next characterization of countability, leaving the poof of a lemma as an exercise for you:

lemma ctble_of_ctble_equinum {U V : Type}
    (h1 : U ∼ V) (h2 : ctble U) : ctble V := sorry

theorem ctble_iff_set_nat_equinum (U : Type) :
    ctble U ↔ ∃ (J : Set Nat), J ∼ U := by
  apply Iff.intro
  · -- (→)
    assume h1 : ctble U
    define at h1  --h1 : finite U ∨ denum U
    by_cases on h1
    · -- Case 1. h1 : finite U
      define at h1  --h1 : ∃ (n : Nat), I n ∼ U
      obtain (n : Nat) (h2 : I n ∼ U) from h1
      show ∃ (J : Set Nat), J ∼ U from Exists.intro (I n) h2
      done
    · -- Case 2. h1 : denum U
      rewrite [denum_def] at h1  --h1 : Nat ∼ U
      have h2 : Univ Nat ∼ Nat := univ_equinum_type Nat
      apply Exists.intro (Univ Nat)
      show Univ Nat ∼ U from Theorem_8_1_3_3 h2 h1
      done
    done
  · -- (←)
    assume h1 : ∃ (J : Set Nat), J ∼ U
    obtain (J : Set Nat) (h2 : J ∼ U) from h1
    have h3 : ctble J := set_nat_ctble J
    show ctble U from ctble_of_ctble_equinum h2 h3
    done
  done

We have seen that if we have f : U → V, then it can be useful to replace either U or V with a subtype. We accomplished this by defining two functions, func_to_range and func_restrict. It is also sometimes useful to go in the other direction. To do this, we will define functions func_to_type and func_extend that are, in a sense, the reverses of func_to_range and func_restrict. If we have f : U → B, where B has type Set V, then func_to_type f is a function from U to V; it is the same as f, but with the values of the function coerced from B to V. If we have f : A → V and v : V, where A has type Set U, then func_extend f v is also a function from U to V; when applied to an element of A, it has the value specified by f, and when applied to anything else it has the value v. Here are the definitions:

def func_to_type {U V : Type} {B : Set V}
  (f : U → B) (x : U) : V := (f x).val

lemma ftt_def {U V : Type} {B : Set V} (f : U → B) (x : U) :
    func_to_type f x = (f x).val := by rfl

noncomputable def func_extend {U V : Type} {A : Set U}
  (f : A → V) (v : V) (u : U) : V :=
  if test : u ∈ A then f (Subtype_elt test) else v

lemma fe_elt {U V : Type} {A : Set U} (f : A → V) (v : V) (a : A) :
    func_extend f v a.val = f a := dif_pos a.property

Notice that in the definition of func_extend, we gave an identifier to the test in the if clause, so that we could refer to that test in the then clause. As a result, the if-then-else expression in the definition is what is called a dependent if-then-else. The proof of the lemma fe_elt uses the theorem dif_pos, which is just like if_pos, but for dependent if-then-else expressions. (Of course, dif_neg is the dependent version of if_neg.)

The sense in which func_to_type and func_extend reverse func_to_range and func_restrict is given by the following examples. We leave the proof of the second as an exercise for you:

example (U V : Type) (f : U → V) :
    func_to_type (func_to_range f) = f := by rfl

example (U V : Type) (A : Set U) (f : A → V) (v : V) :
    func_restrict (func_extend f v) A = f := sorry

How do func_to_type and func_extend interact with the properties one_to_one and onto? The answers are given by the following lemmas; you can find the straightforward proofs in the HTPI Lean package.

lemma ftt_range_of_onto {U V : Type} {B : Set V} {f : U → B}
    (h : onto f) : range (func_to_type f) = B := sorry

lemma ftt_one_one_of_one_one {U V : Type} {B : Set V} {f : U → B}
    (h : one_to_one f) : one_to_one (func_to_type f) := sorry

lemma fe_image {U V : Type} {A : Set U}
    (f : A → V) (v : V) : image (func_extend f v) A = range f := sorry

lemma fe_one_one_on_of_one_one {U V : Type} {A : Set U} {f : A → V}
    (h : one_to_one f) (v : V) : one_one_on (func_extend f v) A := sorry

Just as func_to_type and func_extend can be thought of as reversing func_to_range and func_restrict, the following theorem can be thought of as reversing the theorem equinum_image:

theorem type_to_type_of_equinum {U V : Type} {A : Set U} {B : Set V}
    (h : A ∼ B) (v : V) :
    ∃ (f : U → V), one_one_on f A ∧ image f A = B := by
  obtain (g : A → B) (h1 : one_to_one g ∧ onto g) from h
  set gtt : A → V := func_to_type g
  set f : U → V := func_extend gtt v
  apply Exists.intro f
  apply And.intro
  · -- Proof of one_to_one_on f A
    have h2 : one_to_one gtt := ftt_one_one_of_one_one h1.left
    show one_one_on f A from fe_one_one_on_of_one_one h2 v
    done
  · -- Proof of image f A = B
    have h2 : range gtt = B := ftt_range_of_onto h1.right
    have h3 : image f A = range gtt := fe_image gtt v
    rewrite [h3, h2]
    rfl
    done
  done

We are finally ready to turn to Theorem 8.1.5 in HTPI. The theorem says that for any set \(A\), the following statements are equivalent:

1. \(A\) is countable.
2. Either \(A = \varnothing\) or there is a function \(f : \mathbb{Z}^+ \to A\) that is onto.
3. There is a function \(f : A \to \mathbb{Z}^+\) that is one-to-one.

We will find it convenient to phrase these statements a little differently in Lean. Our plan is to prove that if A has type Set U then the following statements are equivalent:

1. ctble A
2. empty A ∨ ∃ (f : Nat → U), A ⊆ range f
3. ∃ (f : U → Nat), one_one_on f A

As in HTPI, we will do this by proving 1 → 2 → 3 → 1. Here is the proof of 1 → 2.

theorem Theorem_8_1_5_1_to_2 {U : Type} {A : Set U} (h : ctble A) :
    empty A ∨ ∃ (f : Nat → U), A ⊆ range f := by
  or_right with h1                          --h1 : ∃ (x : U), x ∈ A
  obtain (a : U) (h2 : a ∈ A) from h1
  rewrite [ctble_iff_set_nat_equinum] at h  --h : ∃ (J : Set Nat), J ∼ A
  obtain (J : Set Nat) (h3 : J ∼ A) from h
  obtain (f : Nat → U) (h4 : one_one_on f J ∧ image f J = A) from
    type_to_type_of_equinum h3 a
  apply Exists.intro f                      --Goal : A ⊆ range f
  fix y : U
  assume h5 : y ∈ A
  rewrite [←h4.right] at h5
  define at h5
  obtain (n : Nat) (h6 : n ∈ J ∧ f n = y) from h5
  rewrite [←h6.right]
  show f n ∈ range f from elt_range f n
  done

For the proof of 2 → 3, we need to consider two cases. If A is empty, then any function f : U → Nat will do to prove statement 3; we use the constant function that always takes the value 0. The easiest way to prove that this function is one-to-one on A is to use a lemma that says if A is empty, then any statement of the form x ∈ A → P is true.

The more interesting case is when we have a function g : Nat → U with A ⊆ range g. This means that for each x ∈ A, there is at least one natural number n such that g n = x. As in HTPI, we first define a function F : A → Nat that picks out the smallest such n; we could call it the smallest preimage of x. We then use func_extend to get the required function from U to Nat. The easiest way to define F is to first define its graph, which we call smallest_preimage_graph g A.

def constant_func (U : Type) {V : Type} (v : V) (x : U) : V := v

lemma elt_empty_implies {U : Type} {A : Set U} {x : U} {P : Prop}
    (h : empty A) : x ∈ A → P := by
  assume h1 : x ∈ A
  contradict h
  show ∃ (x : U), x ∈ A from Exists.intro x h1
  done

lemma one_one_on_empty {U : Type} {A : Set U}
    (f : U → Nat) (h : empty A) : one_one_on f A := by
  fix x1 : U; fix x2 : U
  show x1 ∈ A → x2 ∈ A → f x1 = f x2 → x1 = x2 from
    elt_empty_implies h
  done

def smallest_preimage_graph {U : Type}
  (g : Nat → U) (A : Set U) : Set (A × Nat) :=
  {(x, n) : A × Nat | g n = x.val ∧ ∀ (m : Nat), g m = x.val → n ≤ m}

lemma spg_is_func_graph {U : Type} {g : Nat → U} {A : Set U}
    (h : A ⊆ range g) : is_func_graph (smallest_preimage_graph g A) := by
  define
  fix x : A
  exists_unique
  · -- Existence
    set W : Set Nat := {n : Nat | g n = x.val}
    have h1 : ∃ (n : Nat), n ∈ W := h x.property
    show ∃ (y : Nat), (x, y) ∈ smallest_preimage_graph g A from
      well_ord_princ W h1
    done
  · -- Uniqueness
    fix n1 : Nat; fix n2 : Nat
    assume h1 : (x, n1) ∈ smallest_preimage_graph g A
    assume h2 : (x, n2) ∈ smallest_preimage_graph g A
    define at h1; define at h2
    have h3 : n1 ≤ n2 := h1.right n2 h2.left
    have h4 : n2 ≤ n1 := h2.right n1 h1.left
    linarith
    done
  done

lemma spg_one_one {U : Type} {g : Nat → U} {A : Set U} {f : A → Nat}
    (h : graph f = smallest_preimage_graph g A) : one_to_one f := by
  fix a1 : A; fix a2 : A
  assume h1 : f a1 = f a2
  set y : Nat := f a2           --h1 : f a1 = y
  have h2 : f a2 = y := by rfl
  rewrite [←graph_def, h] at h1 --h1 : (a1, y) ∈ smallest_preimage_graph g A
  rewrite [←graph_def, h] at h2 --h2 : (a2, y) ∈ smallest_preimage_graph g A
  define at h1                  --h1 : g y = a1.val ∧ ...
  define at h2                  --h2 : g y = a2.val ∧ ...
  apply Subtype.ext             --Goal : a1.val = a2.val
  rewrite [←h1.left, ←h2.left]
  rfl
  done

theorem Theorem_8_1_5_2_to_3 {U : Type} {A : Set U}
    (h : empty A ∨ ∃ (f : Nat → U), A ⊆ range f) :
    ∃ (f : U → Nat), one_one_on f A := by
  by_cases on h
  · -- Case 1. h : empty A
    set f : U → Nat := constant_func U 0
    apply Exists.intro f
    show one_one_on f A from one_one_on_empty f h
    done
  · -- Case 2. h : ∃ (f : Nat → U), A ⊆ range f
    obtain (g : Nat → U) (h1 : A ⊆ range g) from h
    have h2 : is_func_graph (smallest_preimage_graph g A) :=
      spg_is_func_graph h1
    rewrite [←func_from_graph] at h2
    obtain (F : A → Nat)
      (h3 : graph F = smallest_preimage_graph g A) from h2
    have h4 : one_to_one F := spg_one_one h3
    set f : U → Nat := func_extend F 0
    apply Exists.intro f
    show one_one_on f A from fe_one_one_on_of_one_one h4 0
    done
  done

Finally, the proof of 3 → 1 is straightforward, using the theorem equinum_image.

theorem Theorem_8_1_5_3_to_1 {U : Type} {A : Set U}
    (h1 : ∃ (f : U → Nat), one_one_on f A) :
    ctble A := by
  obtain (f : U → Nat) (h2 : one_one_on f A) from h1
  have h3 : A ∼ image f A := equinum_image h2
  rewrite [ctble_iff_set_nat_equinum]
  show ∃ (J : Set Nat), J ∼ A from
    Exists.intro (image f A) (Theorem_8_1_3_2 h3)
  done

We now know that statements 1–3 are equivalent, which means that statements 2 and 3 can be thought of as alternative ways to think about countability:

theorem Theorem_8_1_5_2 {U : Type} (A : Set U) :
    ctble A ↔ empty A ∨ ∃ (f : Nat → U), A ⊆ range f := by
  apply Iff.intro Theorem_8_1_5_1_to_2
  assume h1 : empty A ∨ ∃ (f : Nat → U), A ⊆ range f
  have h2 : ∃ (f : U → Nat), one_one_on f A := Theorem_8_1_5_2_to_3 h1
  show ctble A from Theorem_8_1_5_3_to_1 h2
  done

theorem Theorem_8_1_5_3 {U : Type} (A : Set U) :
    ctble A ↔ ∃ (f : U → Nat), one_one_on f A := sorry

We end this section with a proof of Theorem 8.1.6 in HTPI, which says that the set of rational numbers is denumerable. Our strategy is to define a one-to-one function from Rat (the type of rational numbers) to Nat. We will need to know a little bit about the way rational numbers are represented in Lean. If q has type Rat, then q.num is the numerator of q, which is an integer, and q.den is the denominator, which is a nonzero natural number. The theorem Rat.ext says that if two rational numbers have the same numerator and denominator, then they are equal. And we will also use the theorem Prod.mk.inj, which says that if two ordered pairs are equal, then their first coordinates are equal, as are their second coordinates.

def fqn (q : Rat) : Nat := fnnn (fzn q.num, q.den)

lemma fqn_def (q : Rat) : fqn q = fnnn (fzn q.num, q.den) := by rfl

lemma fqn_one_one : one_to_one fqn := by
  define
  fix q1 : Rat; fix q2 : Rat
  assume h1 : fqn q1 = fqn q2
  rewrite [fqn_def, fqn_def] at h1
    --h1 : fnnn (fzn q1.num, q1.den) = fnnn (fzn q2.num, q2.den)
  have h2 : (fzn q1.num, q1.den) = (fzn q2.num, q2.den) :=
    fnnn_one_one _ _ h1
  have h3 : fzn q1.num = fzn q2.num ∧ q1.den = q2.den :=
    Prod.mk.inj h2
  have h4 : q1.num = q2.num := fzn_one_one _ _ h3.left
  show q1 = q2 from Rat.ext h4 h3.right
  done

lemma range_fqn_unbdd :
    ∀ (m : Nat), ∃ n ∈ range fqn, n ≥ m := by
  fix m : Nat
  set n : Nat := fqn ↑m
  apply Exists.intro n
  apply And.intro
  · -- Proof that n ∈ range fqn
    define
    apply Exists.intro ↑m
    rfl
    done
  · -- Proof that n ≥ m
    show n ≥ m from
      calc n
        _ = tri (2 * m + 1) + 2 * m := by rfl
        _ ≥ m := by linarith
    done
  done

theorem Theorem_8_1_6 : denum Rat := by
  set I : Set Nat := range fqn
  have h1 : Nat ∼ I := unbdd_subset_nat range_fqn_unbdd
  have h2 : Rat ∼ I := equinum_range fqn_one_one
  have h3 : I ∼ Rat := Theorem_8_1_3_2 h2
  show denum Rat from Theorem_8_1_3_3 h1 h3
  done

Exercises

--Hint:  Use Exercise_6_1_16a2 from the exercises of Section 6.1.
lemma fnz_odd (k : Nat) : fnz (2 * k + 1) = -↑(k + 1) := sorry

lemma fnz_fzn : fnz ∘ fzn = id  := sorry

lemma tri_step (k : Nat) : tri (k + 1) = tri k + k + 1 := sorry

lemma tri_incr {j k : Nat} (h1 : j ≤ k) : tri j ≤ tri k := sorry

example {U V : Type} (f : U → V) : range f = Ran (graph f) := sorry

lemma onto_iff_range_eq_univ {U V : Type} (f : U → V) :
    onto f ↔ range f = Univ V := sorry

7. Notice that ctble_of_ctble_equinum was used in the proof of ctble_iff_set_nat_equinum. Therefore, to avoid circularity, you must not use ctble_iff_set_nat_equinum in your solution to this exercise.

lemma ctble_of_ctble_equinum {U V : Type}
    (h1 : U ∼ V) (h2 : ctble U) : ctble V := sorry

theorem Exercise_8_1_1_b : denum {n : Int | even n} := sorry

theorem equinum_iff_inverse_pair (U V : Type) :
    U ∼ V ↔ ∃ (f : U → V) (g : V → U), f ∘ g = id ∧ g ∘ f = id := sorry

10. Notice that if f is a function from U to V, then for every X of type Set U, image f X has type Set V. Therefore image f is a function from Set U to Set V.

lemma image_comp_id {U V : Type} {f : U → V} {g : V → U}
    (h : g ∘ f = id) : (image g) ∘ (image f) = id := sorry

theorem Exercise_8_1_5_1 {U V : Type}
    (h : U ∼ V) : Set U ∼ Set V := sorry

If A has type Set U and X has type Set A (that is, Set ↑A), then every element of X has type ↑A, which means that its value is an element of A. Thus, if we take the values of all the elements of X, we will get a set of type Set U that is a subset of A. We will call this the value image of X. We can define a function that computes the value image of any X : Set A:

def val_image {U : Type} (A : Set U) (X : Set A) : Set U :=
  {y : U | ∃ x ∈ X, x.val = y}

The next three exercises ask you to prove properties of this function.

lemma subset_of_val_image_eq {U : Type} {A : Set U} {X1 X2 : Set A}
    (h : val_image A X1 = val_image A X2) : X1 ⊆ X2 := sorry

lemma val_image_one_one {U : Type} (A : Set U) :
    one_to_one (val_image A) := sorry

lemma range_val_image {U : Type} (A : Set U) :
    range (val_image A) = 𝒫 A := sorry

lemma Set_equinum_powerset {U : Type} (A : Set U) :
    Set A ∼ 𝒫 A := sorry

--Hint:  Use Exercise_8_1_5_1 and Set_equinum_powerset.
theorem Exercise_8_1_5_2 {U V : Type} {A : Set U} {B : Set V}
    (h : A ∼ B) : 𝒫 A ∼ 𝒫 B := sorry

example (U V : Type) (A : Set U) (f : A → V) (v : V) :
    func_restrict (func_extend f v) A = f := sorry

18. We proved the implications in Theorem 8.1.5 for sets, but we could prove similar theorems for types. Here is a version of Theorem_8_1_5_3 for types.

theorem Theorem_8_1_5_3_type {U : Type} :
    ctble U ↔ ∃ (f : U → Nat), one_to_one f := sorry

theorem ctble_set_of_ctble_type {U : Type}
    (h : ctble U) (A : Set U) : ctble A := sorry

theorem Exercise_8_1_17 {U : Type} {A B : Set U}
    (h1 : B ⊆ A) (h2 : ctble A) : ctble B := sorry

8.1½. Debts Paid

It is time to fulfill promises we made in two earlier chapters.

In Section 6.2, we promised to define a proposition numElts A n to express the idea that the set A has n elements. It should now be clear how to define this proposition:

def numElts {U : Type} (A : Set U) (n : Nat) : Prop := I n ∼ A

lemma numElts_def {U : Type} (A : Set U) (n : Nat) :
    numElts A n ↔ I n ∼ A := by rfl

It is sometimes convenient to phrase the definition of finite in terms of numElts, so we state that version of the definition as a lemma.

lemma finite_def {U : Type} (A : Set U) :
    finite A ↔ ∃ (n : Nat), numElts A n := by rfl

We also owe you the proofs of several theorems about numElts. We’ll skip the details of some of these proofs, but for those that are not left as exercises, you can find all the details in the HTPI Lean package. We begin with the fact that a set has zero elements if and only if it is empty. If A has type Set U and A is empty, then any function from U to Nat can be used to prove A ∼ I 0. In the proof below, we use a constant function.

lemma not_empty_iff_exists_elt {U : Type} {A : Set U} :
    ¬empty A ↔ ∃ (x : U), x ∈ A := by
  define : empty A
  double_neg
  rfl
  done

lemma image_empty {U : Type} {A : Set U}
    (f : U → Nat) (h : empty A) : image f A = I 0 := sorry

theorem zero_elts_iff_empty {U : Type} (A : Set U) :
    numElts A 0 ↔ empty A := by
  apply Iff.intro
  · -- (→)
    assume h1 : numElts A 0
    define at h1
    obtain (f : I 0 → A) (h2 : one_to_one f ∧ onto f) from h1
    by_contra h3
    rewrite [not_empty_iff_exists_elt] at h3
    obtain (x : U) (h4 : x ∈ A) from h3
    set xA : A := Subtype_elt h4
    obtain (n : I 0) (h5 : f n = xA) from h2.right xA
    have h6 : n.val < 0 := n.property
    linarith
    done
  · -- (←)
    assume h1 : empty A
    rewrite [numElts_def]
    set f : U → Nat := constant_func U 0
    have h2 : one_one_on f A := one_one_on_empty f h1
    have h3 : image f A = I 0 := image_empty f h1
    have h4 : A ∼ image f A := equinum_image h2
    rewrite [h3] at h4
    show I 0 ∼ A from Theorem_8_1_3_2 h4
    done
  done

Next, we prove that if a set has a positive number of elements then it is not empty. The proof is straightforward.

theorem nonempty_of_pos_numElts {U : Type} {A : Set U} {n : Nat}
    (h1 : numElts A n) (h2 : n > 0) : ∃ (x : U), x ∈ A := by
  define at h1
  obtain (f : I n → A) (h3 : one_to_one f ∧ onto f) from h1
  have h4 : 0 ∈ I n := h2
  set x : A := f (Subtype_elt h4)
  show ∃ (x : U), x ∈ A from Exists.intro x.val x.property
  done

Our next theorem is remove_one_numElts, which says that if a set has n + 1 elements, and we remove one element, then the resulting set has n elements. We begin by proving that for any k < n + 1, if we remove k from I (n + 1) then the resulting set is equinumerous with I n. To do this, we define a function that matches up I n with I (n + 1) \ {k}.

def incr_from (k n : Nat) : Nat := if n < k then n else n + 1

The function incr_from k increments natural numbers from k on, while leaving numbers less than k fixed. Our strategy now is to prove that incr_from k is one-to-one on I n, and the image of I n under incr_from k is I (n + 1) \ {k}. The proof is a bit long, so we skip some of the details. Notice that Lean gets confused when coercing I (n + 1) \ {k} to a subtype unless we specify that we want ↑(I (n + 1) \ {k}) rather than ↑(I (n + 1)) \ ↑{k}.

lemma incr_from_one_one (k : Nat) :
    one_to_one (incr_from k) := sorry

lemma incr_from_image {k n : Nat} (h : k < n + 1) :
    image (incr_from k) (I n) = I (n + 1) \ {k} := sorry

lemma one_one_on_of_one_one {U V : Type} {f : U → V}
    (h : one_to_one f) (A : Set U) : one_one_on f A := by
  define
  fix x1 : U; fix x2 : U
  assume h1 : x1 ∈ A
  assume h2 : x2 ∈ A
  show f x1 = f x2 → x1 = x2 from h x1 x2
  done

lemma I_equinum_I_remove_one {k n : Nat}
    (h : k < n + 1) : I n ∼ ↑(I (n + 1) \ {k}) := by
  rewrite [←incr_from_image h]
  show I n ∼ image (incr_from k) (I n) from
    equinum_image (one_one_on_of_one_one (incr_from_one_one k) (I n))
  done

Using one more lemma, whose proof we leave as an exercise for you, we can prove remove_one_numElts.

lemma remove_one_equinum
    {U V : Type} {A : Set U} {B : Set V} {a : U} {b : V} {f : U → V}
    (h1 : one_one_on f A) (h2 : image f A = B)
    (h3 : a ∈ A) (h4 : f a = b) : ↑(A \ {a}) ∼ ↑(B \ {b}) := sorry

theorem remove_one_numElts {U : Type} {A : Set U} {n : Nat} {a : U}
    (h1 : numElts A (n + 1)) (h2 : a ∈ A) : numElts (A \ {a}) n := by
  rewrite [numElts_def] at h1; rewrite [numElts_def]
    --h1 : I (n + 1) ∼ A;  Goal : I n ∼ ↑(A \ {a})
  obtain (f : Nat → U) (h3 : one_one_on f (I (n + 1)) ∧
    image f (I (n + 1)) = A) from type_to_type_of_equinum h1 a
  rewrite [←h3.right] at h2
  obtain (k : Nat) (h4 : k ∈ I (n + 1) ∧ f k = a) from h2
  have h5 : ↑(I (n + 1) \ {k}) ∼ ↑(A \ {a}) :=
    remove_one_equinum h3.left h3.right h4.left h4.right
  have h6 : k < n + 1 := h4.left
  have h7 : I n ∼ ↑(I (n + 1) \ {k}) := I_equinum_I_remove_one h6
  show I n ∼ ↑(A \ {a}) from Theorem_8_1_3_3 h7 h5
  done

Finally, we prove that a set has one element if and only if it is a singleton set, leaving the proof of one lemma as an exercise for you.

lemma singleton_of_diff_empty {U : Type} {A : Set U} {a : U}
    (h1 : a ∈ A) (h2 : empty (A \ {a})) : A = {a} := sorry

lemma one_one_on_I_1 {U : Type} (f : Nat → U) : one_one_on f (I 1) := by
  fix x1 : Nat; fix x2 : Nat
  assume h1 : x1 ∈ I 1
  assume h2 : x2 ∈ I 1
  assume h3 : f x1 = f x2
  define at h1; define at h2   --h1 : x1 < 1; h2 : x2 < 1
  linarith
  done

lemma image_I_1 {U : Type} (f : Nat → U) : image f (I 1) = {f 0} := by
  apply Set.ext
  fix y
  apply Iff.intro
  · -- (→)
    assume h1 : y ∈ image f (I 1)
    define at h1; define
    obtain (x : Nat) (h2 : x ∈ I 1 ∧ f x = y) from h1
    have h3 : x < 1 := h2.left
    have h4 : x = 0 := by linarith
    rewrite [←h2.right, h4]
    rfl
    done
  · -- (←)
    assume h1 : y ∈ {f 0}
    define at h1; define
    apply Exists.intro 0
    apply And.intro _ h1.symm
    define
    linarith
    done
  done

lemma singleton_one_elt {U : Type} (u : U) : numElts {u} 1 := by
  rewrite [numElts_def]  --Goal : I 1 ∼ {u}
  set f : Nat → U := constant_func Nat u
  have h1 : one_one_on f (I 1) := one_one_on_I_1 f
  have h2 : image f (I 1) = {f 0} := image_I_1 f
  have h3 : f 0 = u := by rfl
  rewrite [←h3, ←h2]
  show I 1 ∼ image f (I 1) from equinum_image h1
  done

theorem one_elt_iff_singleton {U : Type} (A : Set U) :
    numElts A 1 ↔ ∃ (x : U), A = {x} := by
  apply Iff.intro
  · -- (→)
    assume h1 : numElts A 1  --Goal : ∃ (x : U), A = {x}
    have h2 : 1 > 0 := by linarith
    obtain (x : U) (h3 : x ∈ A) from nonempty_of_pos_numElts h1 h2
    have h4 : numElts (A \ {x}) 0 := remove_one_numElts h1 h3
    rewrite [zero_elts_iff_empty] at h4
    show ∃ (x : U), A = {x} from
      Exists.intro x (singleton_of_diff_empty h3 h4)
    done
  · -- (←)
    assume h1 : ∃ (x : U), A = {x}
    obtain (x : U) (h2 : A = {x}) from h1
    rewrite [h2]
    show numElts {x} 1 from singleton_one_elt x
    done
  done

We have now proven all of the theorems about numElts whose proofs were promised in Section 6.2. However, there is still one important issue that we have not addressed. Could there be a set A such that, say, numElts A 5 and numElts A 6 are both true? Surely the answer is no—a set can’t have five elements and also have six elements! But it requires proof. We ask you to prove the following theorem in the exercises.

theorem Exercise_8_1_6b {U : Type} {A : Set U} {m n : Nat}
    (h1 : numElts A m) (h2 : numElts A n) : m = n := sorry

Next, we turn to our promise, at the end of Section 7.4, to prove Theorem 7.4.4 of HTPI, which says that the totient function \(\varphi\) is multiplicative.

To define the totient function in Lean, in Chapter 7 we defined phi m to be num_rp_below m m, where num_rp_below m k is the number of natural numbers less than k that are relatively prime to m. But in this chapter we have developed new methods for counting things. Our first task is to show that these new methods agree with the method used in Chapter 7.

We have already remarked that the definition of num_elts_below in this chapter bears some resemblance to the definition of num_rp_below in Chapter 7. It should not be surprising, therefore, that these two counting methods give results that agree.

def set_rp_below (m : Nat) : Set Nat := {n : Nat | rel_prime m n ∧ n < m}

lemma set_rp_below_def (a m : Nat) :
    a ∈ set_rp_below m ↔ rel_prime m a ∧ a < m := by rfl

lemma neb_nrpb (m : Nat) : ∀ ⦃k : Nat⦄, k ≤ m →
    num_elts_below (set_rp_below m) k = num_rp_below m k := sorry

lemma neb_phi (m : Nat) :
    num_elts_below (set_rp_below m) m = phi m := by
  rewrite [phi_def]
  have h1 : m ≤ m := by linarith
  show num_elts_below (set_rp_below m) m = num_rp_below m m from
    neb_nrpb m h1
  done

lemma phi_is_numElts (m : Nat) :
    numElts (set_rp_below m) (phi m) := by
  rewrite [numElts_def, ←neb_phi m]
    --Goal : I (num_elts_below (set_rp_below m) m) ∼ set_rp_below m
  have h1 : ∀ n ∈ set_rp_below m, n < m := by
    fix n : Nat
    assume h2 : n ∈ set_rp_below m
    define at h2
    show n < m from h2.right
    done
  show I (num_elts_below (set_rp_below m) m) ∼ set_rp_below m from
    bdd_subset_nat h1
  done

According to the last lemma, we can now think of phi m as the number of elements of the set set_rp_below m.

We will need one more number-theoretic fact: Lemma 7.4.7 from HTPI. We follow the strategy of the proof in HTPI, separating out one calculation as an auxiliary lemma before giving the main proof.

lemma Lemma_7_4_7_aux {m n : Nat} {s t : Int}
    (h : s * m + t * n = 1) (a b : Nat) :
    t * n * a + s * m * b ≡ a (MOD m) := by
  define
  apply Exists.intro (s * (b - a))
  show t * n * a + s * m * b - a = m * (s * (b - a)) from
    calc t * n * a + s * m * b - a
      _ = (t * n - 1) * a + s * m * b := by ring
      _ = (t * n - (s * m + t * n)) * a + s * m * b := by rw [h]
      _ = m * (s * (b - a)) := by ring
  done

lemma Lemma_7_4_7 {m n : Nat} [NeZero m] [NeZero n]
    (h1 : rel_prime m n) (a b : Nat) :
    ∃ (r : Nat), r < m * n ∧ r ≡ a (MOD m) ∧ r ≡ b (MOD n) := by
  set s : Int := gcd_c1 m n
  set t : Int := gcd_c2 m n
  have h4 : s * m + t * n = gcd m n := gcd_lin_comb n m
  define at h1                      --h1 : gcd m n = 1
  rewrite [h1, Nat.cast_one] at h4  --h4 : s * m + t * n = 1
  set x : Int := t * n * a + s * m * b
  have h5 : x ≡ a (MOD m) := Lemma_7_4_7_aux h4 a b
  rewrite [add_comm] at h4          --h4 : t * n + s * m = 1
  have h6 : s * m * b + t * n * a ≡ b (MOD n) :=
    Lemma_7_4_7_aux h4 b a
  have h7 : s * m * b + t * n * a = x := by ring
  rewrite [h7] at h6                --h6 : x ≡ b (MOD n)
  have h8 : m * n ≠ 0 := mul_ne_zero (NeZero.ne m) (NeZero.ne n)
  rewrite [←neZero_iff] at h8       --h8 : NeZero (m * n)
  have h9 : 0 ≤ x % ↑(m * n) ∧ x % ↑(m * n) < ↑(m * n) ∧
    x ≡ x % ↑(m * n) (MOD m * n) := mod_cmpl_res (m * n) x
  have h10 : x % ↑(m * n) < ↑(m * n) ∧
    x ≡ x % ↑(m * n) (MOD m * n) := h9.right
  set r : Nat := Int.toNat (x % ↑(m * n))
  have h11 : x % ↑(m * n) = ↑r := (Int.toNat_of_nonneg h9.left).symm
  rewrite [h11, Nat.cast_lt] at h10 --h10 : r < m * n ∧ x ≡ r (MOD m * n)
  apply Exists.intro r
  apply And.intro h10.left
  have h12 : r ≡ x (MOD (m * n)) := congr_symm h10.right
  rewrite [Lemma_7_4_5 _ _ h1] at h12 --h12 : r ≡ x (MOD m) ∧ r ≡ x (MOD n)
  apply And.intro
  · -- Proof that r ≡ a (MOD m)
    show r ≡ a (MOD m) from congr_trans h12.left h5
    done
  · -- Proof that r ≡ b (MOD n)
    show r ≡ b (MOD n) from congr_trans h12.right h6
    done
  done

The next fact we need is part 1 of Theorem 8.1.2 in HTPI, which says that if \(A\), \(B\), \(C\), and \(D\) are sets such that \(A \sim B\) and \(C \sim D\), then \(A \times C \sim B \times D\). It is straightforward to translate the HTPI proof into a Lean proof about Cartesian products of equinumerous types.

def func_prod {U V W X : Type} (f : U → V) (g : W → X)
  (p : U × W) : V × X := (f p.1, g p.2)

lemma func_prod_def {U V W X : Type}
    (f : U → V) (g : W → X) (u : U) (w : W) :
    func_prod f g (u, w) = (f u, g w) := by rfl

theorem Theorem_8_1_2_1_type {U V W X : Type}
    (h1 : U ∼ V) (h2 : W ∼ X) : (U × W) ∼ (V × X) := by
  obtain (f : U → V) (h3 : one_to_one f ∧ onto f) from h1
  obtain (g : W → X) (h4 : one_to_one g ∧ onto g) from h2
  apply Exists.intro (func_prod f g)
  apply And.intro
  · -- Proof of one_to_one (func_prod f g)
    fix (u1, w1) : U × W; fix (u2, w2) : U × W
    assume h5 : func_prod f g (u1, w1) = func_prod f g (u2, w2)
    rewrite [func_prod_def, func_prod_def] at h5
    have h6 : f u1 = f u2 ∧ g w1 = g w2 := Prod.mk.inj h5
    have h7 : u1 = u2 := h3.left u1 u2 h6.left
    have h8 : w1 = w2 := h4.left w1 w2 h6.right
    rewrite [h7, h8]
    rfl
    done
  · -- Proof of onto (func_prod f g)
    fix (v, x) : V × X
    obtain (u : U) (h5 : f u = v) from h3.right v
    obtain (w : W) (h6 : g w = x) from h4.right x
    apply Exists.intro (u, w)
    rewrite [func_prod_def, h5, h6]
    rfl
  done

Using coercions to subtypes, we can also apply this theorem to sets. If A, B, C, and D are sets and we have A ∼ B and C ∼ D, then Theorem_8_1_2_1_type implies that ↑A × ↑C ∼ ↑B × ↑D. Unfortunately, Cartesian products of subtypes are somewhat inconvenient to work with. It will turn out to be easier to work with subtypes of Cartesian products. To make this possible, we define a Cartesian product operation on sets:

def set_prod {U V : Type} (A : Set U) (B : Set V) : Set (U × V) :=
  {(a, b) : U × V | a ∈ A ∧ b ∈ B}

notation:75 A:75 " ×ₛ " B:75 => set_prod A B

lemma set_prod_def {U V : Type} (A : Set U) (B : Set V) (a : U) (b : V) :
    (a, b) ∈ A ×ₛ B ↔ a ∈ A ∧ b ∈ B := by rfl

To type the subscript s after ×, type \_s. Thus, to type ×ₛ, you can type \times\_s or \x\_s. Notice that in the notation command that introduces the symbol ×ₛ, we have used the number 75 in positions where we used 50 when defining the notation ∼. Without going into detail about exactly what the three occurrences of 50 and 75 mean, we will just say that this tells Lean that ×ₛ is to be given higher precedence than ∼, and as a result an expression like A ∼ B ×ₛ C will be interpreted as A ∼ (B ×ₛ C) rather than (A ∼ B) ×ₛ C.

According to this definition, if A has type Set U and B has type Set V, then A ×ₛ B has type Set (U × V), and therefore ↑(A ×ₛ B) is a subtype of U × V. There is an obvious correspondence between ↑(A ×ₛ B) and ↑A × ↑B that can be used to prove that they are equinumerous:

lemma elt_set_prod {U V : Type} {A : Set U} {B : Set V} (p : ↑A × ↑B) :
    (p.1.val, p.2.val) ∈ A ×ₛ B := And.intro p.1.property p.2.property

def prod_type_to_prod_set {U V : Type}
  (A : Set U) (B : Set V) (p : ↑A × ↑B) : ↑(A ×ₛ B) :=
  Subtype_elt (elt_set_prod p)

def prod_set_to_prod_type {U V : Type}
  (A : Set U) (B : Set V) (p : ↑(A ×ₛ B)) : ↑A × ↑B :=
  (Subtype_elt p.property.left, Subtype_elt p.property.right)

lemma set_prod_equinum_type_prod {U V : Type} (A : Set U) (B : Set V) :
    ↑(A ×ₛ B) ∼ (↑A × ↑B) := by
  set F : ↑(A ×ₛ B) → ↑A × ↑B := prod_set_to_prod_type A B
  set G : ↑A × ↑B → ↑(A ×ₛ B) := prod_type_to_prod_set A B
  have h1 : F ∘ G = id := by rfl
  have h2 : G ∘ F = id := by rfl
  have h3 : one_to_one F := Theorem_5_3_3_1 F G h2
  have h4 : onto F := Theorem_5_3_3_2 F G h1
  show ↑(A ×ₛ B) ∼ (↑A × ↑B) from Exists.intro F (And.intro h3 h4)
  done

Using this lemma we can now prove a more convenient set version of the first part of Theorem 8.1.2.

theorem Theorem_8_1_2_1_set
    {U V W X : Type} {A : Set U} {B : Set V} {C : Set W} {D : Set X}
    (h1 : A ∼ B) (h2 : C ∼ D) : A ×ₛ C ∼ B ×ₛ D := by
  have h3 : ↑(A ×ₛ C) ∼ (↑A × ↑C) := set_prod_equinum_type_prod A C
  have h4 : (↑A × ↑C) ∼ (↑B × ↑D) := Theorem_8_1_2_1_type h1 h2
  have h5 : ↑(B ×ₛ D) ∼ (↑B × ↑D) := set_prod_equinum_type_prod B D
  have h6 : (↑B × ↑D) ∼ ↑(B ×ₛ D) := Theorem_8_1_3_2 h5
  have h7 : ↑(A ×ₛ C) ∼ (↑B × ↑D) := Theorem_8_1_3_3 h3 h4
  show ↑(A ×ₛ C) ∼ ↑(B ×ₛ D) from Theorem_8_1_3_3 h7 h6
  done

As explained in Section 7.4 of HTPI, a key fact used in the proof of Theorem 7.4.4 is that if \(A\) is a set with \(m\) elements and \(B\) is a set with \(n\) elements, then \(A \times B\) has \(mn\) elements. Section 7.4 of HTPI gives an intuitive explanation of this fact, but we’ll need to prove it in Lean. In other words, we need to prove the following theorem:

theorem numElts_prod {U V : Type} {A : Set U} {B : Set V} {m n : Nat}
    (h1 : numElts A m) (h2 : numElts B n) : numElts (A ×ₛ B) (m * n)

Here’s our plan for this proof: The hypotheses numElts A m and numElts B n mean I m ∼ A and I n ∼ B. Applying Theorem_8_1_2_1_set to these hypotheses, we can infer I m ×ₛ I n ∼ A ×ₛ B. If we can prove that I (m * n) ∼ I m ×ₛ I n, then we’ll be able to conclude I (m * n) ∼ A ×ₛ B, or in other words numElts (A ×ₛ B) (m * n), as required. Thus, the key to the proof is to show that I (m * n) ∼ I m ×ₛ I n.

To prove this, we’ll define a function from Nat to Nat × Nat that maps I (m * n) to I m ×ₛ I n. The function we will use maps a natural number a to the quotient and remainder when a is divided by n.

def qr (n a : Nat) : Nat × Nat := (a / n, a % n)

lemma qr_def (n a : Nat) : qr n a = (a / n, a % n) := by rfl

lemma qr_one_one (n : Nat) : one_to_one (qr n) := by
  define
  fix a1 : Nat; fix a2 : Nat
  assume h1 : qr n a1 = qr n a2       --Goal : a1 = a2
  rewrite [qr_def, qr_def] at h1
  have h2 : a1 / n = a2 / n ∧ a1 % n = a2 % n := Prod.mk.inj h1
  show a1 = a2 from
    calc a1
      _ = n * (a1 / n) + a1 % n := (Nat.div_add_mod a1 n).symm
      _ = n * (a2 / n) + a2 % n := by rw [h2.left, h2.right]
      _ = a2 := Nat.div_add_mod a2 n
  done

lemma qr_image (m n : Nat) :
    image (qr n) (I (m * n)) = (I m) ×ₛ (I n) := sorry

lemma I_prod (m n : Nat) : I (m * n) ∼ I m ×ₛ I n := by
  rewrite [←qr_image m n]
  show I (m * n) ∼ image (qr n) (I (m * n)) from
    equinum_image (one_one_on_of_one_one (qr_one_one n) (I (m * n)))
  done

theorem numElts_prod {U V : Type} {A : Set U} {B : Set V} {m n : Nat}
    (h1 : numElts A m) (h2 : numElts B n) : numElts (A ×ₛ B) (m * n) := by
  rewrite [numElts_def] at h1     --h1 : I m ∼ A
  rewrite [numElts_def] at h2     --h2 : I n ∼ B
  rewrite [numElts_def]           --Goal : I (m * n) ∼ A ×ₛ B
  have h3 : I m ×ₛ I n ∼ A ×ₛ B := Theorem_8_1_2_1_set h1 h2
  have h4 : I (m * n) ∼ I m ×ₛ I n := I_prod m n
  show I (m * n) ∼ A ×ₛ B from Theorem_8_1_3_3 h4 h3
  done

Our strategy for proving Theorem 7.4.4 will be to show that if m and n are relatively prime, then set_rp_below (m * n) ∼ set_rp_below m ×ₛ set_rp_below n. Once again, we use a function from Nat to Nat × Nat to show that these sets are equinumerous. This time, the function will map a to (a % m, a % n).

def mod_mod (m n a : Nat) : Nat × Nat := (a % m, a % n)

lemma mod_mod_def (m n a : Nat) : mod_mod m n a = (a % m, a % n) := by rfl

Our proof will make use of several theorems from the exercises of Sections 7.3 and 7.4:

theorem congr_rel_prime {m a b : Nat} (h1 : a ≡ b (MOD m)) :
    rel_prime m a ↔ rel_prime m b := sorry

theorem rel_prime_mod (m a : Nat) :
    rel_prime m (a % m) ↔ rel_prime m a := sorry

theorem congr_iff_mod_eq_Nat (m a b : Nat) [NeZero m] :
    ↑a ≡ ↑b (MOD m) ↔ a % m = b % m := sorry

lemma Lemma_7_4_6 {a b c : Nat} :
    rel_prime (a * b) c ↔ rel_prime a c ∧ rel_prime b c := sorry

Combining these with other theorems from Chapter 7, we can now use mod_mod m n to show that set_rp_below (m * n) ∼ set_rp_below m ×ₛ set_rp_below n.

lemma left_NeZero_of_mul {m n : Nat} (h : m * n ≠ 0) : NeZero m :=
  neZero_iff.rtl (left_ne_zero_of_mul h)

lemma right_NeZero_of_mul {m n : Nat} (h : m * n ≠ 0) : NeZero n :=
  neZero_iff.rtl (right_ne_zero_of_mul h)

lemma mod_mod_one_one_on {m n : Nat} (h1 : rel_prime m n) :
    one_one_on (mod_mod m n) (set_rp_below (m * n)) := by
  define
  fix a1 : Nat; fix a2 : Nat
  assume h2 : a1 ∈ set_rp_below (m * n)
  assume h3 : a2 ∈ set_rp_below (m * n)
  assume h4 : mod_mod m n a1 = mod_mod m n a2   --Goal : a1 = a2
  define at h2; define at h3
  rewrite [mod_mod_def, mod_mod_def] at h4
  have h5 : a1 % m = a2 % m ∧ a1 % n = a2 % n := Prod.mk.inj h4
  have h6 : m * n ≠ 0 := by linarith
  have h7 : NeZero m := left_NeZero_of_mul h6
  have h8 : NeZero n := right_NeZero_of_mul h6
  rewrite [←congr_iff_mod_eq_Nat, ←congr_iff_mod_eq_Nat] at h5
      --h5 : ↑a1 ≡ ↑a2 (MOD m) ∧ ↑a1 ≡ ↑a2 (MOD n)
  rewrite [←Lemma_7_4_5 _ _ h1] at h5  --h5 : ↑a1 ≡ ↑a2 (MOD m * n)
  rewrite [congr_iff_mod_eq_Nat] at h5 --h5 : a1 % (m * n) = a2 % (m * n)
  rewrite [Nat.mod_eq_of_lt h2.right, Nat.mod_eq_of_lt h3.right] at h5
  show a1 = a2 from h5
  done

lemma mod_elt_set_rp_below {a m : Nat} [NeZero m] (h1 : rel_prime m a) :
    a % m ∈ set_rp_below m := by
  define                  --Goal : rel_prime m (a % m) ∧ a % m < m
  rewrite [rel_prime_mod] --Goal : rel_prime m a ∧ a % m < m
  show rel_prime m a ∧ a % m < m from
    And.intro h1 (mod_nonzero_lt a (NeZero.ne m))
  done

lemma mod_mod_image {m n : Nat} (h1 : rel_prime m n) :
    image (mod_mod m n) (set_rp_below (m * n)) =
      (set_rp_below m) ×ₛ (set_rp_below n) := by
  apply Set.ext
  fix (b, c) : Nat × Nat
  apply Iff.intro
  · -- (→)
    assume h2 : (b, c) ∈ image (mod_mod m n) (set_rp_below (m * n))
    define at h2
    obtain (a : Nat)
      (h3 : a ∈ set_rp_below (m * n) ∧ mod_mod m n a = (b, c)) from h2
    rewrite [set_rp_below_def, mod_mod_def] at h3
    have h4 : rel_prime (m * n) a := h3.left.left
    rewrite [Lemma_7_4_6] at h4   --h4 : rel_prime m a ∧ rel_prime n a
    have h5 : a % m = b ∧ a % n = c := Prod.mk.inj h3.right
    define
    rewrite [←h5.left, ←h5.right]
      --Goal : a % m ∈ set_rp_below m ∧ a % n ∈ set_rp_below n
    have h6 : m * n ≠ 0 := by linarith
    have h7 : NeZero m := left_NeZero_of_mul h6
    have h8 : NeZero n := right_NeZero_of_mul h6
    apply And.intro
    · -- Proof that a % m ∈ set_rp_below m
      show a % m ∈ set_rp_below m from mod_elt_set_rp_below h4.left
      done
    · -- Proof that a % n ∈ set_rp_below n
      show a % n ∈ set_rp_below n from mod_elt_set_rp_below h4.right
      done
    done
  · -- (←)
    assume h2 : (b, c) ∈ set_rp_below m ×ₛ set_rp_below n
    rewrite [set_prod_def, set_rp_below_def, set_rp_below_def] at h2
      --h2 : (rel_prime m b ∧ b < m) ∧ (rel_prime n c ∧ c < n)
    define
    have h3 : m ≠ 0 := by linarith
    have h4 : n ≠ 0 := by linarith
    rewrite [←neZero_iff] at h3
    rewrite [←neZero_iff] at h4
    obtain (a : Nat) (h5 : a < m * n ∧ a ≡ b (MOD m) ∧ a ≡ c (MOD n))
      from Lemma_7_4_7 h1 b c
    apply Exists.intro a
    apply And.intro
    · -- Proof of a ∈ set_rp_below (m * n)
      define                  --Goal : rel_prime (m * n) a ∧ a < m * n
      apply And.intro _ h5.left
      rewrite [Lemma_7_4_6]   --Goal : rel_prime m a ∧ rel_prime n a
      rewrite [congr_rel_prime h5.right.left,
        congr_rel_prime h5.right.right]
      show rel_prime m b ∧ rel_prime n c from
        And.intro h2.left.left h2.right.left
      done
    · -- Proof of mod_mod m n a = (b, c)
      rewrite [congr_iff_mod_eq_Nat, congr_iff_mod_eq_Nat] at h5
      rewrite [mod_mod_def, h5.right.left, h5.right.right]
        --Goal : (b % m, c % n) = (b, c)
      rewrite [Nat.mod_eq_of_lt h2.left.right,
        Nat.mod_eq_of_lt h2.right.right]
      rfl
      done
    done
  done

lemma set_rp_below_prod {m n : Nat} (h1 : rel_prime m n) :
    set_rp_below (m * n) ∼ (set_rp_below m) ×ₛ (set_rp_below n) := by
  rewrite [←mod_mod_image h1]
  show set_rp_below (m * n) ∼
    image (mod_mod m n) (set_rp_below (m * n)) from
    equinum_image (mod_mod_one_one_on h1)
  done

We finally have everything we need to prove Theorem 7.4.4.

lemma eq_numElts_of_equinum {U V : Type} {A : Set U} {B : Set V} {n : Nat}
    (h1 : A ∼ B) (h2 : numElts A n) : numElts B n := by
  rewrite [numElts_def] at h2   --h2 : I n ∼ A
  rewrite [numElts_def]         --Goal : I n ∼ B
  show I n ∼ B from Theorem_8_1_3_3 h2 h1
  done

theorem Theorem_7_4_4 {m n : Nat} (h1 : rel_prime m n) :
    phi (m * n) = (phi m) * (phi n) := by
  have h2 : numElts (set_rp_below m) (phi m) := phi_is_numElts m
  have h3 : numElts (set_rp_below n) (phi n) := phi_is_numElts n
  have h4 : numElts (set_rp_below (m * n)) (phi (m * n)) :=
    phi_is_numElts (m * n)
  have h5 : numElts (set_rp_below m ×ₛ set_rp_below n) (phi (m * n)) :=
    eq_numElts_of_equinum (set_rp_below_prod h1) h4
  have h6 : numElts (set_rp_below m ×ₛ set_rp_below n) (phi m * phi n) :=
    numElts_prod h2 h3
  show phi (m * n) = phi m * phi n from Exercise_8_1_6b h5 h6
  done

Exercises

lemma image_empty {U : Type} {A : Set U}
    (f : U → Nat) (h : empty A) : image f A = I 0 := sorry

lemma remove_one_equinum
    {U V : Type} {A : Set U} {B : Set V} {a : U} {b : V} {f : U → V}
    (h1 : one_one_on f A) (h2 : image f A = B)
    (h3 : a ∈ A) (h4 : f a = b) : ↑(A \ {a}) ∼ ↑(B \ {b}) := sorry

lemma singleton_of_diff_empty {U : Type} {A : Set U} {a : U}
    (h1 : a ∈ A) (h2 : empty (A \ {a})) : A = {a} := sorry

lemma eq_zero_of_I_zero_equinum {n : Nat} (h : I 0 ∼ I n) : n = 0 := sorry

--Hint: Use mathematical induction.
theorem Exercise_8_1_6a : ∀ ⦃m n : Nat⦄, (I m ∼ I n) → m = n := sorry

theorem Exercise_8_1_6b {U : Type} {A : Set U} {m n : Nat}
    (h1 : numElts A m) (h2 : numElts A n) : m = n := sorry

lemma neb_nrpb (m : Nat) : ∀ ⦃k : Nat⦄, k ≤ m →
    num_elts_below (set_rp_below m) k = num_rp_below m k := sorry

--Hint:  You might find it helpful to apply the theorem div_mod_char
--from the exercises of Section 6.4.
lemma qr_image (m n : Nat) :
    image (qr n) (I (m * n)) = I m ×ₛ I n := sorry

Suppose U and V are types, A and C have type Set U, and we have two functions f : A → V and g : C → V. Then we can define a new function func_union f g : A ∪ C → V as follows:

lemma is_elt_snd_of_not_fst {U : Type} {A C : Set U} {x : U}
    (h1 : x ∈ A ∪ C) (h2 : x ∉ A) : x ∈ C := by
  disj_syll h1 h2
  show x ∈ C from h1
  done

def elt_snd_of_not_fst {U : Type} {A C : Set U} {x : ↑(A ∪ C)}
  (h : x.val ∉ A) : C :=
  Subtype_elt (is_elt_snd_of_not_fst x.property h)

noncomputable def func_union {U V : Type} {A C : Set U}
  (f : A → V) (g : C → V) (x : ↑(A ∪ C)) : V :=
  if test : x.val ∈ A then f (Subtype_elt test)
    else g (elt_snd_of_not_fst test)

Note that in the definition of func_union, we have test : x.val ∈ A in the then clause and test : x.val ∉ A in the else clause. If x.val ∈ A then the value of func_union f g x is determined by f, and if x.val ∉ A then it is determined by g. The next two exercises ask you to prove properties of this function

lemma func_union_one_one {U V : Type} {A C : Set U}
    {f : A → V} {g : C → V} (h1 : empty (range f ∩ range g))
    (h2 : one_to_one f) (h3 : one_to_one g) :
    one_to_one (func_union f g) := sorry

lemma func_union_range {U V : Type} {A C : Set U}
    (f : A → V) (g : C → V) (h : empty (A ∩ C)) :
    range (func_union f g) = range f ∪ range g := sorry

--Hint:  Use the last two exercises.
theorem Theorem_8_1_2_2
    {U V : Type} {A C : Set U} {B D : Set V}
    (h1 : empty (A ∩ C)) (h2 : empty (B ∩ D))
    (h3 : A ∼ B) (h4 : C ∼ D) : ↑(A ∪ C) ∼ ↑(B ∪ D) := sorry

lemma shift_I_equinum (n m : Nat) : I m ∼ ↑(I (n + m) \ I n) := sorry

theorem Theorem_8_1_7 {U : Type} {A B : Set U} {n m : Nat}
    (h1 : empty (A ∩ B)) (h2 : numElts A n) (h3 : numElts B m) :
    numElts (A ∪ B) (n + m) := sorry

theorem equinum_sub {U V : Type} {A C : Set U} {B : Set V}
    (h1 : A ∼ B) (h2 : C ⊆ A) : ∃ (D : Set V), D ⊆ B ∧ C ∼ D := sorry

theorem Exercise_8_1_8b {U : Type} {A B : Set U}
    (h1 : finite A) (h2 : B ⊆ A) : finite B := sorry

theorem finite_bdd {A : Set Nat} (h : finite A) :
    ∃ (m : Nat), ∀ n ∈ A, n < m := sorry

lemma N_not_finite : ¬finite Nat := sorry

theorem denum_not_finite (U : Type)
    (h : denum U) : ¬finite U := sorry

--Hint:  Use Like_Exercise_6_2_16 from the exercises of Section 6.2.
theorem Exercise_6_2_16 {U : Type} {f : U → U}
    (h1 : one_to_one f) (h2 : finite U) : onto f := sorry

8.2. Countable and Uncountable Sets

Section 8.2 of HTPI shows that many set-theoretic operations, when applied to countable sets, produce results that are countable. For example, the first part of Theorem 8.2.1 shows that a Cartesian product of countable sets is countable. Our proof of this statement in Lean is based on Theorem_8_1_2_1_set and the denumerability of Nat × Nat. We also use an exercise from Section 8.1.

theorem NxN_denum : denum (Nat × Nat) := Theorem_8_1_3_2 NxN_equinum_N

theorem Theorem_8_2_1_1 {U V : Type} {A : Set U} {B : Set V}
    (h1 : ctble A) (h2 : ctble B) : ctble (A ×ₛ B) := by
  rewrite [ctble_iff_set_nat_equinum] at h1
  rewrite [ctble_iff_set_nat_equinum] at h2
  obtain (J : Set Nat) (h3 : J ∼ A) from h1
  obtain (K : Set Nat) (h4 : K ∼ B) from h2
  have h5 : J ×ₛ K ∼ A ×ₛ B := Theorem_8_1_2_1_set h3 h4
  have h6 : ctble (Nat × Nat) := Or.inr NxN_denum
  have h7 : ctble (J ×ₛ K) := ctble_set_of_ctble_type h6 (J ×ₛ K)
  show ctble (A ×ₛ B) from ctble_of_ctble_equinum h5 h7
  done

The second part of Theorem 8.2.1 shows that a union of two countable sets is countable, but, as we ask you to show in the exercises, it is superseded by Theorem 8.2.2, which says that a union of a countable family of countable sets is countable. So we will skip ahead to Theorem 8.2.2. Here’s how we state the theorem in Lean:

theorem Theorem_8_2_2 {U : Type} {F : Set (Set U)}
    (h1 : ctble F) (h2 : ∀ A ∈ F, ctble A) : ctble (⋃₀ F)

As in the proof in HTPI, we will use the characterization of countability from Theorem_8_1_5_2. We first consider the case in which F is nonempty and also all elements of F are nonempty. According to Theorem_8_1_5_2, the hypotheses h1 and h2 then imply that there is a function j : Nat → Set U such that F ⊆ range j, and also for each A ∈ F there is a function gA : Nat → U with A ⊆ range gA. We begin by proving an easier version of the theorem, where we assume that we have a function g from Set U to Nat → U that supplies, for each A ∈ F, the required function gA. Imitating the proof in HTPI, we can use j and g to construct the function needed to prove that ⋃₀ F is countable.

lemma Lemma_8_2_2_1 {U : Type} {F : Set (Set U)} {g : Set U → Nat → U}
    (h1 : ctble F) (h2 : ¬empty F) (h3 : ∀ A ∈ F, A ⊆ range (g A)) :
    ctble (⋃₀ F) := by
  rewrite [Theorem_8_1_5_2] at h1
  disj_syll h1 h2               --h1 : ∃ (f : Nat → Set U), F ⊆ range f
  rewrite [Theorem_8_1_5_2]
  apply Or.inr                  --Goal : ∃ (f : Nat → Set U), ⋃₀F ⊆ range f
  obtain (j : Nat → Set U) (h4 : F ⊆ range j) from h1
  obtain (p : Nat → Nat × Nat) (h5 : one_to_one p ∧ onto p) from NxN_denum
  set f : Nat → U := fun (n : Nat) => g (j (p n).1) (p n).2
  apply Exists.intro f
  fix x : U
  assume h6 : x ∈ ⋃₀ F
  obtain (A : Set U) (h7 : A ∈ F ∧ x ∈ A) from h6
  obtain (n1 : Nat) (h8 : j n1 = A) from h4 h7.left
  obtain (n2 : Nat) (h9 : g A n2 = x) from h3 A h7.left h7.right
  obtain (n : Nat) (h10 : p n = (n1, n2)) from h5.right (n1, n2)
  apply Exists.intro n
  show f n = x from
    calc f n
      _ = g (j (p n).1) (p n).2 := by rfl
      _ = g (j n1) n2 := by rw [h10]
      _ = g A n2 := by rw [h8]
      _ = x := by rw [h9]
  done

How can we use Lemma_8_2_2_1 to prove Theorem_8_2_2 (still assuming that F and every element of F are nonempty)? We must use the hypothesis h2 : ∀ A ∈ F, ctble A in Theorem_8_2_2 to produce the function g required in Lemma_8_2_2_1. As we have already observed, Theorem_8_1_5_2 guarantees that for each A ∈ F, an appropriate function gA : Nat → U exists. We need a function g that will choose such a function gA for each A. A function with this property is often called a choice function. And now we come to a delicate point that was skipped over in HTPI: to prove the existence of a choice function, we must use a statement called the axiom of choice.¹

The distinction between the existence of an appropriate function gA for each A and the existence of a function that chooses such a function for each A is a subtle one. Perhaps for this reason, many people find the axiom of choice to be intuitively obvious. HTPI took advantage of this intuition to skip over this step in the proof without comment. But of course Lean won’t let us skip anything!

To implement the axiom of choice, Lean uses a function called Classical.choose. Given a proof h of a statement of the form ∃ (x : U), P x, the expression Classical.choose h produces (“chooses”) some u : U such that P u is true. There is also a theorem Classical.choose_spec that guarantees that the Classical.choose function meets its specification—that is, P (Classical.choose h) is true. Using these, we can prove a lemma that will bridge the gap between Lemma_8_2_2_1 and Theorem_8_2_2.

lemma Lemma_8_2_2_2 {U : Type} {F : Set (Set U)} (h1 : ∀ A ∈ F, ctble A)
    (h2 : ¬empty F) (h3 : ∀ A ∈ F, ¬empty A):
    ∃ (g : Set U → Nat → U), ∀ A ∈ F, A ⊆ range (g A) := by
  have h4 : ∀ (A : Set U), ∃ (gA : Nat → U),
      A ∈ F → A ⊆ range gA := by
    fix A : Set U
    by_cases h4 : A ∈ F
    · -- Case 1. h4 : A ∈ F
      have h5 : ctble A := h1 A h4
      rewrite [Theorem_8_1_5_2] at h5
      disj_syll h5 (h3 A h4)    --h5 : ∃ (f : Nat → U), A ⊆ range f
      obtain (gA : Nat → U) (h6 : A ⊆ range gA) from h5
      apply Exists.intro gA
      assume h7 : A ∈ F
      show A ⊆ range gA from h6
      done
    · -- Case 2. h4 : A ∉ F
      rewrite [not_empty_iff_exists_elt] at h2
      obtain (A0 : Set U) (h5 : A0 ∈ F) from h2
      have h6 : ¬empty A0 := h3 A0 h5
      rewrite [not_empty_iff_exists_elt] at h6
      obtain (x0 : U) (h7 : x0 ∈ A0) from h6
      set gA : Nat → U := constant_func Nat x0
      apply Exists.intro gA
      contrapos
      assume h8 : A ⊈ range gA
      show A ∉ F from h4
      done
    done
  set g : Set U → Nat → U := fun (A : Set U) => Classical.choose (h4 A)
  apply Exists.intro g
  fix A : Set U
  show A ∈ F → A ⊆ range (g A) from Classical.choose_spec (h4 A)
  done

Notice that the domain of the function g in Lemma_8_2_2_2 is Set U, not F. Thus, we must produce a function gA for every A : Set U, but it is only when A ∈ F that we care what gA is. Thus, the proof above just picks a default value (constant_func Nat x0) when A ∉ F.

We can now prove the theorem, still under the assumption that all elements of F are nonempty. If F is empty, then we can show that ⋃₀ F is empty, so it has zero elements, which implies that it is finite and therefore countable. If F is not empty, then we can combine Lemma_8_2_2_1 and Lemma_8_2_2_2 to prove the theorem.

lemma Lemma_8_2_2_3 {U : Type} {F : Set (Set U)}
    (h1 : ctble F) (h2 : ∀ A ∈ F, ctble A) (h3 : ∀ A ∈ F, ¬empty A) :
    ctble (⋃₀ F) := by
  by_cases h4 : empty F
  · -- Case 1. h4 : empty F
    have h5 : empty (⋃₀ F) := by
      contradict h4 with h5
      rewrite [not_empty_iff_exists_elt] at h5
      obtain (x : U) (h6 : x ∈ ⋃₀ F) from h5
      obtain (A : Set U) (h7 : A ∈ F ∧ x ∈ A) from h6
      show ∃ (x : Set U), x ∈ F from Exists.intro A h7.left
      done
    rewrite [←zero_elts_iff_empty] at h5    --h5 : numElts (⋃₀ F) 0
    define
    apply Or.inl
    rewrite [finite_def]
    show ∃ (n : Nat), numElts (⋃₀ F) n from Exists.intro 0 h5
    done
  · -- Case 2. h4 : ¬empty F
    obtain (g : Set U → Nat → U) (h5 : ∀ A ∈ F, A ⊆ range (g A)) from
      Lemma_8_2_2_2 h2 h4 h3
    show ctble (⋃₀ F) from Lemma_8_2_2_1 h1 h4 h5
    done

Finally, we deal with the possibility that F contains the empty set. As in HTPI, we show that we can simply remove the empty set from F and then apply our earlier reasoning.

lemma remove_empty_subset {U : Type} (F : Set (Set U)) :
    {A : Set U | A ∈ F ∧ ¬empty A} ⊆ F := by
  fix X : Set U
  assume h1 : X ∈ {A : Set U | A ∈ F ∧ ¬empty A}
  define at h1
  show X ∈ F from h1.left
  done

lemma remove_empty_union_eq {U : Type} (F : Set (Set U)) :
    ⋃₀ {A : Set U | A ∈ F ∧ ¬empty A} = ⋃₀ F := sorry

theorem Theorem_8_2_2 {U : Type} {F : Set (Set U)}
    (h1 : ctble F) (h2 : ∀ A ∈ F, ctble A) : ctble (⋃₀ F) := by
  set G : Set (Set U) := {A : Set U | A ∈ F ∧ ¬empty A}
  have h3 : G ⊆ F := remove_empty_subset F
  have h4 : ⋃₀ G = ⋃₀ F := remove_empty_union_eq F
  rewrite [←h4]
  have h5 : ctble G := Exercise_8_1_17 h3 h1
  have h6 : ∀ A ∈ G, ctble A := by
    fix A : Set U
    assume h6 : A ∈ G
    show ctble A from h2 A (h3 h6)
    done
  have h7 : ∀ A ∈ G, ¬empty A := by
    fix A : Set U
    assume h7 : A ∈ G
    define at h7
    show ¬empty A from h7.right
    done
  show ctble (⋃₀ G) from Lemma_8_2_2_3 h5 h6 h7
  done

By the way, we can now explain a mystery from Section 5.1. The reason we skipped the proof of the right-to-left direction of func_from_graph is that the proof uses Classical.choose and Classical.choose_spec. Now that you know about this function and theorem, we can show you the proof.

theorem func_from_graph_rtl {A B : Type} (F : Set (A × B)) :
    is_func_graph F → (∃ (f : A → B), graph f = F) := by
  assume h1 : is_func_graph F
  define at h1    --h1 : ∀ (x : A), ∃! (y : B), (x, y) ∈ F
  have h2 : ∀ (x : A), ∃ (y : B), (x, y) ∈ F := by
    fix x : A
    obtain (y : B) (h3 : (x, y) ∈ F)
      (h4 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x
    show ∃ (y : B), (x, y) ∈ F from Exists.intro y h3
    done
  set f : A → B := fun (x : A) => Classical.choose (h2 x)
  apply Exists.intro f
  apply Set.ext
  fix (x, y) : A × B
  have h3 : (x, f x) ∈ F := Classical.choose_spec (h2 x)
  apply Iff.intro
  · -- (→)
    assume h4 : (x, y) ∈ graph f
    define at h4        --h4 : f x = y
    rewrite [h4] at h3
    show (x, y) ∈ F from h3
    done
  · -- (←)
    assume h4 : (x, y) ∈ F
    define              --Goal : f x = y
    obtain (z : B) (h5 : (x, z) ∈ F)
      (h6 : ∀ (y1 y2 : B), (x, y1) ∈ F → (x, y2) ∈ F → y1 = y2) from h1 x
    show f x = y from h6 (f x) y h3 h4
    done
  done

There is one more theorem in Section 8.2 of HTPI showing that a set-theoretic operation, when applied to a countable set, gives a countable result. Theorem 8.2.4 says that if a set \(A\) is countable, then the set of all finite sequences of elements of \(A\) is also countable. In HTPI, finite sequences are represented by functions, but in Lean it is easier to use lists. Thus, if A has type Set U, then we define a finite sequence of elements of A to be a list l : List U with the property that every entry of l is an element of A. Letting seq A denote the set of all finite sequences of elements of A, our version of Theorem 8.2.4 will say that if A is countable, then so is seq A.

def seq {U : Type} (A : Set U) : Set (List U) :=
  {l : List U | ∀ x ∈ l, x ∈ A}

lemma seq_def {U : Type} (A : Set U) (l : List U) :
    l ∈ seq A ↔ ∀ x ∈ l, x ∈ A := by rfl

theorem Theorem_8_2_4 {U : Type} {A : Set U}
    (h1 : ctble A) : ctble (seq A)

Our proof of Theorem_8_2_4 will use exactly the same strategy as the proof in HTPI. We begin by showing that, for every natural number n, the set of sequences of elements of A of length n is countable. The proof is by mathematical induction. The base case is easy, because the only sequence of length 0 is the nil list.

def seq_by_length {U : Type} (A : Set U) (n : Nat) : Set (List U) :=
  {l : List U | l ∈ seq A ∧ l.length = n}

lemma sbl_base {U : Type} (A : Set U) : seq_by_length A 0 = {[]} := by
  apply Set.ext
  fix l : List U
  apply Iff.intro
  · -- (→)
    assume h1 : l ∈ seq_by_length A 0
    define at h1   --h1 : l ∈ seq A ∧ l.length = 0
    rewrite [List.length_eq_zero_iff] at h1
    define
    show l = [] from h1.right
    done
  · -- (←)
    assume h1 : l ∈ {[]}
    define at h1     --h1 : l = []
    define           --Goal : l ∈ seq A ∧ l.length = 0
    apply And.intro _ (List.length_eq_zero_iff.rtl h1)
    define           --Goal : ∀ x ∈ l, x ∈ A
    fix x : U
    contrapos
    assume h2 : x ∉ A
    rewrite [h1]
    show x ∉ [] from List.not_mem_nil
    done
  done

For the induction step, the key idea is that A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1). To prove this, we define a function seq_cons U that matches up A ×ₛ (seq_by_length A n) with seq_by_length A (n + 1).

def seq_cons (U : Type) (p : U × (List U)) : List U := p.1 :: p.2

lemma seq_cons_def {U : Type} (x : U) (l : List U) :
    seq_cons U (x, l) = x :: l := by rfl

lemma seq_cons_one_one (U : Type) : one_to_one (seq_cons U) := by
  fix (a1, l1) : U × List U; fix (a2, l2) : U × List U
  assume h1 : seq_cons U (a1, l1) = seq_cons U (a2, l2)
  rewrite [seq_cons_def, seq_cons_def] at h1  --h1 : a1 :: l1 = a2 :: l2
  rewrite [List.cons_eq_cons] at h1           --h1 : a1 = a2 ∧ l1 = l2
  rewrite [h1.left, h1.right]
  rfl
  done

lemma seq_cons_image {U : Type} (A : Set U) (n : Nat) :
    image (seq_cons U) (A ×ₛ (seq_by_length A n)) =
      seq_by_length A (n + 1) := sorry

lemma Lemma_8_2_4_1 {U : Type} (A : Set U) (n : Nat) :
    A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1) := by
  rewrite [←seq_cons_image A n]
  show A ×ₛ seq_by_length A n ∼
    image (seq_cons U) (A ×ₛ seq_by_length A n) from equinum_image
    (one_one_on_of_one_one (seq_cons_one_one U) (A ×ₛ (seq_by_length A n)))
  done

With this preparation, we can now use singleton_one_elt to justify the base case of our induction proof and Theorem_8_2_1_1 for the induction step.

lemma Lemma_8_2_4_2 {U : Type} {A : Set U} (h1 : ctble A) :
    ∀ (n : Nat), ctble (seq_by_length A n) := by
  by_induc
  · -- Base Case
    rewrite [sbl_base]   --Goal : ctble {[]}
    define
    apply Or.inl         --Goal : finite {[]}
    rewrite [finite_def]
    apply Exists.intro 1 --Goal : numElts {[]} 1
    show numElts {[]} 1 from singleton_one_elt []
    done
  · -- Induction Step
    fix n : Nat
    assume ih : ctble (seq_by_length A n)
    have h2 : A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1) :=
      Lemma_8_2_4_1 A n
    have h3 : ctble (A ×ₛ (seq_by_length A n)) := Theorem_8_2_1_1 h1 ih
    show ctble (seq_by_length A (n + 1)) from ctble_of_ctble_equinum h2 h3
    done
  done

Our next step is to show that the union of all of the sets seq_by_length A n, for n : Nat, is seq A.

def sbl_set {U : Type} (A : Set U) : Set (Set (List U)) :=
  {S : Set (List U) | ∃ (n : Nat), seq_by_length A n = S}

lemma Lemma_8_2_4_3 {U : Type} (A : Set U) : ⋃₀ (sbl_set A) = seq A := by
  apply Set.ext
  fix l : List U
  apply Iff.intro
  · -- (→)
    assume h1 : l ∈ ⋃₀ (sbl_set A)
    define at h1
    obtain (S : Set (List U)) (h2 :  S ∈ sbl_set A ∧ l ∈ S) from h1
    have h3 : S ∈ sbl_set A := h2.left
    define at h3
    obtain (n : Nat) (h4 : seq_by_length A n = S) from h3
    have h5 : l ∈ S := h2.right
    rewrite [←h4] at h5
    define at h5
    show l ∈ seq A from h5.left
    done
  · -- (←)
    assume h1 : l ∈ seq A
    define
    set n : Nat := l.length
    apply Exists.intro (seq_by_length A n)
    apply And.intro
    · -- Proof of seq_by_length A n ∈ sbl_set A
      define
      apply Exists.intro n
      rfl
      done
    · -- Proof of l ∈ seq_by_length A n
      define
      apply And.intro h1
      rfl
      done
    done
  done

Of course, sbl_set A is countable. The easiest way to prove this is to note that seq_by_length A is a function from Nat to Set (List U) whose range contains all of the sets in sbl_set A.

lemma Lemma_8_2_4_4 {U : Type} (A : Set U) : ctble (sbl_set A) := by
  rewrite [Theorem_8_1_5_2]
  apply Or.inr   --Goal : ∃ (f : Nat → Set (List U)), sbl_set A ⊆ range f
  apply Exists.intro (seq_by_length A)
  fix S : Set (List U)
  assume h1 : S ∈ sbl_set A
  define at h1; define
  show ∃ (x : Nat), seq_by_length A x = S from h1
  done

We now have everything we need to prove Theorem_8_2_4 as an application of Theorem_8_2_2.

theorem Theorem_8_2_4 {U : Type} {A : Set U}
    (h1 : ctble A) : ctble (seq A) := by
  set F : Set (Set (List U)) := sbl_set A
  have h2 : ctble F := Lemma_8_2_4_4 A
  have h3 : ∀ S ∈ F, ctble S := by
    fix S : Set (List U)
    assume h3 : S ∈ F
    define at h3
    obtain (n : Nat) (h4 : seq_by_length A n = S) from h3
    rewrite [←h4]
    show ctble (seq_by_length A n) from Lemma_8_2_4_2 h1 n
    done
  rewrite [←Lemma_8_2_4_3 A]
  show ctble (⋃₀ sbl_set A) from Theorem_8_2_2 h2 h3
  done

There is a set-theoretic operation that can produce an uncountable set from a countable set: the power set operation. HTPI demonstrates this by proving Cantor’s theorem (Theorem 8.2.5), which says that \(\mathscr{P}(\mathbb{Z}^+)\) is uncountable. The strategy for this proof is tricky; it involves defining a set \(D\) using a method called diagonalization. For an explanation of the motivation behind this strategy, see HTPI.

Here we will prove in Lean that the collection of all sets of natural numbers is uncountable. There is no need to use the power set operation for this, because we have a type, namely Set Nat, that contains all sets of natural numbers. So our Lean version of Cantor’s theorem says that Set Nat is uncountable.

theorem Cantor's_theorem : ¬ctble (Set Nat) := by
  by_contra h1
  rewrite [ctble_iff_set_nat_equinum] at h1
  obtain (J : Set Nat) (h2 : J ∼ Set Nat) from h1
  obtain (F : J → Set Nat) (h3 : one_to_one F ∧ onto F) from h2
  set f : Nat → Set Nat := func_extend F ∅
  set D : Set Nat := {n : Nat | n ∉ f n}
  obtain (nJ : J) (h4 : F nJ = D) from h3.right D
  set n : Nat := nJ.val
  have h5 : n ∈ D ↔ n ∉ f n := by rfl
  have h6 : f n = F nJ := fe_elt F ∅ nJ
  rewrite [h6, h4] at h5      --h5 : n ∈ D ↔ n ∉ D
  by_cases h7 : n ∈ D
  · -- Case 1. h7 : n ∈ D
    contradict h7
    show n ∉ D from h5.ltr h7
    done
  · -- Case 2. h7 : n ∉ D
    contradict h7
    show n ∈ D from h5.rtl h7
    done
  done

As a consequence of Theorem 8.2.5, HTPI shows that \(\mathbb{R}\) is uncountable. The proof is not hard, but it requires facts about the decimal expansions of real numbers. Developing those facts in Lean would take us too far afield, so we will skip the proof.

Exercises

lemma pair_ctble {U : Type}
    (a b : U) : ctble ↑({a, b} : Set U) := sorry

--Hint:  Use the previous exercise and Theorem_8_2_2.
theorem Theorem_8_2_1_2 {U : Type} {A B : Set U}
    (h1 : ctble A) (h2 : ctble B) : ctble ↑(A ∪ B) := sorry

lemma remove_empty_union_eq {U : Type} (F : Set (Set U)) :
    ⋃₀ {A : Set U | A ∈ F ∧ ¬empty A} = ⋃₀ F := sorry

lemma seq_cons_image {U : Type} (A : Set U) (n : Nat) :
    image (seq_cons U) (A ×ₛ (seq_by_length A n)) =
      seq_by_length A (n + 1) := sorry

--Hint:  Apply Theorem_8_2_4 to the set Univ U.
theorem Theorem_8_2_4_type {U : Type}
    (h : ctble U) : ctble (List U) := sorry

def list_to_set (U : Type) (l : List U) : Set U := {x : U | x ∈ l}

lemma list_to_set_def (U : Type) (l : List U) (x : U) :
    x ∈ list_to_set U l ↔ x ∈ l := by rfl

--Hint:  Use induction on the size of A.
lemma set_from_list {U : Type} {A : Set U} (h : finite A) :
    ∃ (l : List U), list_to_set U l = A := sorry

--Hint:  Use the previous exercise and Theorem_8_2_4_type.
theorem Like_Exercise_8_2_4 (U : Type) (h : ctble U) :
    ctble {X : Set U | finite X} := sorry

theorem Exercise_8_2_6b (U V W : Type) :
     ((U × V) → W) ∼ (U → V → W) := sorry

theorem Like_Exercise_8_2_7 : ∃ (P : Set (Set Nat)),
    partition P ∧ denum P ∧ ∀ X ∈ P, denum X := sorry

theorem unctbly_many_inf_set_nat :
    ¬ctble {X : Set Nat | ¬finite X} := sorry

theorem Exercise_8_2_8 {U : Type} {A B : Set U}
    (h : empty (A ∩ B)) : 𝒫 (A ∪ B) ∼ 𝒫 A ×ₛ 𝒫 B := sorry

8.3. The Cantor–Schröder–Bernstein Theorem

The final section of HTPI proves the Cantor–Schröder–Bernstein theorem. The theorem says that if we have two sets such that there is a one-to-one function from each set to the other, then the two sets are equinumerous. We will prove it in Lean for types, but of course we can apply it to sets as well by coercing the sets to subtypes.

theorem Cantor_Schroeder_Bernstein_theorem
    {U V : Type} {f : U → V} {g : V → U}
    (h1 : one_to_one f) (h2 : one_to_one g) : U ∼ V

To prove the theorem, we must produce a one-to-one, onto function h from U to V. Imitating the proof in HTPI, we will do this by defining a set X : Set U and then using f to determine the values of h on elements of the domain that belong to X and the inverse of g for those that don’t. That is, the graph of h will be the set csb_func_graph f g X defined as follows:

def csb_func_graph {U V : Type}
  (f : U → V) (g : V → U) (X : Set U) : Set (U × V) :=
  {(x, y) : U × V | (x ∈ X ∧ f x = y) ∨ (x ∉ X ∧ g y = x)}

Is csb_func_graph f g X the graph of a function? It is not hard to show that it is, as long as ∀ (x : U), x ∉ X → x ∈ range g. We first state lemmas spelling out the two cases in the definition of csb_func_graph f g X, leaving the proof of the second as an exercise for you.

lemma csb_func_graph_X {U V : Type} {X : Set U} {x : U}
    (f : U → V) (g : V → U) (h : x ∈ X) (y : V) :
    (x, y) ∈ csb_func_graph f g X ↔ f x = y := by
  apply Iff.intro
  · -- (→)
    assume h1 : (x, y) ∈ csb_func_graph f g X
    define at h1
    have h2 : ¬(x ∉ X ∧ g y = x) := by
      demorgan
      show x ∈ X ∨ g y ≠ x from Or.inl h
      done
    disj_syll h1 h2        --h1 : x ∈ X ∧ f x = y
    show f x = y from h1.right
    done
  · -- (←)
    assume h1 : f x = y
    define
    apply Or.inl
    show x ∈ X ∧ f x = y from And.intro h h1
    done
  done

lemma csb_func_graph_not_X {U V : Type} {X : Set U} {x : U}
    (f : U → V) (g : V → U) (h : x ∉ X) (y : V) :
    (x, y) ∈ csb_func_graph f g X ↔ g y = x := sorry

lemma csb_func_graph_is_func_graph {U V : Type} {g : V → U} {X : Set U}
    (f : U → V) (h1 : ∀ (x : U), x ∉ X → x ∈ range g) (h2 : one_to_one g) :
    is_func_graph (csb_func_graph f g X) := by
  define
  fix x : U
  by_cases h3 : x ∈ X
  · -- Case 1. h3 : x ∈ X
    exists_unique
    · -- Existence
      apply Exists.intro (f x)
      rewrite [csb_func_graph_X f g h3]
      rfl
      done
    · -- Uniqueness
      fix y1 : V; fix y2 : V
      assume h4 : (x, y1) ∈ csb_func_graph f g X
      assume h5 : (x, y2) ∈ csb_func_graph f g X
      rewrite [csb_func_graph_X f g h3] at h4  --h4 : f x = y1
      rewrite [csb_func_graph_X f g h3] at h5  --h5 : f x = y2
      rewrite [←h4, ←h5]
      rfl
      done
    done
  · -- Case 2. h3 : x ∉ X
    exists_unique
    · -- Existence
      obtain (y : V) (h4 : g y = x) from h1 x h3
      apply Exists.intro y
      rewrite [csb_func_graph_not_X f g h3]
      show g y = x from h4
      done
    · -- Uniqueness
      fix y1 : V; fix y2 : V
      assume h4 : (x, y1) ∈ csb_func_graph f g X
      assume h5 : (x, y2) ∈ csb_func_graph f g X
      rewrite [csb_func_graph_not_X f g h3] at h4 --h4 : g y1 = x
      rewrite [csb_func_graph_not_X f g h3] at h5 --h5 : g y2 = x
      rewrite [←h5] at h4
      show y1 = y2 from h2 y1 y2 h4
      done
    done
  done

Our plan is to define h to be the function whose graph is csb_func_graph f g X. With this definition, the value of h x for any x : U can be determined by a simple rule: if x ∈ X, then h x = f x, and if x ∉ X, then h x has the property that g (h x) = x:

lemma csb_func_X
    {U V : Type} {f h : U → V} {g : V → U} {X : Set U} {x : U}
    (h1 : graph h = csb_func_graph f g X) (h2 : x ∈ X) : h x = f x := by
  rewrite [←graph_def, h1, csb_func_graph_X f g h2]
  rfl
  done

lemma csb_func_not_X
    {U V : Type} {f h : U → V} {g : V → U} {X : Set U} {x : U}
    (h1 : graph h = csb_func_graph f g X) (h2 : x ∉ X) : g (h x) = x := by
  have h3 : (x, h x) ∈ graph h := by rfl
  rewrite [h1, csb_func_graph_not_X f g h2] at h3
  show g (h x) = x from h3
  done

We still have to say how X will be defined. Let A0 = {x : U | x ∉ range g}. To make sure that the condition ∀ (x : U), x ∉ X → x ∈ range g is satisfied, we will need to have A0 ⊆ X. As explained in HTPI, we can now get a suitable set X by repeatedly taking the image of A0 under g ∘ f. Fortunately, we defined functions in Section 6.5 that do what we need: rep_image (g ∘ f) n A0 is the result of taking the image of A0 under g ∘ f n times. That is, rep_image (g ∘ f) 0 A0 = A0, rep_image (g ∘ f) 1 A0 = image (g ∘ f) A0, rep_image (g ∘ f) 2 A0 = image (g ∘ f) (image (g ∘ f) A0), and so on. We will define X to be the union of all of the sets rep_image (g ∘ f) n A0, which is given by the function cumul_image (g ∘ f) A0.

To prove that h is one-to-one, we will need to know that it cannot happen that h x1 = h x2, x1 ∈ X, and x2 ∉ X. After proving this last lemma, we are ready to prove the Cantor–Schröder–Bernstein theorem.

lemma csb_X_of_X
    {U V : Type} {f h : U → V} {g : V → U} {A0 : Set U} {x1 x2 : U}
    (h1 : graph h = csb_func_graph f g (cumul_image (g ∘ f) A0))
    (h2 : h x1 = h x2) (h3 : x1 ∈ cumul_image (g ∘ f) A0) :
    x2 ∈ cumul_image (g ∘ f) A0 := by
  by_contra h4                      --h4 : x2 ∉ cumul_image (g ∘ f) A0
  rewrite [csb_func_X h1 h3] at h2  --h2 : f x1 = h x2
  have h5 : (g ∘ f) x1 = x2 :=
    calc (g ∘ f) x1
      _ = g (f x1) := by rfl
      _ = g (h x2) := by rw [h2]
      _ = x2 := csb_func_not_X h1 h4
  obtain (n : Nat) (h6 : x1 ∈ rep_image (g ∘ f) n A0) from h3
  contradict h4               --Goal : x2 ∈ cumul_image (g ∘ f) A0
  apply Exists.intro (n + 1)  --Goal : x2 ∈ rep_image (g ∘ f) (n + 1) A0
  rewrite [rep_image_step]
  apply Exists.intro x1
  show x1 ∈ rep_image (g ∘ f) n A0 ∧ (g ∘ f) x1 = x2 from
    And.intro h6 h5
  done

theorem Cantor_Schroeder_Bernstein_theorem
    {U V : Type} {f : U → V} {g : V → U}
    (h1 : one_to_one f) (h2 : one_to_one g) : U ∼ V := by
  set A0 : Set U := {x : U | x ∉ range g}
  set X : Set U := cumul_image (g ∘ f) A0
  set H : Set (U × V) := csb_func_graph f g X
  have h3 : ∀ (x : U), x ∉ X → x ∈ range g := by
    fix x : U
    contrapos
    assume h3 : x ∉ range g
    define
    apply Exists.intro 0
    rewrite [rep_image_base]
    show x ∈ A0 from h3
    done
  have h4 : is_func_graph H := csb_func_graph_is_func_graph f h3 h2
  rewrite [←func_from_graph] at h4
  obtain (h : U → V) (h5 : graph h = H) from h4
  apply Exists.intro h
  apply And.intro
  · -- proof that h is one-to-one
    fix x1 : U; fix x2 : U
    assume h6 : h x1 = h x2
    by_cases h7 : x1 ∈ X
    · -- Case 1. h7 : x1 ∈ X
      have h8 : x2 ∈ X := csb_X_of_X h5 h6 h7
      rewrite [csb_func_X h5 h7, csb_func_X h5 h8] at h6 --h6 : f x1 = f x2
      show x1 = x2 from h1 x1 x2 h6
      done
    · -- Case 2. h7 : x1 ∉ X
      have h8 : x2 ∉ X := by
        contradict h7 with h8
        show x1 ∈ X from csb_X_of_X h5 h6.symm h8
        done
      show x1 = x2 from
        calc x1
          _ = g (h x1) := (csb_func_not_X h5 h7).symm
          _ = g (h x2) := by rw [h6]
          _ = x2 := csb_func_not_X h5 h8
      done
    done
  · -- proof that h is onto
    fix y : V
    by_cases h6 : g y ∈ X
    · -- Case 1. h6 : g y ∈ X
      define at h6
      obtain (n : Nat) (h7 : g y ∈ rep_image (g ∘ f) n A0) from h6
      have h8 : n ≠ 0 := by
        by_contra h8
        rewrite [h8, rep_image_base] at h7 --h7 : g y ∈ A0
        define at h7                       --h7 : ¬∃ (x : V), g x = g y
        contradict h7
        apply Exists.intro y
        rfl
        done
      obtain (k : Nat) (h9 : n = k + 1) from
        exists_eq_add_one_of_ne_zero h8
      rewrite [h9, rep_image_step] at h7
      obtain (x : U)
        (h10 : x ∈ rep_image (g ∘ f) k A0 ∧ (g ∘ f) x = g y) from h7
      have h11 : g (f x) = g y := h10.right
      have h12 : f x = y := h2 (f x) y h11
      have h13 : x ∈ X := Exists.intro k h10.left
      apply Exists.intro x
      rewrite [csb_func_X h5 h13]
      show f x = y from h12
      done
    · -- Case 2. h6 : g y ∉ X
      apply Exists.intro (g y)
      have h7 : g (h (g y)) = g y := csb_func_not_X h5 h6
      show h (g y) = y from h2 (h (g y)) y h7
      done
    done
  done

Exercises

lemma csb_func_graph_not_X {U V : Type} {X : Set U} {x : U}
    (f : U → V) (g : V → U) (h : x ∉ X) (y : V) :
    (x, y) ∈ csb_func_graph f g X ↔ g y = x := sorry

theorem intervals_equinum :
    {x : Real | 0 < x ∧ x < 1} ∼ {x : Real | 0 < x ∧ x ≤ 1} := sorry

3. The following theorem could be thought of as an extensionality principle for relations. You may find it useful in later exercises. Hint for proof: First show that extension R = extension S, and then use the fact that R and S can be determined from extension R and extension S (see Section 4.3).

theorem relext {U V : Type} {R S : Rel U V}
    (h : ∀ (u : U) (v : V), R u v ↔ S u v) : R = S := sorry

The next six exercises lead up to a proof that the set of all equivalence relations on the natural numbers is equinumerous with the type Set Nat. These exercises use the following definitions:

def EqRel (U : Type) : Set (BinRel U) :=
  {R : BinRel U | equiv_rel R}

def Part (U : Type) : Set (Set (Set U)) :=
  {P : Set (Set U) | partition P}

def EqRelExt (U : Type) : Set (Set (U × U)) :=
  {E : Set (U × U) | ∃ (R : BinRel U), equiv_rel R ∧ extension R = E}

def shift_and_zero (X : Set Nat) : Set Nat :=
  {x + 2 | x ∈ X} ∪ {0}

def shift_and_zero_comp (X : Set Nat) : Set Nat :=
  {n : Nat | n ∉ shift_and_zero X}

def saz_pair (X : Set Nat) : Set (Set Nat) :=
  {shift_and_zero X, shift_and_zero_comp X}

theorem EqRel_equinum_Part (U : Type) : EqRel U ∼ Part U := sorry

theorem EqRel_equinum_EqRelExt (U : Type) :
    EqRel U ∼ EqRelExt U := sorry

theorem EqRel_Nat_to_Set_Nat :
    ∃ (f : EqRel Nat → Set Nat), one_to_one f := sorry

theorem saz_pair_part (X : Set Nat) : saz_pair X ∈ Part Nat := sorry

theorem Set_Nat_to_EqRel_Nat :
    ∃ (f : Set Nat → EqRel Nat), one_to_one f := sorry

theorem EqRel_Nat_equinum_Set_Nat : EqRel Nat ∼ Set Nat := sorry

---

1. The axiom of choice was first stated by Ernst Zermelo in 1904. You can learn more about it in Gregory H. Moore, Zermelo’s Axiom of Choice: Its Origins, Development, and Influence, Dover Publications, 2013. See also https://en.wikipedia.org/wiki/Axiom_of_choice.