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.  As we will see, in Lean we will need to phrase this definition somewhat differently.  However, we begin by considering some examples of functions that are one-to-one and onto.

The first example in *HTPI* is a one-to-one, onto function from $\mathbb{Z}^+$ to $\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 : fnz (2 * k) = if 2 ∣ 2 * k then ↑(2 * k / 2)
    else -↑((2 * k + 1) / 2) := by rfl
  rewrite [if_pos h1] at h2  --h2 : fnz (2 * k) = ↑(2 * k / 2)
  have h3 : 0 < 2 := by linarith
  rewrite [Nat.mul_div_cancel_left k h3] at h2
  show fnz (2 * k) = ↑k from 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'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)]
  --Answer: [0, 1, 2, 3, 4]
```

Two simple lemmas about `tri` will 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
```

Despite these successes with one-to-one, onto functions, we will use a definition of "equinumerous" in Lean that is different from the definition in *HTPI*.  There are two reasons for this change.  First of all, the domain of a function in Lean must be a *type*, but we want to be able to talk about *sets* being equinumerous.  Secondly, Lean expects functions to be *computable*; it regards the definition of a function as an algorithm for computing the value of the function on any input.  This restriction would cause problems with some of our proofs.  While there are ways to overcome these difficulties, they would introduce complications that we can avoid by using a different approach.

Suppose `U` and `V` are types, and we have sets `A : Set U` and `B : Set V`.  We will define `A` to be equinumerous with `B` if there is a relation `R` from `U` to `V` that defines a one-to-one correspondence between the elements of `A` and `B`.  To formulate this precisely, suppose that `R` has type `Rel U V`.  We will place three requirements on `R`.  First, we require that the relation `R` should hold only between elements of `A` and `B`.  We say in this case that `R` is a *relation within `A` and `B`*:

```lean
def rel_within {U V : Type} (R : Rel U V) (A : Set U) (B : Set V) : Prop :=
  ∀ ⦃x : U⦄ ⦃y : V⦄, R x y → x ∈ A ∧ y ∈ B
```

Notice that in this definition, we have used the same double braces for the quantified variables `x` and `y` that were used in the definition of "subset."  This means that `x` and `y` are implicit arguments, and therefore if we have `h1 : rel_within R A B` and `h2 : R a b`, then `h1 h2` is a proof of `a ∈ A ∧ b ∈ B`.  There is no need to specify that `a` and `b` are the values to be assigned to `x` and `y`; 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.)

Next, we require that every element of `A` is related by `R` to exactly one thing.  We say in this case that `R` is *functional on `A`*:

```lean
def fcnl_on {U V : Type} (R : Rel U V) (A : Set U) : Prop :=
  ∀ ⦃x : U⦄, x ∈ A → ∃! (y : V), R x y
```

Finally, we impose the same requirement in the other direction: for every element of `B`, exactly one thing should be related to it by `R`.  We can express this by saying that the inverse of `R` is functional on `B`.  In Chapter 4, we defined the inverse of a set of ordered pairs, but we can easily convert this to an operation on relations:

```lean
def invRel {U V : Type} (R : Rel U V) : Rel V U :=
  RelFromExt (inv (extension R))

lemma invRel_def {U V : Type} (R : Rel U V) (u : U) (v : V) :
    invRel R v u ↔ R u v := by rfl
```

We will call `R` a *matching from `A` to `B`* if it meets the three requirements above:

```lean
def matching {U V : Type} (R : Rel U V) (A : Set U) (B : Set V) : Prop :=
  rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
```

Finally, we say that *`A` is equinumerous with `B`* if there is a matching from `A` to `B`, and, as in *HTPI* we introduce the notation `A ∼ B` to indicate that `A` is equinumerous with `B` (to enter the symbol `∼`, type `\sim` or `\~`).

```lean
def equinum {U V : Type} (A : Set U) (B : Set V) : Prop :=
  ∃ (R : Rel U V), matching R A B

notation:50  A:50 " ∼ " B:50 => equinum A B
```

Can the examples at the beginning of this section be used to establish that `Int ∼ Nat` and `Nat × Nat ∼ Nat`?  Not quite, because `Int`, `Nat`, and `Nat × Nat` are types, not sets.  We must talk about the sets of all objects of those types, not the types themselves, so we introduce another definition.

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

lemma elt_Univ {U : Type} (u : U) :
    u ∈ Univ U := by trivial
```

For any type `U`, `Univ U` is the set of all objects of type `U`; we might call it the *universal set* for the type `U`.  Now we can use the functions defined earlier to prove that `Univ Int ∼ Univ Nat` and `Univ (Nat × Nat) ∼ Univ Nat`.  The do this, we must convert the functions into relations and prove that those relations are matchings.  The conversion can be done with the following function.

```lean
def RelWithinFromFunc {U V : Type} (f : U → V) (A : Set U)
  (x : U) (y : V) : Prop := x ∈ A ∧ f x = y
```

This definition says that if we have `f : U → V` and `A : Set U`, then `RelWithinFromFunc f A` is a relation from `U` to `V` that relates any `x` that is an element of `A` to `f x`.

We will say that a function is one-to-one on a set `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
```

With all of this preparation, we can now prove that if `f` is one-to-one on `A`, then `A` is equinumerous with its image under `f`.

```lean
theorem equinum_image {U V : Type} {A : Set U} {B : Set V} {f : U → V}
    (h1 : one_one_on f A) (h2 : image f A = B) : A ∼ B := by
  rewrite [←h2]
  define   --Goal : ∃ (R : Rel U V), matching R A (image f A)
  set R : Rel U V := RelWithinFromFunc f A
  apply Exists.intro R
  define   --Goal : rel_within R A (image f A) ∧
           --fcnl_on R A ∧ fcnl_on (invRel R) (image f A)
  apply And.intro
  · -- Proof of rel_within
    define --Goal : ∀ ⦃x : U⦄ ⦃y : V⦄, R x y → x ∈ A ∧ y ∈ image f A
    fix x : U; fix y : V
    assume h3 : R x y  --Goal : x ∈ A ∧ y ∈ image f A
    define at h3       --h3 : x ∈ A ∧ f x = y
    apply And.intro h3.left
    define
    show ∃ x ∈ A, f x = y from Exists.intro x h3
    done
  · -- Proofs of fcnl_ons
    apply And.intro
    · -- Proof of fcnl_on R A
      define  --Goal : ∀ ⦃x : U⦄, x ∈ A → ∃! (y : V), R x y
      fix x : U
      assume h3 : x ∈ A
      exists_unique
      · -- Existence
        apply Exists.intro (f x)
        define  --Goal : x ∈ A ∧ f x = f x
        apply And.intro h3
        rfl
        done
      · -- Uniqueness
        fix y1 : V; fix y2 : V
        assume h4 : R x y1
        assume h5 : R x y2   --Goal : y1 = y2
        define at h4; define at h5
          --h4 : x ∈ A ∧ f x = y1;  h5 : x ∈ A ∧ f x = y2
        rewrite [h4.right] at h5
        show y1 = y2 from h5.right
        done
      done
    · -- Proof of fcnl_on (invRel R) (image f A)
      define  --Goal : ∀ ⦃x : V⦄, x ∈ image f A → ∃! (y : U), invRel R x y
      fix y : V
      assume h3 : y ∈ image f A
      obtain (x : U) (h4 : x ∈ A ∧ f x = y) from h3
      exists_unique
      · -- Existence
        apply Exists.intro x
        define
        show x ∈ A ∧ f x = y from h4
        done
      · -- Uniqueness
        fix x1 : U; fix x2 : U
        assume h5 : invRel R y x1
        assume h6 : invRel R y x2
        define at h5; define at h6
          --h5 : x1 ∈ A ∧ f x1 = y;  h6 : x2 ∈ A ∧ f x2 = y
        rewrite [←h6.right] at h5
        show x1 = x2 from h1 h5.left h6.left h5.right
        done
      done
    done
  done
```

To apply this result to the functions introduced at the beginning of this section, we will want to use `Univ U` for the set `A` in the theorem `equinum_image`:

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

theorem equinum_Univ {U V : Type} {f : U → V}
    (h1 : one_to_one f) (h2 : onto f) : Univ U ∼ Univ V := by
  have h3 : image f (Univ U) = Univ V := by
    apply Set.ext
    fix v : V
    apply Iff.intro
    · -- (→)
      assume h3 : v ∈ image f (Univ U)
      show v ∈ Univ V from elt_Univ v
      done
    · -- (←)
      assume h3 : v ∈ Univ V
      obtain (u : U) (h4 : f u = v) from h2 v
      apply Exists.intro u
      apply And.intro _ h4
      show u ∈ Univ U from elt_Univ u
      done
    done
  show Univ U ∼ Univ V from
    equinum_image (one_one_on_of_one_one h1 (Univ U)) h3
  done

theorem Z_equinum_N : Univ Int ∼ Univ Nat :=
  equinum_Univ fzn_one_one fzn_onto

theorem NxN_equinum_N : Univ (Nat × Nat) ∼ Univ Nat :=
  equinum_Univ fnnn_one_one fnnn_onto
```

Theorem 8.1.3 in *HTPI* shows 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.

```lean
lemma id_one_one_on {U : Type} (A : Set U) : one_one_on id A := sorry

lemma image_id {U : Type} (A : Set U) : image id A = A := sorry

theorem Theorem_8_1_3_1 {U : Type} (A : Set U) : A ∼ A :=
  equinum_image (id_one_one_on A) (image_id A)
```

For symmetry, we show that the inverse of a matching is also a matching.

```lean
lemma inv_inv {U V : Type} (R : Rel U V) : invRel (invRel R) = R := by rfl

lemma inv_match {U V : Type} {R : Rel U V} {A : Set U} {B : Set V}
    (h : matching R A B) : matching (invRel R) B A := by
  define       --Goal : rel_within (invRel R) B A ∧
               --fcnl_on (invRel R) B ∧ fcnl_on (invRel (invRel R)) A
  define at h  --h : rel_within R A B ∧ fcnl_on R A ∧ fcnl_on (invRel R) B
  apply And.intro
  · -- Proof that rel_within (invRel R) B A
    define     --Goal : ∀ ⦃x : V⦄ ⦃y : U⦄, invRel R x y → x ∈ B ∧ y ∈ A
    fix y : V; fix x : U
    assume h1 : invRel R y x
    define at h1  --h1 : R x y
    have h2 : x ∈ A ∧ y ∈ B := h.left h1
    show y ∈ B ∧ x ∈ A from And.intro h2.right h2.left
    done
  · -- proof that fcnl_on (inv R) B ∧ fcnl_on (inv (inv R)) A
    rewrite [inv_inv]
    show fcnl_on (invRel R) B ∧ fcnl_on R A from
      And.intro h.right.right h.right.left
    done
  done

theorem Theorem_8_1_3_2 {U V : Type} {A : Set U} {B : Set V}
    (h : A ∼ B) : B ∼ A := by
  obtain (R : Rel U V) (h1 : matching R A B) from h
  apply Exists.intro (invRel R)
  show matching (invRel R) B A from inv_match h1
  done
```

The proof of transitivity is a bit more involved.  In this proof, as well as some later proofs, we find it useful to separate out the existence and uniqueness parts of the definition of `fcnl_on`:

```lean
lemma fcnl_exists {U V : Type} {R : Rel U V} {A : Set U} {x : U}
    (h1 : fcnl_on R A) (h2 : x ∈ A) : ∃ (y : V), R x y := by
  define at h1
  obtain (y : V) (h3 : R x y)
    (h4 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2) from h1 h2
  show ∃ (y : V), R x y from Exists.intro y h3
  done

lemma fcnl_unique {U V : Type}
    {R : Rel U V} {A : Set U} {x : U} {y1 y2 : V} (h1 : fcnl_on R A)
    (h2 : x ∈ A) (h3 : R x y1) (h4 : R x y2) : y1 = y2 := by
  define at h1
  obtain (z : V) (h5 : R x z)
    (h6 : ∀ (y_1 y_2 : V), R x y_1 → R x y_2 → y_1 = y_2) from h1 h2
  show y1 = y2 from h6 y1 y2 h3 h4
  done
```

To prove transitivity, we will show that a composition of matchings is a matching.  Once again we must convert our definition of composition of sets of ordered pairs into an operation on relations.  A few preliminary lemmas help with the proof.

```lean
def compRel {U V W : Type} (S : Rel V W) (R : Rel U V) : Rel U W :=
  RelFromExt (comp (extension S) (extension R))

lemma compRel_def {U V W : Type}
    (S : Rel V W) (R : Rel U V) (u : U) (w : W) :
    compRel S R u w ↔ ∃ (x : V), R u x ∧ S x w := by rfl

lemma inv_comp {U V W : Type} (R : Rel U V) (S : Rel V W) :
    invRel (compRel S R) = compRel (invRel R) (invRel S) := 
  calc invRel (compRel S R)
    _ = RelFromExt (inv (comp (extension S) (extension R))) := by rfl
    _ = RelFromExt (comp (inv (extension R)) (inv (extension S))) := by
          rw [Theorem_4_2_5_5]
    _ = compRel (invRel R) (invRel S) := by rfl

lemma comp_fcnl {U V W : Type} {R : Rel U V} {S : Rel V W}
    {A : Set U} {B : Set V} {C : Set W} (h1 : matching R A B)
    (h2 : matching S B C) : fcnl_on (compRel S R) A := by
  define; define at h1; define at h2
  fix a : U
  assume h3 : a ∈ A
  obtain (b : V) (h4 : R a b) from fcnl_exists h1.right.left h3
  have h5 : a ∈ A ∧ b ∈ B := h1.left h4
  obtain (c : W) (h6 : S b c) from fcnl_exists h2.right.left h5.right
  exists_unique
  · -- Existence
    apply Exists.intro c
    rewrite [compRel_def]
    show ∃ (x : V), R a x ∧ S x c from Exists.intro b (And.intro h4 h6)
    done
  · -- Uniqueness
    fix c1 : W; fix c2 : W
    assume h7 : compRel S R a c1
    assume h8 : compRel S R a c2    --Goal : c1 = c2
    rewrite [compRel_def] at h7
    rewrite [compRel_def] at h8
    obtain (b1 : V) (h9 : R a b1 ∧ S b1 c1) from h7
    obtain (b2 : V) (h10 : R a b2 ∧ S b2 c2) from h8
    have h11 : b1 = b := fcnl_unique h1.right.left h3 h9.left h4
    have h12 : b2 = b := fcnl_unique h1.right.left h3 h10.left h4
    rewrite [h11] at h9
    rewrite [h12] at h10
    show c1 = c2 from
      fcnl_unique h2.right.left h5.right h9.right h10.right
    done
  done

lemma comp_match {U V W : Type} {R : Rel U V} {S : Rel V W}
    {A : Set U} {B : Set V} {C : Set W} (h1 : matching R A B)
    (h2 : matching S B C) : matching (compRel S R) A C := by
  define
  apply And.intro
  · -- Proof of rel_within (compRel S R) A C
    define
    fix a : U; fix c : W
    assume h3 : compRel S R a c
    rewrite [compRel_def] at h3
    obtain (b : V) (h4 : R a b ∧ S b c) from h3
    have h5 : a ∈ A ∧ b ∈ B := h1.left h4.left
    have h6 : b ∈ B ∧ c ∈ C := h2.left h4.right
    show a ∈ A ∧ c ∈ C from And.intro h5.left h6.right
    done
  · -- Proof of fcnl_on statements
    apply And.intro
    · -- Proof of fcnl_on (compRel S R) A
      show fcnl_on (compRel S R) A from comp_fcnl h1 h2
      done
    · -- Proof of fcnl_on (invRel (compRel S R)) Z
      rewrite [inv_comp]
      have h3 : matching (invRel R) B A := inv_match h1
      have h4 : matching (invRel S) C B := inv_match h2
      show fcnl_on (compRel (invRel R) (invRel S)) C from comp_fcnl h4 h3
      done
    done
  done

theorem Theorem_8_1_3_3 {U V W : Type} {A : Set U} {B : Set V} {C : Set W}
    (h1 : A ∼ B) (h2 : B ∼ C) : A ∼ C := by
  obtain (R : Rel U V) (h3 : matching R A B) from h1
  obtain (S : Rel V W) (h4 : matching S B C) from h2
  apply Exists.intro (compRel S R)
  show matching (compRel S R) A C from comp_match h3 h4
  done
```

Now that we have a basic understanding of the concept of equinumerous sets, we can use this concept 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} (A : Set U) : Prop :=
  ∃ (n : Nat), I n ∼ A

def denum {U : Type} (A : Set U) : Prop :=
  Univ Nat ∼ A

lemma denum_def {U : Type} (A : Set U) : denum A ↔ Univ Nat ∼ A := by rfl

def ctble {U : Type} (A : Set U) : Prop :=
  finite A ∨ denum A
```

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 relation `enum A` that "enumerates" the elements of `A` by relating `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 related to any element `n` of `A`?  Notice that if `n` is the smallest element of `A`, then there are `0` elements of `A` that are smaller than `n`; if it is second smallest element of `A`, then there is `1` element of `A` that is smaller than `n`; and so on.  Thus, `enum A` should relate a natural number `s` to `n` if and only if the number of elements of `A` that are smaller than `n` is `s`.  This suggests a plan:  First we define a proposition `num_elts_below A n s` saying that the number of elements of `A` that are smaller than `n` is `s`.  Then we use this proposition to define the relation `enum A`, and finally we show that `enum A` is a matching that can be used to prove that `A` is countable.

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 s : Nat) : Prop :=
  match m with
    | 0 => s = 0
    | n + 1 => (n ∈ A ∧ 1 ≤ s ∧ num_elts_below A n (s - 1)) ∨
                (n ∉ A ∧ num_elts_below A n s)

def enum (A : Set Nat) (s n : Nat) : Prop := n ∈ A ∧ num_elts_below A n s
```

The details of the proof that `enum A` is the required matching are long.  We'll skip them here, but you can find them in the HTPI Lean package.

```lean
lemma neb_exists (A : Set Nat) :
    ∀ (n : Nat), ∃ (s : Nat), num_elts_below A n s := sorry

lemma bdd_subset_nat_match {A : Set Nat} {m s : Nat}
    (h1 : ∀ n ∈ A, n < m) (h2 : num_elts_below A m s) :
    matching (enum A) (I s) A := sorry

lemma bdd_subset_nat {A : Set Nat} {m s : Nat}
    (h1 : ∀ n ∈ A, n < m) (h2 : num_elts_below A m s) :
    I s ∼ A := Exists.intro (enum A) (bdd_subset_nat_match h1 h2)

lemma unbdd_subset_nat_match {A : Set Nat}
    (h1 : ∀ (m : Nat), ∃ n ∈ A, n ≥ m) :
    matching (enum A) (Univ Nat) A := sorry

lemma unbdd_subset_nat {A : Set Nat}
    (h1 : ∀ (m : Nat), ∃ n ∈ A, n ≥ m) :
    denum A := Exists.intro (enum A) (unbdd_subset_nat_match h1)

lemma subset_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
    obtain (s : Nat) (h3 : num_elts_below A m s) from neb_exists A m
    apply Exists.intro s
    show I s ∼ A from bdd_subset_nat h2 h3
    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 lemma, we get another characterization of countable sets: a set is countable if and only if it is equinumerous with some subset of the natural numbers:

```lean
lemma ctble_of_equinum_ctble {U V : Type} {A : Set U} {B : Set V}
    (h1 : A ∼ B) (h2 : ctble A) : ctble B := sorry

lemma ctble_iff_equinum_set_nat {U : Type} (A : Set U) : 
    ctble A ↔ ∃ (I : Set Nat), I ∼ A := by
  apply Iff.intro
  · -- (→)
    assume h1 : ctble A
    define at h1  --h1 : finite A ∨ denum A
    by_cases on h1
    · -- Case 1. h1 : finite A
      define at h1  --h1 : ∃ (n : Nat), I n ∼ A
      obtain (n : Nat) (h2 : I n ∼ A) from h1
      show ∃ (I : Set Nat), I ∼ A from Exists.intro (I n) h2
      done
    · -- Case 2. h1 : denum A
      rewrite [denum_def] at h1  --h1 : Univ Nat ∼ A
      show ∃ (I : Set Nat), I ∼ A from Exists.intro (Univ Nat) h1
      done
    done
  · -- (←)
    assume h1 : ∃ (I : Set Nat), I ∼ A
    obtain (I : Set Nat) (h2 : I ∼ A) from h1
    have h3 : ctble I := subset_nat_ctble I
    show ctble A from ctble_of_equinum_ctble h2 h3
    done
  done
```

We are now ready to turn to Theorem 8.1.5 in *HTPI*.  The theorem gives two statements that are equivalent to the countability of a set $A$.  The first involves a function from the natural numbers to $A$ that is onto.  In keeping with our approach in this section, we state a similar characterization involving a relation rather than a function.

```lean
def unique_val_on_N {U : Type} (R : Rel Nat U) : Prop :=
  ∀ ⦃n : Nat⦄ ⦃x1 x2 : U⦄, R n x1 → R n x2 → x1 = x2

def nat_rel_onto {U : Type} (R : Rel Nat U) (A : Set U) : Prop :=
  ∀ ⦃x : U⦄, x ∈ A → ∃ (n : Nat), R n x

def fcnl_onto_from_nat {U : Type} (R : Rel Nat U) (A : Set U) : Prop :=
  unique_val_on_N R ∧ nat_rel_onto R A
```

Intuitively, you might think of `fcnl_onto_from_nat R A` as meaning that the relation `R` defines a function whose domain is a subset of the natural numbers and whose range contains `A`.

The second characterization of the countability of $A$ in Theorem 8.1.5 involves a function from $A$ to the natural numbers that is one-to-one.  Once again, we rephrase this in terms of relations.  We define `fcnl_one_one_to_nat R A` to mean that `R` defines a function from `A` to the natural numbers that is one-to-one:

```lean
def fcnl_one_one_to_nat {U : Type} (R : Rel U Nat) (A : Set U) : Prop :=
  fcnl_on R A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : Nat⦄,
    (x1 ∈ A ∧ R x1 n) → (x2 ∈ A ∧ R x2 n) → x1 = x2
```

Our plan is to prove that if `A` has type `Set U` then the following statements are equivalent:

1.  `ctble A`
2.  `∃ (R : Rel Nat U), fcnl_onto_from_nat R A`
3.  `∃ (R : Rel U Nat), fcnl_one_one_to_nat R 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} (h1 : ctble A) :
    ∃ (R : Rel Nat U), fcnl_onto_from_nat R A := by
  rewrite [ctble_iff_equinum_set_nat] at h1
  obtain (I : Set Nat) (h2 : I ∼ A) from h1
  obtain (R : Rel Nat U) (h3 : matching R I A) from h2
  define at h3
    --h3 : rel_within R I A ∧ fcnl_on R I ∧ fcnl_on (invRel R) A
  apply Exists.intro R
  define  --Goal : unique_val_on_N R ∧ nat_rel_onto R A
  apply And.intro
  · -- Proof of unique_val_on_N R
    define
    fix n : Nat; fix x1 : U; fix x2 : U
    assume h4 : R n x1
    assume h5 : R n x2      --Goal : x1 = x2
    have h6 : n ∈ I ∧ x1 ∈ A := h3.left h4
    show x1 = x2 from fcnl_unique h3.right.left h6.left h4 h5
    done
  · -- Proof of nat_rel_onto R A
    define
    fix x : U
    assume h4 : x ∈ A  --Goal : ∃ (n : Nat), R n x
    show ∃ (n : Nat), R n x from fcnl_exists h3.right.right h4
    done
  done
```

For the proof of 2 → 3, suppose we have `A : Set U` and `S : Rel Nat U`, and the statement `fcnl_onto_from_nat S A` is true.  We need to come up with a relation `R : Rel U Nat` for which we can prove `fcnl_one_one_to_nat R A`.  You might be tempted to try `R = invRel S`, but there is a problem with this choice:  if `x ∈ A`, there might be multiple natural numbers `n` such that `S n x` holds, but we must make sure that there is only one `n` for which `R x n` holds.  Our solution to this problem will be to define `R x n` to mean that `n` is the smallest natural number for which `S n x` holds.  (The proof in *HTPI* uses a similar idea.)  The well-ordering principle guarantees that there always is such a smallest element.

```lean
def least_rel_to {U : Type} (S : Rel Nat U) (x : U) (n : Nat) : Prop :=
  S n x ∧ ∀ (m : Nat), S m x → n ≤ m

lemma exists_least_rel_to {U : Type} {S : Rel Nat U} {x : U}
    (h1 : ∃ (n : Nat), S n x) : ∃ (n : Nat), least_rel_to S x n := by
  set W : Set Nat := {n : Nat | S n x}
  have h2 : ∃ (n : Nat), n ∈ W := h1
  show ∃ (n : Nat), least_rel_to S x n from well_ord_princ W h2
  done

theorem Theorem_8_1_5_2_to_3 {U : Type} {A : Set U}
    (h1 : ∃ (R : Rel Nat U), fcnl_onto_from_nat R A) :
    ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A := by
  obtain (S : Rel Nat U) (h2 : fcnl_onto_from_nat S A) from h1
  define at h2  --h2 : unique_val_on_N S ∧ nat_rel_onto S A
  set R : Rel U Nat := least_rel_to S
  apply Exists.intro R
  define
  apply And.intro
  · -- Proof of fcnl_on R A
    define
    fix x : U
    assume h4 : x ∈ A  --Goal : ∃! (y : Nat), R x y
    exists_unique
    · -- Existence
      have h5 : ∃ (n : Nat), S n x := h2.right h4
      show ∃ (n : Nat), R x n from exists_least_rel_to h5
      done
    · -- Uniqueness
      fix n1 : Nat; fix n2 : Nat
      assume h5 : R x n1
      assume h6 : R x n2      --Goal : n1 = n2
      define at h5    --h5 : S n1 x ∧ ∀ (m : Nat), S m x → n1 ≤ m
      define at h6    --h6 : S n2 x ∧ ∀ (m : Nat), S m x → n2 ≤ m
      have h7 : n1 ≤ n2 := h5.right n2 h6.left
      have h8 : n2 ≤ n1 := h6.right n1 h5.left
      linarith
      done
    done
  · -- Proof of one-to-one
    fix x1 : U; fix x2 : U; fix n : Nat
    assume h4 : x1 ∈ A ∧ R x1 n
    assume h5 : x2 ∈ A ∧ R x2 n
    have h6 : R x1 n := h4.right
    have h7 : R x2 n := h5.right
    define at h6   --h6 : S n x1 ∧ ∀ (m : Nat), S m x1 → n ≤ m
    define at h7   --h7 : S n x2 ∧ ∀ (m : Nat), S m x2 → n ≤ m
    show x1 = x2 from h2.left h6.left h7.left
    done
  done
```

Finally, for the proof of 3 → 1, suppose we have `A : Set U`, `S : Rel U Nat`, and `fcnl_one_one_to_nat S A` holds.  Our plan is to restrict `S` to elements of `A` and then show that the inverse of the resulting relation is a matching from some set of natural numbers to `A`.  By `ctble_iff_equinum_set_nat`, this implies that `A` is countable.

```lean
def restrict_to {U V : Type} (S : Rel U V) (A : Set U)
  (x : U) (y : V) : Prop := x ∈ A ∧ S x y

theorem Theorem_8_1_5_3_to_1 {U : Type} {A : Set U}
    (h1 : ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A) :
    ctble A := by
  obtain (S : Rel U Nat) (h2 : fcnl_one_one_to_nat S A) from h1
  define at h2  --h2 : fcnl_on S A ∧ ∀ ⦃x1 x2 : U⦄ ⦃n : Nat⦄,
                --x1 ∈ A ∧ S x1 n → x2 ∈ A ∧ S x2 n → x1 = x2
  rewrite [ctble_iff_equinum_set_nat]  --Goal : ∃ (I : Set Nat), I ∼ A
  set R : Rel Nat U := invRel (restrict_to S A)
  set I : Set Nat := {n : Nat | ∃ (x : U), R n x}
  apply Exists.intro I
  define        --Goal : ∃ (R : Rel Nat U), matching R I A
  apply Exists.intro R
  define
  apply And.intro
  · -- Proof of rel_within R I A
    define
    fix n : Nat; fix x : U
    assume h3 : R n x   --Goal : n ∈ I ∧ x ∈ A
    apply And.intro
    · -- Proof that n ∈ I
      define            --Goal : ∃ (x : U), R n x
      show ∃ (x : U), R n x from Exists.intro x h3
      done
    · -- Proof that x ∈ A
      define at h3      --h3 : x ∈ A ∧ S x n
      show x ∈ A from h3.left
      done
    done
  · -- Proofs of fcnl_ons
    apply And.intro
    · -- Proof of fcnl_on R I
      define
      fix n : Nat
      assume h3 : n ∈ I   --Goal : ∃! (y : U), R n y
      exists_unique
      · -- Existence
        define at h3      --h3 : ∃ (x : U), R n x
        show ∃ (y : U), R n y from h3
        done
      · -- Uniqueness
        fix x1 : U; fix x2 : U
        assume h4 : R n x1
        assume h5 : R n x2
        define at h4      --h4 : x1 ∈ A ∧ S x1 n; 
        define at h5      --h5 : x2 ∈ A ∧ S x2 n
        show x1 = x2 from h2.right h4 h5
        done
      done
    · -- Proof of fcnl_on (invRel R) A
      define
      fix x : U
      assume h3 : x ∈ A  --Goal : ∃! (y : Nat), invRel R x y
      exists_unique
      · -- Existence
        obtain (y : Nat) (h4 : S x y) from fcnl_exists h2.left h3
        apply Exists.intro y
        define
        show x ∈ A ∧ S x y from And.intro h3 h4
        done
      · -- Uniqueness
        fix n1 : Nat; fix n2 : Nat
        assume h4 : invRel R x n1
        assume h5 : invRel R x n2  --Goal : n1 = n2
        define at h4     --h4 : x ∈ A ∧ S x n1
        define at h5     --h5 : x ∈ A ∧ S x n2
        show n1 = n2 from fcnl_unique h2.left h3 h4.right h5.right
        done
      done
    done
  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 ↔ ∃ (R : Rel Nat U), fcnl_onto_from_nat R A := by
  apply Iff.intro
  · -- (→)
    assume h1 : ctble A
    show ∃ (R : Rel Nat U), fcnl_onto_from_nat R A from
      Theorem_8_1_5_1_to_2 h1
    done
  · -- (←)
    assume h1 : ∃ (R : Rel Nat U), fcnl_onto_from_nat R A
    have h2 : ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A :=
      Theorem_8_1_5_2_to_3 h1
    show ctble A from Theorem_8_1_5_3_to_1 h2
    done
  done

theorem Theorem_8_1_5_3 {U : Type} (A : Set U) :
    ctble A ↔ ∃ (R : Rel U Nat), fcnl_one_one_to_nat R A := sorry
```

In the exercises, we ask you to show that countability of a set can be proven using functions of the kind considered in Theorem 8.1.5 of *HTPI*.

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

```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 image_fqn_unbdd :
    ∀ (m : Nat), ∃ n ∈ image fqn (Univ Rat), n ≥ m := by
  fix m : Nat
  set n : Nat := fqn ↑m
  apply Exists.intro n
  apply And.intro
  · -- Proof that n ∈ image fqn (Univ Rat)
    define
    apply Exists.intro ↑m
    apply And.intro (elt_Univ (↑m : Rat))
    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 (Univ Rat) := by
  set I : Set Nat := image fqn (Univ Rat)
  have h1 : Univ Nat ∼ I := unbdd_subset_nat image_fqn_unbdd
  have h2 : image fqn (Univ Rat) = I := by rfl
  have h3 : Univ Rat ∼ I :=
    equinum_image (one_one_on_of_one_one fqn_one_one (Univ Rat)) h2
  have h4 : I ∼ Univ Rat := Theorem_8_1_3_2 h3
  show denum (Univ Rat) from Theorem_8_1_3_3 h1 h4
  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
lemma ctble_of_equinum_ctble {U V : Type} {A : Set U} {B : Set V}
    (h1 : A ∼ B) (h2 : ctble A) : ctble B := sorry
```
:::

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

::: {.mdsk}
:::

The next four exercises use the following definition:

```lean
def Rel_image {U V : Type} (R : Rel U V) (A : Set U) : Set V :=
  {y : V | ∃ x ∈ A, R x y}
```

Note that if `R` has type `Rel U V`, then `Rel_image R` has type `Set U → Set V`.

::: {.numex arguments="7"}
```lean
lemma Rel_image_on_power_set {U V : Type} {R : Rel U V}
    {A C : Set U} {B : Set V} (h1 : matching R A B) (h2 : C ∈ 𝒫 A) :
    Rel_image R C ∈ 𝒫 B := sorry
```
:::

::: {.numex arguments="8"}
```lean
lemma Rel_image_inv {U V : Type} {R : Rel U V}
    {A C : Set U} {B : Set V} (h1 : matching R A B) (h2 : C ∈ 𝒫 A) :
    Rel_image (invRel R) (Rel_image R C) = C := sorry
```
:::

::: {.numex arguments="9"}
```lean
lemma Rel_image_one_one_on {U V : Type} {R : Rel U V}
    {A : Set U} {B : Set V} (h1 : matching R A B) :
    one_one_on (Rel_image R) (𝒫 A) := sorry
```
:::

::: {.numex arguments="10"}
```lean
lemma Rel_image_image {U V : Type} {R : Rel U V}
    {A : Set U} {B : Set V} (h1 : matching R A B) :
    image (Rel_image R) (𝒫 A) = 𝒫 B := sorry
```
:::

::: {.numex arguments="11"}
```lean
--Hint:  Use the previous two exercises.
theorem Exercise_8_1_5 {U V : Type} {A : Set U} {B : Set V}
    (h1 : A ∼ B) : 𝒫 A ∼ 𝒫 B := sorry
```
:::

::: {.numex arguments="12"}
```lean
theorem Exercise_8_1_17 {U : Type} {A B : Set U}
    (h1 : B ⊆ A) (h2 : ctble A) : ctble B := sorry
```
:::

::: {.numex arguments="13"}
```lean
theorem ctble_of_onto_func_from_N {U : Type} {A : Set U} {f : Nat → U}
    (h1 : ∀ x ∈ A, ∃ (n : Nat), f n = x) : ctble A := sorry
```
:::

::: {.numex arguments="14"}
```lean
theorem ctble_of_one_one_func_to_N {U : Type} {A : Set U} {f : U → Nat}
    (h1 : one_one_on f A) : ctble A := 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 begin with the fact that a set has zero elements if and only if it is empty.  To prove this, we will need to produce a relation that is a matching between two sets if the sets are empty.  The natural choice for this relation is what we will call the empty relation---the relation that is always false.

```lean
def emptyRel (U V : Type) (x : U) (y : V) : Prop := False

lemma fcnl_on_empty {U V : Type}
    (R : Rel U V) {A : Set U} (h1 : empty A) : fcnl_on R A := by
  define
  fix a : U
  assume h2 : a ∈ A      --Goal : ∃! (y : V), R a y
  contradict h1 with h3  --Goal : ∃ (x : U), x ∈ A
  show ∃ (x : U), x ∈ A from Exists.intro a h2
  done

lemma empty_match {U V : Type} {A : Set U} {B : Set V}
    (h1 : empty A) (h2 : empty B) : matching (emptyRel U V) A B := by
  define
  apply And.intro
  · -- Proof of rel_within
    define
    fix a : U; fix b : V
    assume h3 : emptyRel U V a b   --Goal : a ∈ A ∧ b ∈ B
    by_contra h4                   --Goal : False
    define at h3
    show False from h3
    done
  · -- Proof of fcnl_ons
    apply And.intro
    · -- Proof of fcnl_on emptyRel
      show fcnl_on (emptyRel U V) A from fcnl_on_empty (emptyRel U V) h1
      done
    · -- Proof of fcnl_on (invRel emptyRel)
      show fcnl_on (invRel (emptyRel U V)) B from
        fcnl_on_empty (invRel (emptyRel U V)) h2
      done
  done

lemma I_0_empty : empty (I 0) := by
  define
  by_contra h1    --h1 : ∃ (x : Nat), x ∈ I 0
  obtain (x : Nat) (h2 : x ∈ I 0) from h1
  define at h2    --h2 : x < 0
  linarith
  done

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
    by_contra h2         --h2 : ∃ (x : U), x ∈ A
    obtain (x : U) (h3 : x ∈ A) from h2
    define at h1
    obtain (R : Rel Nat U) (h4 : matching R (I 0) A) from h1
    define at h4
      --h4 : rel_within R (I 0) A ∧ fcnl_on R (I 0) ∧ fcnl_on (invRel R) A
    obtain (j : Nat) (h5 : invRel R x j) from
      fcnl_exists h4.right.right h3
    define at h5         --h5 : R j x
    have h6 : j ∈ I 0 ∧ x ∈ A := h4.left h5
    contradict I_0_empty --Goal : ∃ (x : Nat), x ∈ I 0
    show ∃ (x : Nat), x ∈ I 0 from Exists.intro j h6.left
    done
  · -- (←)
    assume h1 : empty A
    show ∃ (R : Rel Nat U), matching R (I 0) A from
      Exists.intro (emptyRel Nat U) (empty_match I_0_empty h1)
    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 (R : Rel Nat U) (h3 : matching R (I n) A) from h1
  define at h3
  have h4 : 0 ∈ I n := h2
  obtain (x : U) (h5 : R 0 x) from fcnl_exists h3.right.left h4
  have h6 : 0 ∈ I n ∧ x ∈ A := h3.left h5
  show ∃ (x : U), x ∈ A from Exists.intro x h6.right
  done
```

To prove our next theorem about `numElts`, we will need to prove that two relations are equal.  How can we do that?  To prove that two sets are equal, we usually start by applying `Set.ext`, and to prove that two functions are equal we apply `funext`.  We'll need a similar extensionality principle for relations.  If `R` and `S` are relations from `U` to `V`, the principle will say that if we have `h : ∀ (u : U) (v : V), R u v ↔ S u v`, then we can conclude that `R = S`.  To prove it, we'll use `h` to prove `extension R = extension S`, and then go on to deduce `R = S`.

```lean
theorem relext {U V : Type} {R S : Rel U V}
    (h : ∀ (u : U) (v : V), R u v ↔ S u v) : R = S := by
  have h2 : extension R = extension S := by
    apply Set.ext
    fix (u, v) : U × V --Goal : (u, v) ∈ extension R ↔ (u, v) ∈ extension S
    rewrite [ext_def, ext_def]  --Goal : R u v ↔ S u v
    show R u v ↔ S u v from h u v
    done
  show R = S from
    calc R
      _ = RelFromExt (extension R) := by rfl
      _ = RelFromExt (extension S) := by rw [h2]
      _ = S := by rfl
  done
```

Now we are ready to prove that if `A` has `n + 1` elements and we remove one element, then the resulting set has `n` elements.  The key lemma for this proof says that if `A ∼ B`, `u ∈ A`, and `v ∈ B`, then `A \ {u} ∼ B \ {v}`.  To see how to prove this lemma, suppose that `R` is a matching from `A` to `B`.  We must find a way to modify `R` to get a matching from `A \ {u}` to `B \ {v}`.  If we're lucky, `R u v` will be true, in which case if we simply eliminate the pairing of `u` with `v` from `R`, the resulting relation will be a matching from `A \ {u}` to `B \ {v}`.  But it may happen that `R u v` is not true.  In that case, there must be some `x ∈ A \ {u}` and some `y ∈ B \ {v}` such that `R x v` and `R u y`.  When we remove `u` from `A` and `v` from `B`, `x` and `y` will be left unpaired.  The obvious solution is to pair them with each other!  This motivates the definition of a new relation `remove_one R u v`:

```lean
def remove_one {U V : Type} (R : Rel U V) (u : U) (v : V)
  (x : U) (y : V) : Prop := x ≠ u ∧ y ≠ v ∧ (R x y ∨ (R x v ∧ R u y))

lemma remove_one_def {U V : Type} (R : Rel U V) (u x : U) (v y : V) :
    remove_one R u v x y ↔
      x ≠ u ∧ y ≠ v ∧ (R x y ∨ (R x v ∧ R u y)) := by rfl
```

Our strategy now is to prove that `remove_one R u v` is a matching from `A \ {u}` to `B \ {v}`.  The proof is long but not hard, so we skip some of the details.

```lean
lemma remove_one_rel_within {U V : Type}
    {R : Rel U V} {A : Set U} {B : Set V} {x u : U} {y v : V}
    (h1 : matching R A B) (h2 : remove_one R u v x y) :
    x ∈ A \ {u} ∧ y ∈ B \ {v} := sorry

lemma remove_one_inv {U V : Type} (R : Rel U V) (u : U) (v : V) :
    invRel (remove_one R u v) = remove_one (invRel R) v u := by
  apply relext
  fix y : V; fix x : U
    --Goal : invRel (remove_one R u v) y x ↔ remove_one (invRel R) v u y x
  rewrite [invRel_def, remove_one_def, remove_one_def]
  rewrite [invRel_def, invRel_def, invRel_def]
  rewrite [←and_assoc, ←and_assoc]
    --Goal : (x ≠ u ∧ y ≠ v) ∧ (R x y ∨ R x v ∧ R u y) ↔
    --       (y ≠ v ∧ x ≠ u) ∧ (R x y ∨ R u y ∧ R x v)
  have h1 : x ≠ u ∧ y ≠ v ↔ y ≠ v ∧ x ≠ u := and_comm
  have h2 : R x v ∧ R u y ↔ R u y ∧ R x v := and_comm
  rewrite [h1, h2]
  rfl
  done

lemma remove_one_iff {U V : Type}
    {A : Set U} {B : Set V} {R : Rel U V} (h1 : matching R A B)
    {u : U} (h2 : u ∈ A) (v : V) {x : U} (h3 : x ∈ A \ {u}) :
    ∃ w ∈ A, ∀ (y : V), remove_one R u v x y ↔ R w y := sorry

theorem remove_one_fcnl {U V : Type}
    {R : Rel U V} {A : Set U} {B : Set V} {u : U}
    (h1 : matching R A B) (h2 : u ∈ A) (v : V) :
    fcnl_on (remove_one R u v) (A \ {u}) := by
  define
  fix x : U
  assume h3 : x ∈ A \ {u}  --Goal : ∃! (y : V), remove_one R u v x y
  obtain (w : U) (h4 : w ∈ A ∧ ∀ (y : V),
    remove_one R u v x y ↔ R w y) from remove_one_iff h1 h2 v h3
  define at h1
  exists_unique
  · -- Existence
    obtain (y : V) (h5 : R w y) from fcnl_exists h1.right.left h4.left
    apply Exists.intro y
    rewrite [h4.right]
    show R w y from h5
    done
  · -- Uniqueness
    fix y1 : V; fix y2 : V
    rewrite [h4.right, h4.right]
    assume h5 : R w y1
    assume h6 : R w y2
    show y1 = y2 from fcnl_unique h1.right.left h4.left h5 h6
    done
  done

theorem remove_one_match {U V : Type}
    {R : Rel U V} {A : Set U} {B : Set V} {u : U} {v : V}
    (h1 : matching R A B) (h2 : u ∈ A) (h3 : v ∈ B) :
    matching (remove_one R u v) (A \ {u}) (B \ {v}) := by
  define
  apply And.intro
  · -- Proof of rel_within
    define
    fix x : U; fix y : V
    assume h4 : remove_one R u v x y
    show x ∈ A \ {u} ∧ y ∈ B \ {v} from remove_one_rel_within h1 h4
    done
  · -- Proof of fcnl_ons
    apply And.intro (remove_one_fcnl h1 h2 v)
    rewrite [remove_one_inv]
    show fcnl_on (remove_one (invRel R) v u) (B \ {v}) from
      remove_one_fcnl (inv_match h1) h3 u
  done

theorem remove_one_equinum {U V : Type}
    {A : Set U} {B : Set V} {u : U} {v : V}
    (h1 : A ∼ B) (h2 : u ∈ A) (h3 : v ∈ B) : A \ {u} ∼ B \ {v} := by
  define
  obtain (R : Rel U V) (h4 : matching R A B) from h1
  apply Exists.intro (remove_one R u v)
  show matching (remove_one R u v) (A \ {u}) (B \ {v}) from
    remove_one_match h4 h2 h3
  done

lemma I_max (n : Nat) : n ∈ I (n + 1) := sorry

lemma I_diff (n : Nat) : I (n + 1) \ {n} = I n := 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
  have h3 : n ∈ I (n + 1) := I_max n
  rewrite [numElts_def] at h1     --h1 : I (n + 1) ∼ X
  have h4 : I (n + 1) \ {n} ∼ A \ {a} := remove_one_equinum h1 h3 h2
  rewrite [I_diff] at h4          --h4 : I n ∼ A \ {a}
  show numElts (A \ {a}) n from h4
  done
```

Finally, we prove that a set has one element if and only if it is a singleton set.  For this proof, we need to be able to produce a relation that is a matching between two singleton sets.  Suppose we have `a : U` and `b : V`.  Of course, a matching from `{a}` to `{b}` must pair `a` with `b`, so we make the following definition:

```lean
def one_match {U V : Type} (a : U) (b : V)
  (x : U) (y : V) : Prop := x = a ∧ y = b
  
lemma one_match_def {U V : Type} (a x : U) (b y : V) :
    one_match a b x y ↔ x = a ∧ y = b := by rfl
```

We prove the theorem using a few lemmas, whose proofs we leave to you.

```lean
lemma one_match_match {U V : Type} (a : U) (b : V) :
    matching (one_match a b) {a} {b} := sorry

lemma I_1_singleton : I 1 = {0} := sorry

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

lemma singleton_one_elt {U : Type} (u : U) : numElts {u} 1 := by
  define
  rewrite [I_1_singleton]
  show ∃ (R : Rel Nat U), matching R {0} {u} from
    Exists.intro (one_match 0 u) (one_match_match 0 u)
  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 decide
    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.

```lean
lemma eq_zero_of_I_zero_equinum {n : Nat} (h1 : I 0 ∼ I n) : n = 0 := by
  rewrite [←numElts_def, zero_elts_iff_empty] at h1
    --h1 : empty (I n)
  contradict h1 with h2       --Goal : ∃ (x : Nat), x ∈ I n
  apply Exists.intro 0
  define
  show 0 < n from Nat.pos_of_ne_zero h2
  done

theorem eq_of_I_equinum : ∀ ⦃m n : Nat⦄, I m ∼ I n → m = n := by
  by_induc
  · -- Base Case
    fix n : Nat
    assume h1 : I 0 ∼ I n
    show 0 = n from (eq_zero_of_I_zero_equinum h1).symm
    done
  · -- Induction Step
    fix m : Nat
    assume ih : ∀ ⦃n : Nat⦄, I m ∼ I n → m = n
    fix n : Nat
    assume h1 : I (m + 1) ∼ I n      --Goal : m + 1 = n
    have h2 : n ≠ 0 := by
      by_contra h2
      have h3 : I n ∼ I (m + 1) := Theorem_8_1_3_2 h1
      rewrite [h2] at h3
      have h4 : m + 1 = 0 := eq_zero_of_I_zero_equinum h3
      linarith
      done
    obtain (k : Nat) (h3 : n = k + 1) from exists_eq_add_one_of_ne_zero h2
    rewrite [h3] at h1               --h1 : I (m + 1) ∼ I (k + 1)
    rewrite [h3]                     --Goal : m + 1 = k + 1
    have h4 : m ∈ I (m + 1) := I_max m
    have h5 : k ∈ I (k + 1) := I_max k
    have h6 : I (m + 1) \ {m} ∼ I (k + 1) \ {k} :=
      remove_one_equinum h1 h4 h5
    rewrite [I_diff, I_diff] at h6   --h6 : I m ∼ I k
    have h7 : m = k := ih h6
    rewrite [h7]
    rfl
    done
  done

theorem numElts_unique {U : Type} {A : Set U} {m n : Nat}
    (h1 : numElts A m) (h2 : numElts A n) : m = n := by
  rewrite [numElts_def] at h1      --h1 : I m ∼ A
  rewrite [numElts_def] at h2      --h2 : I n ∼ A
  have h3 : A ∼ I n := Theorem_8_1_3_2 h2
  have h4 : I m ∼ I n := Theorem_8_1_3_3 h1 h3
  show m = n from eq_of_I_equinum h4
  done
```

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]    --Goal : I (phi 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
  have h2 : num_elts_below (Set_rp_below m) m (phi m) := neb_phi m
  show I (phi m) ∼ Set_rp_below m from bdd_subset_nat h1 h2
  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$.  We would like to prove this in Lean, but how do we state the theorem?  In Lean, Cartesian product is an operation on types, not sets.  However, we can 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`.

We can now state the theorem corresponding to the first part of Theorem 8.1.2 in *HTPI*.

```lean
theorem Theorem_8_1_2_1
    {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
```

To see how to prove this theorem, suppose that `R` is a matching from `A` to `B` and `S` is a matching from `C` to `D`.  We must produce a matching from `A ×ₛ C` to `B ×ₛ D`.  The following definition is motivated by the proof in *HTPI*:

```lean
def Rel_prod {U V W X : Type} (R : Rel U V) (S : Rel W X)
  (p : U × W) (q : V × X) : Prop := R p.1 q.1 ∧ S p.2 q.2

notation:75 R:75 " ×ᵣ " S:75 => Rel_prod R S

lemma Rel_prod_def {U V W X : Type} (R : Rel U V) (S : Rel W X)
    (u : U) (v : V) (w : W) (x : X) :
    (R ×ᵣ S) (u, w) (v, x) ↔ R u v ∧ S w x := by rfl
```

With this definition, `R ×ᵣ S` is a relation from `U × W` to `V × X`.  (Of course, to type the subscript `r` after `×`, you should type `\_r`.)  We leave the proof that `R ×ᵣ S` is a matching from `A ×ₛ C` to `B ×ₛ D` as an exercise for you.

```lean
lemma prod_match {U V W X : Type}
    {A : Set U} {B : Set V} {C : Set W} {D : Set X}
    {R : Rel U V} {S : Rel W X}
    (h1 : matching R A B) (h2 : matching S C D) :
    matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D) := sorry

theorem Theorem_8_1_2_1
    {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
  obtain (R : Rel U V) (h3 : matching R A B) from h1
  obtain (S : Rel W X) (h4 : matching S C D) from h2
  apply Exists.intro (R ×ᵣ S)
  show matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D) from prod_match h3 h4
  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` 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 := equinum_image
  (one_one_on_of_one_one (qr_one_one n) (I (m * n))) (qr_image m n)

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 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) :=
  equinum_image (mod_mod_one_one_on h1) (mod_mod_image h1)
```

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 numElts_unique h5 h6
  done
```

### Exercises

::: {.numex arguments="1"}
```lean
lemma remove_one_iff {U V : Type}
    {A : Set U} {B : Set V} {R : Rel U V} (h1 : matching R A B)
    {u : U} (h2 : u ∈ A) (v : V) {x : U} (h3 : x ∈ A \ {u}) :
    ∃ w ∈ A, ∀ (y : V), remove_one R u v x y ↔ R w y := sorry
```
:::

::: {.numex arguments="2"}
```lean
lemma inv_one_match {U V : Type} (a : U) (b : V) :
    invRel (one_match a b) = one_match b a := sorry
```
:::

::: {.numex arguments="3"}
```lean
theorem one_match_fcnl {U V : Type} (a : U) (b : V) :
    fcnl_on (one_match a b) {a} := sorry
```
:::

::: {.numex arguments="4"}
```lean
--Hint:  Use the previous two exercises.
lemma one_match_match {U V : Type} (a : U) (b : V) :
    matching (one_match a b) {a} {b} := sorry
```
:::

::: {.numex arguments="5"}
```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="6"}
```lean
lemma prod_fcnl {U V W X : Type} {R : Rel U V} {S : Rel W X}
    {A : Set U} {C : Set W} (h1 : fcnl_on R A) (h2 : fcnl_on S C) :
    fcnl_on (R ×ᵣ S) (A ×ₛ C) := sorry
```
:::

::: {.numex arguments="7"}
```lean
--Hint:  Use the previous exercise.
lemma prod_match {U V W X : Type}
    {A : Set U} {B : Set V} {C : Set W} {D : Set X}
    {R : Rel U V} {S : Rel W X}
    (h1 : matching R A B) (h2 : matching S C D) :
    matching (R ×ᵣ S) (A ×ₛ C) (B ×ₛ D) := 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
```
:::

::: {.numex arguments="9"}
```lean
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="10"}
```lean
lemma shift_I_equinum (n m : Nat) : I m ∼ I (n + m) \ I n := sorry
```
:::

::: {.numex arguments="11"}
```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="12"}
```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="13"}
```lean
theorem Exercise_8_1_8b {U : Type} {A B : Set U}
    (h1 : finite A) (h2 : B ⊆ A) : finite B := sorry
```
:::

::: {.numex arguments="14"}
```lean
--Hint:  Use Like_Exercise_6_2_16 from the exercises of Section 6.2
lemma N_not_finite : ¬finite (Univ Nat) := sorry
```
:::

::: {.numex arguments="15"}
```lean
theorem denum_not_finite {U : Type} {A : Set U}
    (h : denum A) : ¬finite A := 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` and the countability of `Univ (Nat × Nat)`.  We also use an exercise from Section 8.1.

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

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_equinum_set_nat] at h1
  rewrite [ctble_iff_equinum_set_nat] at h2
  obtain (I : Set Nat) (h3 : I ∼ A) from h1
  obtain (J : Set Nat) (h4 : J ∼ B) from h2
  have h5 : I ×ₛ J ∼ A ×ₛ B := Theorem_8_1_2_1 h3 h4
  have h6 : I ×ₛ J ⊆ Univ (Nat × Nat) := by
    fix p : Nat × Nat
    assume h6 : p ∈ I ×ₛ J
    show p ∈ Univ (Nat × Nat) from elt_Univ p
    done
  have h7 : ctble (Univ (Nat × Nat)) := by
    define   --Goal : finite (Univ (Nat × Nat)) ∨ denum (Univ (Nat × Nat))
    apply Or.inr
    rewrite [denum_def]
    show Univ Nat ∼ Univ (Nat × Nat) from Theorem_8_1_3_2 NxN_equinum_N
    done
  have h8 : ctble (I ×ₛ J) := Exercise_8_1_17 h6 h7
  show ctble (A ×ₛ B) from ctble_of_equinum_ctble h5 h8
  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)
```

In our proof, we will use the characterization of countability from `Theorem_8_1_5_2`.  Thus, we will use the hypotheses `h1` and `h2` to conclude that there is a relation `R : Rel Nat (Set U)` such that `fcnl_onto_from_nat R F`, and also that for each `A ∈ F` there is a relation `SA : Rel Nat U` such that `fcnl_onto_from_nat SA A`.  We begin by proving an easier version of the theorem, where we assume that we have a function `f : Set U → Rel Nat U` that supplies, for each `A ∈ F`, the required relation `SA`.  Imitating the proof in *HTPI*, we can use `R` and `f` to construct the relation needed to prove that `⋃₀ F` is countable.

```lean
def enum_union_fam {U : Type}
  (F : Set (Set U)) (f : Set U → Rel Nat U) (R : Rel Nat (Set U))
  (n : Nat) (a : U) : Prop := ∃ (p : Nat × Nat), fnnn p = n ∧
    ∃ A ∈ F, R p.1 A ∧ (f A) p.2 a

lemma Lemma_8_2_2_1 {U : Type} {F : Set (Set U)} {f : Set U → Rel Nat U}
    (h1 : ctble F) (h2 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A) :
    ctble (⋃₀ F) := by
  rewrite [Theorem_8_1_5_2] at h1
  rewrite [Theorem_8_1_5_2]
  obtain (R : Rel Nat (Set U)) (h3 : fcnl_onto_from_nat R F) from h1
  define at h3
  have Runiqueval : unique_val_on_N R := h3.left
  have Ronto : nat_rel_onto R F := h3.right
  set S : Rel Nat U := enum_union_fam F f R
  apply Exists.intro S
  define
  apply And.intro
  · -- Proof of unique_val_on_N S
    define
    fix n : Nat; fix a1 : U; fix a2 : U
    assume Sna1 : S n a1
    assume Sna2 : S n a2         --Goal : a1 = a2
    define at Sna1; define at Sna2
    obtain ((i1, j1) : Nat × Nat) (h4 : fnnn (i1, j1) = n ∧
      ∃ A ∈ F, R i1 A ∧ f A j1 a1) from Sna1
    obtain (A1 : Set U) (Aija1 : A1 ∈ F ∧ R i1 A1 ∧ f A1 j1 a1)
      from h4.right
    obtain ((i2, j2) : Nat × Nat) (h5 : fnnn (i2, j2) = n ∧
      ∃ A ∈ F, R i2 A ∧ f A j2 a2) from Sna2
    obtain (A2 : Set U) (Aija2 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a2)
      from h5.right
    rewrite [←h5.left] at h4
    have h6 : (i1, j1) = (i2, j2) :=
      fnnn_one_one (i1, j1) (i2, j2) h4.left
    have h7 : i1 = i2 ∧ j1 = j2 := Prod.mk.inj h6
    rewrite [h7.left, h7.right] at Aija1
      --Aija1 : A1 ∈ F ∧ R i2 A1 ∧ f A1 j2 a1
    define at Runiqueval
    have h8 : A1 = A2 := Runiqueval Aija1.right.left Aija2.right.left
    rewrite [h8] at Aija1       --Aija1 : A2 ∈ F ∧ R i2 A2 ∧ f A2 j2 a1
    have fA2fcnlonto : fcnl_onto_from_nat (f A2) A2 := h2 A2 Aija2.left
    define at fA2fcnlonto
    have fA2uniqueval : unique_val_on_N (f A2) := fA2fcnlonto.left
    define at fA2uniqueval
    show a1 = a2 from fA2uniqueval Aija1.right.right Aija2.right.right
    done
  · -- Proof of nat_rel_onto S (⋃₀ F)
    define
    fix x : U
    assume h4 : x ∈ ⋃₀ F    --Goal : ∃ (n : Nat), S n x
    define at h4
    obtain (A : Set U) (h5 : A ∈ F ∧ x ∈ A) from h4
    define at Ronto
    obtain (i : Nat) (h6 : R i A) from Ronto h5.left
    have fAfcnlonto : fcnl_onto_from_nat (f A) A := h2 A h5.left
    define at fAfcnlonto
    have fAonto : nat_rel_onto (f A) A := fAfcnlonto.right
    define at fAonto
    obtain (j : Nat) (h7 : f A j x) from fAonto h5.right
    apply Exists.intro (fnnn (i, j))
    define    --Goal : ∃ (p : Nat × Nat), fnnn p = fnnn (i, j) ∧
              --       ∃ A ∈ F, R p.1 A ∧ f A p.2 x
    apply Exists.intro (i, j)
    apply And.intro
    · -- Proof that fnnn (i, j) = fnnn (i, j)
      rfl
      done
    · -- Proof that ∃ A ∈ F, R (i, j).1 A ∧ f A (i, j).2 x
      apply Exists.intro A
      show A ∈ F ∧ R (i, j).1 A ∧ f A (i, j).2 x from
        And.intro h5.left (And.intro h6 h7)
      done
    done
  done
```

How can we use `Lemma_8_2_2_1` to prove `Theorem_8_2_2`?  We must use the hypothesis `h2 : ∀ A ∈ F, ctble A` in `Theorem_8_2_2` to produce the function `f` 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 relation `SA : Rel Nat U` exists.  We need a function `f` that will *choose* such a relation `SA` 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 relation `SA` for each `A` and the existence of a function that chooses such a relation 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)} (h : ∀ A ∈ F, ctble A) :
    ∃ (f : Set U → Rel Nat U), ∀ A ∈ F, fcnl_onto_from_nat (f A) A := by
  have h1 : ∀ (A : Set U), ∃ (SA : Rel Nat U),
      A ∈ F → fcnl_onto_from_nat SA A := by
    fix A : Set U
    by_cases h2 : A ∈ F
    · -- Case 1. h2 : A ∈ F
      have h3 : ctble A := h A h2
      rewrite [Theorem_8_1_5_2] at h3
      obtain (SA : Rel Nat U) (h4 : fcnl_onto_from_nat SA A) from h3
      apply Exists.intro SA
      assume h5 : A ∈ F
      show fcnl_onto_from_nat SA A from h4
      done
    · -- Case 2. h2 : A ∉ F
      apply Exists.intro (emptyRel Nat U)
      assume h3 : A ∈ F
      show fcnl_onto_from_nat (emptyRel Nat U) A from absurd h3 h2
      done
    done
  set f : Set U → Rel Nat U := fun (A : Set U) => Classical.choose (h1 A)
  apply Exists.intro f
  fix A : Set U
  show A ∈ F → fcnl_onto_from_nat (f A) A from Classical.choose_spec (h1 A)
  done
```

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

We now have everything in place to prove `Theorem_8_2_2`:

```lean
theorem Theorem_8_2_2 {U : Type} {F : Set (Set U)}
    (h1 : ctble F) (h2 : ∀ A ∈ F, ctble A) : ctble (⋃₀ F) := by
  obtain (f : Set U → Rel Nat U) (h3 : ∀ A ∈ F, fcnl_onto_from_nat (f A) A)
    from Lemma_8_2_2_2 h2
  show ctble (⋃₀ F) from Lemma_8_2_2_1 h1 h3
  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] 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.rtl h1)
    define           --Goal : ∀ x ∈ l, x ∈ A
    fix x : U
    assume h2 : x ∈ l
    contradict h2 with h3
    rewrite [h1]
    show x ∉ [] from List.not_mem_nil x
    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) :=
  equinum_image (one_one_on_of_one_one (seq_cons_one_one U)
    (A ×ₛ (seq_by_length A n))) (seq_cons_image A n)
```

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_equinum_ctble 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 apply an exercise from Section 8.1.

```lean
theorem ctble_of_onto_func_from_N {U : Type} {A : Set U} {f : Nat → U}
    (h1 : ∀ x ∈ A, ∃ (n : Nat), f n = x) : ctble A := sorry

lemma Lemma_8_2_4_4 {U : Type} (A : Set U) : ctble (sbl_set A) := by
  have h1 : ∀ S ∈ sbl_set A, ∃ (n : Nat), seq_by_length A n = S := by
    fix S : Set (List U)
    assume h1 : S ∈ sbl_set A
    define at h1
    show ∃ (n : Nat), seq_by_length A n = S from h1
    done
  show ctble (sbl_set A) from ctble_of_onto_func_from_N 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 use this strategy to prove that `𝒫 (Univ Nat)` is uncountable.

```lean
lemma set_elt_powerset_univ {U : Type} (A : Set U) :
    A ∈ 𝒫 (Univ U) := by
  fix x : U
  assume h : x ∈ A
  show x ∈ Univ U from elt_Univ x
  done

theorem Cantor's_theorem : ¬ctble (𝒫 (Univ Nat)) := by
  by_contra h1
  rewrite [Theorem_8_1_5_2] at h1
  obtain (R : Rel Nat (Set Nat))
    (h2 : fcnl_onto_from_nat R (𝒫 (Univ Nat))) from h1
  define at h2
  have h3 : unique_val_on_N R := h2.left
  have h4 : nat_rel_onto R (𝒫 (Univ Nat)) := h2.right
  set D : Set Nat := {n : Nat | ∃ (X : Set Nat), R n X ∧ n ∉ X}
  have h5 : D ∈ 𝒫 (Univ Nat) := set_elt_powerset_univ D
  define at h4
  obtain (n : Nat) (h6 : R n D) from h4 h5
  by_cases h7 : n ∈ D
  · -- Case 1. h7 : n ∈ D
    contradict h7
    define at h7
    obtain (X : Set Nat) (h8 : R n X ∧ n ∉ X) from h7
    define at h3
    have h9 : D = X := h3 h6 h8.left
    rewrite [h9]
    show n ∉ X from h8.right
    done
  · -- Case 2. h7 : n ∉ D
    contradict h7
    define
    show ∃ (X : Set Nat), R n X ∧ n ∉ X from
      Exists.intro D (And.intro h6 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} := 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 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="4"}
```lean
--Hint:  Use induction on the size of A
lemma set_to_list {U : Type} {A : Set U} (h : finite A) :
    ∃ (l : List U), ∀ (x : U), x ∈ l ↔ x ∈ A := sorry
```
:::

::: {.numex arguments="5"}
```lean
--Hint:  Use the previous exercise and Theorem_8_2_4
theorem Like_Exercise_8_2_4 {U : Type} {A : Set U} (h : ctble A) :
    ctble {X : Set U | X ⊆ A ∧ finite X} := sorry
```
:::

::: {.numex arguments="6"}
```lean
theorem Exercise_8_2_6b (A B C : Type) :
    Univ ((A × B) → C) ∼ Univ (A → (B → C)) := sorry
```
:::

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

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

::: {.numex arguments="9"}
```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 $A$ and $B$ are sets such that each is equinumerous with a subset of the other, then $A$ and $B$ are equinumerous.  In the notation we are using in this chapter, it can be stated as follows:

```lean
theorem Cantor_Schroeder_Bernstein_theorem
    {U V : Type} {A C : Set U} {B D : Set V}
    (h1 : C ⊆ A) (h2 : D ⊆ B) (h3 : A ∼ D) (h4 : C ∼ B) : A ∼ B
```

The hypotheses `h3` and `h4` imply that there are matchings `R` from `A` to `D` and `S` from `C` to `B`.  To prove the theorem, we must construct a matching `T` from `A` to `B`.  Imitating the proof in *HTPI*, we will do this by defining a set `X ⊆ A` and then combining `R` restricted to `X` with `S` restricted to `A \ X`.  In other words, `T x y` will be defined to mean:

::: {.ind}
```
(x ∈ X ∧ R x y) ∨ (x ∉ X ∧ S x y)
```
:::

Which elements of `A` should be in `X`?  We start with the fact that, since `S` is a relation within `C` and `B`, elements of `A \ C` are not paired with anything by `S`, so they must be in `X`.  In other words, if we define `X0` to be `A \ C`, then we must have `X0 ⊆ X`.

Now suppose `x ∈ X0`, `a ∈ A`, `y ∈ B`, and `R x y` and `S a y` are both true.  In this situation we will say that `x` and `a` have a *common image* under `R` and `S`.  If `a ∉ X`, then we will have `T x y` and `T a y`, which means that `T` will fail to be a matching.  Thus, we must have `a ∈ X`.  In other words, if we define `X1` to be the set of all `a` such that for some `x ∈ X0`, `x` and `a` have a common image under `R` and `S`, then we'll need to have `X1 ⊆ X`.  But now the same reasoning applies to `X1`: if `X2` is the set of all `a` such that for some `x ∈ X1`, `x` and `a` have a common image, then `X2` must also be contained in `X`.  Iterating this reasoning motivates the following definition:

```lean
def rep_common_image
  {U V : Type} (R S : Rel U V) (X0 : Set U) (n : Nat) : Set U :=
  match n with
    | 0 => X0
    | m + 1 => {a : U | ∃ x ∈ rep_common_image R S X0 m,
                          ∃ (y : V), R x y ∧ S a y}

lemma rep_common_image_step
    {U V : Type} (R S : Rel U V) (X0 : Set U) (m : Nat) (a : U) :
    a ∈ rep_common_image R S X0 (m + 1) ↔
    ∃ x ∈ rep_common_image R S X0 m, ∃ (y : V), R x y ∧ S a y := by rfl
```

The sets `rep_common_image R S X0 n` correspond to the sets $A_n$ in *HTPI*.  As in *HTPI*, to define `X` we take the union of these sets.

```lean
def cum_rep_image {U V : Type} (R S : Rel U V) (X0 : Set U) : Set U :=
  {a : U | ∃ (n : Nat), a ∈ rep_common_image R S X0 n}
```

In our proof of the Cantor--Schröder--Bernstein theorem, we will define `X` to be the set `cum_rep_image R S X0`, and therefore the matching `T` will be the relation `csb_match R S X0` defined as follows:

```lean
def csb_match {U V : Type} (R S : Rel U V) (X0 : Set U)
  (x : U) (y : V) : Prop := x ∈ cum_rep_image R S X0 ∧ R x y ∨
    x ∉ cum_rep_image R S X0 ∧ S x y
```

It will be convenient to prove a few simple lemmas about these definitions.  Our first two lemmas spell out that, for `x ∈ X`, `T x y` means `R x y`, and for `x ∉ X`, `T x y` means `S x y`.

```lean
lemma csb_match_cri {U V : Type} {R S : Rel U V} {X0 : Set U}
    {x : U} {y : V} (h1 : csb_match R S X0 x y)
    (h2 : x ∈ cum_rep_image R S X0) : R x y := by
  by_cases on h1
  · -- Case 1. h1 : x ∈ cum_rep_image R S X0 ∧ R x y
    show R x y from h1.right
    done
  · -- Case 2. h1 : x ∉ cum_rep_image R S X0 ∧ S x y
    show R x y from absurd h2 h1.left
    done
  done

lemma csb_match_not_cri {U V : Type} {R S : Rel U V} {X0 : Set U}
    {x : U} {y : V} (h1 : csb_match R S X0 x y)
    (h2 : x ∉ cum_rep_image R S X0) : S x y := sorry
```

We will also need to know that it cannot happen that `T x1 y`, `T x2 y`, `x1 ∈ X`, and `x2 ∉ X`:

```lean
lemma csb_cri_of_cri
    {U V : Type} {R S : Rel U V} {X0 : Set U} {x1 x2 : U} {y : V}
    (h1 : csb_match R S X0 x1 y) (h2 : csb_match R S X0 x2 y)
    (h3 : x1 ∈ cum_rep_image R S X0) : x2 ∈ cum_rep_image R S X0 := by
  have h4 : R x1 y := csb_match_cri h1 h3
  by_contra h5
  have h6 : S x2 y := csb_match_not_cri h2 h5
  contradict h5       --Goal : x2 ∈ cum_rep_image R S X0
  define at h3
  define
  obtain (n : Nat) (h7 : x1 ∈ rep_common_image R S X0 n) from h3
  apply Exists.intro (n + 1)  --Goal : x2 ∈ rep_common_image R S X0 (n + 1)
  rewrite [rep_common_image_step]
  apply Exists.intro x1
    --Goal : x1 ∈ rep_common_image R S X0 n ∧ ∃ (y : V), R x1 y ∧ S x2 y
  apply And.intro h7
  show ∃ (y : V), R x1 y ∧ S x2 y from Exists.intro y (And.intro h4 h6)
  done
```

With that preparation, we are ready to prove the theorem.

```lean
theorem Cantor_Schroeder_Bernstein_theorem
    {U V : Type} {A C : Set U} {B D : Set V}
    (h1 : C ⊆ A) (h2 : D ⊆ B) (h3 : A ∼ D) (h4 : C ∼ B) : A ∼ B := by
  obtain (R : Rel U V) (R_match_AD : matching R A D) from h3
  obtain (S : Rel U V) (S_match_CB : matching S C B) from h4
  define at R_match_AD; define at S_match_CB
  set X0 : Set U := A \ C
  set X : Set U := cum_rep_image R S X0
  set T : Rel U V := csb_match R S X0
  have Tdef : ∀ (x : U) (y : V),
      T x y ↔ (x ∈ X ∧ R x y) ∨ (x ∉ X ∧ S x y) := by
    fix x : U; fix y : V
    rfl
    done
  have A_not_X_in_C : A \ X ⊆ C := by
    fix a : U
    assume h5 : a ∈ A \ X
    contradict h5.right with h6  --h6 : a ∉ C;  Goal : a ∈ X
    define  --Goal : ∃ (n : Nat), a ∈ rep_common_image R S X0 n
    apply Exists.intro 0 
    define
    show a ∈ A ∧ a ∉ C from And.intro h5.left h6
    done
  define    --Goal : ∃ (R : Rel U V), matching R A B
  apply Exists.intro T
  define    --Goal : rel_within T A B ∧ fcnl_on T A ∧ fcnl_on (invRel T) B
  apply And.intro
  · -- Proof of rel_within T A B
    define
    fix a : U; fix b : V
    assume h5 : T a b
    rewrite [Tdef] at h5   --h5 : a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b
    by_cases on h5
    · -- Case 1. h5 : a ∈ X ∧ R a b
      have h6 : a ∈ A ∧ b ∈ D := R_match_AD.left h5.right
      show a ∈ A ∧ b ∈ B from And.intro h6.left (h2 h6.right)
      done
    · -- Case 2. h5 : a ∉ X ∧ S a b
      have h6 : a ∈ C ∧ b ∈ B := S_match_CB.left h5.right
      show a ∈ A ∧ b ∈ B from And.intro (h1 h6.left) h6.right
      done
    done
  · -- Proof of fcnl_ons
    apply And.intro
    · -- Proof of fcnl_on T A
      define
      fix a : U
      assume aA : a ∈ A   --Goal : ∃! (y : V), T a y
      exists_unique
      · -- Existence
        by_cases h5 : a ∈ X
        · -- Case 1. h5 : a ∈ X
          obtain (b : V) (Rab : R a b) from
            fcnl_exists R_match_AD.right.left aA
          apply Exists.intro b
          rewrite [Tdef]
          show a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b from
            Or.inl (And.intro h5 Rab)
          done
        · -- Case 2. h5 : a ∉ X
          have aC : a ∈ C := A_not_X_in_C (And.intro aA h5)
          obtain (b : V) (Sab : S a b) from
            fcnl_exists S_match_CB.right.left aC
          apply Exists.intro b
          rewrite [Tdef]
          show a ∈ X ∧ R a b ∨ a ∉ X ∧ S a b from
            Or.inr (And.intro h5 Sab)
          done
        done
      · -- Uniqueness
        fix b1 : V; fix b2 : V
        assume Tab1 : T a b1
        assume Tab2 : T a b2
        by_cases h5 : a ∈ X
        · -- Case 1. h5 : a ∈ X
          have Rab1 : R a b1 := csb_match_cri Tab1 h5
          have Rab2 : R a b2 := csb_match_cri Tab2 h5
          show b1 = b2 from
            fcnl_unique R_match_AD.right.left aA Rab1 Rab2
          done
        · -- Case 2. h5 : a ∉ X
          have Sab1 : S a b1 := csb_match_not_cri Tab1 h5
          have Sab2 : S a b2 := csb_match_not_cri Tab2 h5
          have aC : a ∈ C := A_not_X_in_C (And.intro aA h5)
          show b1 = b2 from
            fcnl_unique S_match_CB.right.left aC Sab1 Sab2
          done
        done
      done
    · -- Proof of fcnl_on (invRel T) B
      define
      fix b : V
      assume bB : b ∈ B
      obtain (c : U) (Scb : S c b) from
        fcnl_exists S_match_CB.right.right bB
      have cC : c ∈ C := (S_match_CB.left Scb).left
      exists_unique
      · -- Existence
        by_cases h5 : c ∈ X
        · -- Case 1. h5 : c ∈ X
          define at h5
          obtain (n : Nat) (h6 : c ∈ rep_common_image R S X0 n) from h5
          have h7 : n ≠ 0 := by
            by_contra h7
            rewrite [h7] at h6
            define at h6       --h6 : c ∈ A ∧ c ∉ C
            show False from h6.right cC
            done
          obtain (m : Nat) (h8 : n = m + 1) from
            exists_eq_add_one_of_ne_zero h7
          rewrite [h8] at h6
          rewrite [rep_common_image_step] at h6
          obtain (a : U) (h9 : a ∈ rep_common_image R S X0 m ∧
            ∃ (y : V), R a y ∧ S c y) from h6
          apply Exists.intro a
          rewrite [invRel_def, Tdef]
          apply Or.inl    --Goal : a ∈ X ∧ R a b
          obtain (y : V) (h10 : R a y ∧ S c y) from h9.right
          have h11 : y = b :=
            fcnl_unique S_match_CB.right.left cC h10.right Scb
          rewrite [h11] at h10
          apply And.intro _ h10.left
          define
          show ∃ (n : Nat), a ∈ rep_common_image R S X0 n from
            Exists.intro m h9.left
          done
        · -- Case 2. h5 : c ∉ X
          apply Exists.intro c
          rewrite [invRel_def, Tdef]
          show c ∈ X ∧ R c b ∨ c ∉ X ∧ S c b from
            Or.inr (And.intro h5 Scb)
          done
        done
      · -- Uniqueness
        fix a1 : U; fix a2 : U
        assume Ta1b : T a1 b
        assume Ta2b : T a2 b
        by_cases h5 : a1 ∈ X
        · -- Case 1. h5 : a1 ∈ X
          have h6 : a2 ∈ X := csb_cri_of_cri Ta1b Ta2b h5
          have Ra1b : R a1 b := csb_match_cri Ta1b h5
          have Ra2b : R a2 b := csb_match_cri Ta2b h6
          have h7 : b ∈ D := (R_match_AD.left Ra1b).right
          show a1 = a2 from
            fcnl_unique R_match_AD.right.right h7 Ra1b Ra2b
          done
        · -- Case 2. h5 : a1 ∉ X
          have h6 : a2 ∉ X := by
            by_contra h6
            show False from h5 (csb_cri_of_cri Ta2b Ta1b h6)
            done
          have Sa1b : S a1 b := csb_match_not_cri Ta1b h5
          have Sa2b : S a2 b := csb_match_not_cri Ta2b h6
          show a1 = a2 from
            fcnl_unique S_match_CB.right.right bB Sa1b Sa2b
          done
        done
      done
    done
  done
```

### Exercises

::: {.numex arguments="1"}
```lean
theorem CSB_func {U V : Type} {f : U → V} {g : V → U}
    (h1 : one_to_one f) (h2 : one_to_one g) : Univ U ∼ Univ V := sorry
```
:::

::: {.numex arguments="2"}
```lean
theorem intervals_equinum :
    {x : Real | 0 < x ∧ x < 1} ∼ {x : Real | 0 < x ∧ x ≤ 1} := 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 power set of the natural numbers.  These exercises use the following definitions:

```lean
def EqRel (A : Type) : Set (BinRel A) :=
  {R : BinRel A | equiv_rel R}

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

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

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

def saz_pair (X : Set Nat) : Set (Set Nat) :=
  {shift_and_zero X, (Univ Nat) \ (shift_and_zero X)}
```

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

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

::: {.numex arguments="5"}
```lean
theorem EqRel_Nat_equinum_sub_PN :
    ∃ (D : Set (Set Nat)), D ⊆ 𝒫 (Univ Nat) ∧ EqRel Nat ∼ D := sorry
```
:::

::: {.numex arguments="6"}
```lean
theorem saz_pair_part (X : Set Nat) : partition (saz_pair X) := sorry
```
:::

::: {.numex arguments="7"}
```lean
theorem sub_EqRel_Nat_equinum_PN :
    ∃ (C : Set (BinRel Nat)), C ⊆ EqRel Nat ∧ C ∼ 𝒫 (Univ Nat) := sorry
```
:::

::: {.numex arguments="8"}
```lean
theorem EqRel_Nat_equinum_PN : EqRel Nat ∼ 𝒫 (Univ Nat) := sorry
```
:::