Chap8.qmd

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

```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 `\~`).

```lean
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`:

```lean
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:

```lean
#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.

```lean
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

```lean
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.

```lean
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.

```lean
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`:

```lean
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.

```lean
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`:

```lean
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`.)

```lean
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:

```lean
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:

```lean
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:

```lean
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:

::: {.ind}
```
@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:

```lean
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*.

```lean
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.)

```lean
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:

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

```lean
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:

```lean
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:

```lean
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:

```lean
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 mentioned in *HTPI*; see Exercise 7 in Section 5.2 of *HTPI*.)  We can define the restriction of `f` to `A` in Lean as follows:

```lean
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`:

```lean
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:

```lean
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`:

```lean
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:

```lean
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.

```lean
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:

```lean
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:

```lean
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:

```lean
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:

```lean
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.

```lean
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`:

```lean
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.

```lean
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`.

```lean
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`.

```lean
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:

```lean
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 when `q` is written in lowest terms, `q.num` is the numerator, 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.

```lean
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

::: {.numex arguments="1"}
```lean
--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
```
:::

::: {.numex arguments="2"}
```lean
lemma fnz_fzn : fnz ∘ fzn = id  := sorry
```
:::

::: {.numex arguments="3"}
```lean
lemma tri_step (k : Nat) : tri (k + 1) = tri k + k + 1 := sorry
```
:::

::: {.numex arguments="4"}
```lean
lemma tri_incr {j k : Nat} (h1 : j ≤ k) : tri j ≤ tri k := sorry
```
:::

::: {.numex arguments="5"}
```lean
example {U V : Type} (f : U → V) : range f = Ran (graph f) := sorry
```
:::

::: {.numex arguments="6"}
```lean
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.
```lean
lemma ctble_of_ctble_equinum {U V : Type}
    (h1 : U ∼ V) (h2 : ctble U) : ctble V := sorry
```

::: {.numex arguments="8"}
```lean
theorem Exercise_8_1_1_b : denum {n : Int | even n} := sorry
```
:::

::: {.numex arguments="9"}
```lean
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`.
```lean
lemma image_comp_id {U V : Type} {f : U → V} {g : V → U}
    (h : g ∘ f = id) : (image g) ∘ (image f) = id := sorry
```

::: {.numex arguments="11"}
```lean
theorem Exercise_8_1_5_1 {U V : Type}
    (h : U ∼ V) : Set U ∼ Set V := sorry
```
:::

::: {.mdsk}
:::

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

```lean
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.

::: {.numex arguments="12"}
```lean
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
```
:::

::: {.numex arguments="13"}
```lean
lemma val_image_one_one {U : Type} (A : Set U) :
    one_to_one (val_image A) := sorry
```
:::

::: {.numex arguments="14"}
```lean
lemma range_val_image {U : Type} (A : Set U) :
    range (val_image A) = 𝒫 A := sorry
```
:::

::: {.numex arguments="15"}
```lean
lemma Set_equinum_powerset {U : Type} (A : Set U) :
    Set A ∼ 𝒫 A := sorry
```
:::

::: {.numex arguments="16"}
```lean
--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
```
:::

::: {.numex arguments="17"}
```lean
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.

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

::: {.numex arguments="19"}
```lean
theorem ctble_set_of_ctble_type {U : Type}
    (h : ctble U) (A : Set U) : ctble A := sorry
```
:::

::: {.numex arguments="20"}
```lean
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:

```lean
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.

```lean
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.

```lean
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.

```lean
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}`.

```lean
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}`.

```lean
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`.

```lean
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.

```lean
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.

```lean
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.

```lean
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.

```lean
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.

```lean
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:

```lean
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:

```lean
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.

```lean
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:

```lean
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`.

```lean
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)`.

```lean
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:

```lean
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`.

```lean
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.

```lean
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

::: {.numex arguments="1"}
```lean
lemma image_empty {U : Type} {A : Set U}
    (f : U → Nat) (h : empty A) : image f A = I 0 := sorry
```
:::

::: {.numex arguments="2"}
```lean
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
```
:::

::: {.numex arguments="3"}
```lean
lemma singleton_of_diff_empty {U : Type} {A : Set U} {a : U}
    (h1 : a ∈ A) (h2 : empty (A \ {a})) : A = {a} := sorry
```
:::

::: {.numex arguments="4"}
```lean
lemma eq_zero_of_I_zero_equinum {n : Nat} (h : I 0 ∼ I n) : n = 0 := sorry
```
:::

::: {.numex arguments="5"}
```lean
--Hint: Use mathematical induction.
theorem Exercise_8_1_6a : ∀ ⦃m n : Nat⦄, (I m ∼ I n) → m = n := sorry
```
:::

::: {.numex arguments="6"}
```lean
theorem Exercise_8_1_6b {U : Type} {A : Set U} {m n : Nat}
    (h1 : numElts A m) (h2 : numElts A n) : m = n := sorry
```
:::

::: {.numex arguments="7"}
```lean
lemma neb_nrpb (m : Nat) : ∀ ⦃k : Nat⦄, k ≤ m →
    num_elts_below (set_rp_below m) k = num_rp_below m k := sorry
```
:::

::: {.numex arguments="8"}
```lean
--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
```
:::

::: {.mdsk}
:::

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:

```lean
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

::: {.numex arguments="9"}
```lean
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
```
:::

::: {.numex arguments="10"}
```lean
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
```
:::

::: {.numex arguments="11"}
```lean
--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
```
:::

::: {.numex arguments="12"}
```lean
lemma shift_I_equinum (n m : Nat) : I m ∼ ↑(I (n + m) \ I n) := sorry
```
:::

::: {.numex arguments="13"}
```lean
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
```
:::

::: {.numex arguments="14"}
```lean
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
```
:::

::: {.numex arguments="15"}
```lean
theorem Exercise_8_1_8b {U : Type} {A B : Set U}
    (h1 : finite A) (h2 : B ⊆ A) : finite B := sorry
```
:::

::: {.numex arguments="16"}
```lean
theorem finite_bdd {A : Set Nat} (h : finite A) :
    ∃ (m : Nat), ∀ n ∈ A, n < m := sorry
```
:::

::: {.numex arguments="17"}
```lean
lemma N_not_finite : ¬finite Nat := sorry
```
:::

::: {.numex arguments="18"}
```lean
theorem denum_not_finite (U : Type)
    (h : denum U) : ¬finite U := sorry
```
:::

::: {.numex arguments="19"}
```lean
--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.

```lean
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:

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

```lean
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 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>.]

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

```lean
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.

```lean
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.

```lean
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.

```lean
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`.

```lean
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.

```lean
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)`.

```lean
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.

```lean
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`.

```lean
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`.

```lean
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`.

```lean
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.

```lean
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

::: {.numex arguments="1"}
```lean
lemma pair_ctble {U : Type}
    (a b : U) : ctble ↑({a, b} : Set U) := sorry
```
:::

::: {.numex arguments="2"}
```lean
--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
```
:::

::: {.numex arguments="3"}
```lean
lemma remove_empty_union_eq {U : Type} (F : Set (Set U)) :
    ⋃₀ {A : Set U | A ∈ F ∧ ¬empty A} = ⋃₀ F := sorry
```
:::

::: {.numex arguments="4"}
```lean
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
```
:::

::: {.numex arguments="5"}
```lean
--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
```
:::

::: {.numex arguments="6"}
```lean
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
```
:::

::: {.numex arguments="7"}
```lean
--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
```
:::

::: {.numex arguments="8"}
```lean
theorem Exercise_8_2_6b (U V W : Type) :
     ((U × V) → W) ∼ (U → V → W) := sorry
```
:::

::: {.numex arguments="9"}
```lean
theorem Like_Exercise_8_2_7 : ∃ (P : Set (Set Nat)),
    partition P ∧ denum P ∧ ∀ X ∈ P, denum X := sorry
```
:::

::: {.numex arguments="10"}
```lean
theorem unctbly_many_inf_set_nat :
    ¬ctble {X : Set Nat | ¬finite X} := sorry
```
:::

::: {.numex arguments="11"}
```lean
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.

```lean
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:

```lean
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.

```lean
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`:

```lean
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.

```lean
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

::: {.numex arguments="1"}
```lean
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
```
:::

::: {.numex arguments="2"}
```lean
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).  
```lean
theorem relext {U V : Type} {R S : Rel U V}
    (h : ∀ (u : U) (v : V), R u v ↔ S u v) : R = S := sorry
```

::: {.mdsk}
:::

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:

```lean
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}
```

::: {.numex arguments="4"}
```lean
theorem EqRel_equinum_Part (U : Type) : EqRel U ∼ Part U := sorry
```
:::

::: {.numex arguments="5"}
```lean
theorem EqRel_equinum_EqRelExt (U : Type) :
    EqRel U ∼ EqRelExt U := sorry
```
:::

::: {.numex arguments="6"}
```lean
theorem EqRel_Nat_to_Set_Nat :
    ∃ (f : EqRel Nat → Set Nat), one_to_one f := sorry
```
:::

::: {.numex arguments="7"}
```lean
theorem saz_pair_part (X : Set Nat) : saz_pair X ∈ Part Nat := sorry
```
:::

::: {.numex arguments="8"}
```lean
theorem Set_Nat_to_EqRel_Nat :
    ∃ (f : Set Nat → EqRel Nat), one_to_one f := sorry
```
:::

::: {.numex arguments="9"}
```lean
theorem EqRel_Nat_equinum_Set_Nat : EqRel Nat ∼ Set Nat := sorry
```
:::