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

7  Number Theory

7.1. Greatest Common Divisors

The proofs in this chapter and the next are significantly longer than those in previous chapters. As a result, we will skip some details in the text, leaving proofs of a number of theorems as exercises for you. The most interesting of these exercises are included in the exercise lists at the ends of the sections; for the rest, you can compare your solutions to proofs that can be found in the Lean package that accompanies this book. Also, we will occasionally use theorems that we have not used before without explanation. If necessary, you can use #check to look up what they say.

Section 7.1 of HTPI introduces the Euclidean algorithm for computing the greatest common divisor (gcd) of two positive integers \(a\) and \(b\). The motivation for the algorithm is the fact that if \(r\) is the remainder when \(a\) is divided by \(b\), then any natural number that divides both \(a\) and \(b\) also divides \(r\), and any natural number that divides both \(b\) and \(r\) also divides \(a\).

Let’s prove these statements in Lean. Recall that in Lean, the remainder when a is divided by b is called a mod b, and it is denoted a % b. We’ll prove the first statement, and leave the second as an exercise for you. It will be convenient for our work with greatest common divisors in Lean to let a and b be natural numbers rather than positive integers (thus allowing either of them to be zero).

theorem dvd_mod_of_dvd_a_b {a b d : Nat}
    (h1 : d ∣ a) (h2 : d ∣ b) : d ∣ (a % b) := by
  set q : Nat := a / b
  have h3 : b * q + a % b = a := Nat.div_add_mod a b
  obtain (j : Nat) (h4 : a = d * j) from h1
  obtain (k : Nat) (h5 : b = d * k) from h2
  define    --Goal : ∃ (c : Nat), a % b = d * c
  apply Exists.intro (j - k * q)
  show a % b = d * (j - k * q) from
    calc a % b
      _ = b * q + a % b - b * q := (Nat.add_sub_cancel_left _ _).symm
      _ = a - b * q := by rw [h3]
      _ = d * j - d * (k * q) := by rw [h4, h5, mul_assoc]
      _ = d * (j - k * q) := (Nat.mul_sub_left_distrib _ _ _).symm
  done

theorem dvd_a_of_dvd_b_mod {a b d : Nat}
    (h1 : d ∣ b) (h2 : d ∣ (a % b)) : d ∣ a := sorry

These theorems tell us that the gcd of a and b is the same as the gcd of b and a % b, which suggests that the following recursive definition should compute the gcd of a and b:

def **gcd:: (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 => gcd (n + 1) (a % (n + 1))

Unfortunately, Lean puts a red squiggle under gcd, and it displays in the Infoview a long error message that begins fail to show termination. What is Lean complaining about?

The problem is that recursive definitions are dangerous. To understand the danger, consider the following recursive definition:

def loop (n : Nat) : Nat := loop (n + 1)

Suppose we try to use this definition to compute loop 3. The definition would lead us to perform the following calculation:

loop 3 = loop 4 = loop 5 = loop 6 = ...

Clearly this calculation will go on forever and will never produce an answer. So the definition of loop does not actually succeed in defining a function from Nat to Nat.

Lean insists that recursive definitions must avoid such nonterminating calculations. Why did it accept all of our previous recursive definitions? The reason is that in each case, the definition of the value of the function at a natural number n referred only to values of the function at numbers smaller than n. Since a decreasing list of natural numbers cannot go on forever, such definitions lead to calculations that are guaranteed to terminate.

What about our recursive definition of gcd a b? This function has two arguments, a and b, and when b = n + 1, the definition asks us to compute gcd (n + 1) (a % (n + 1)). The first argument here could actually be larger than the first argument in the value we are trying to compute, gcd a b. But the second argument will always be smaller, and that will suffice to guarantee that the calculation terminates. We can tell Lean to focus on the second argument by adding a termination_by clause to the end of our recursive definition:

def gcd (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 => **gcd (n + 1) (a % (n + 1))::
  termination_by gcd a b => b

Unfortunately, Lean still isn’t satisfied, but the error message this time is more helpful. The message says that Lean failed to prove termination, and at the end of the message it says that the goal it failed to prove is a % (n + 1) < Nat.succ n. Here Nat.succ n denotes the successor of n—that is, n + 1—so Lean was trying to prove that a % (n + 1) < n + 1, which is precisely what is needed to show that the second argument of gcd (n + 1) (a % (n + 1)) is smaller than the second argument of gcd a b when b = n + 1. We’ll need to provide a proof of this goal to convince Lean to accept our recursive definition. Fortunately, it’s not hard to prove:

lemma mod_succ_lt (a n : Nat) : a % (n + 1) < n + 1 := by
  have h : n + 1 > 0 := Nat.succ_pos n
  show a % (n + 1) < n + 1 from Nat.mod_lt a h
  done

Lean’s error message suggests several ways to fix the problem with our recursive definition. We’ll use the first suggestion: Use `have` expressions to prove the remaining goals. Here, finally, is the definition of gcd that Lean is willing to accept:

def gcd (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 =>
      have : a % (n + 1) < n + 1 := mod_succ_lt a n
      gcd (n + 1) (a % (n + 1))
  termination_by gcd a b => b

Notice that in the have expression, we have not bothered to specify an identifier for the assertion being proven, since we never need to refer to it. Let’s try out our gcd function:

++#eval:: gcd 672 161    --Answer: 7.  Note 672 = 7 * 96 and 161 = 7 * 23.

To establish the main properties of gcd a b we’ll need several lemmas. We prove some of them and leave others as exercises.

lemma gcd_base (a : Nat) : gcd a 0 = a := by rfl

lemma gcd_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :
    gcd a b = gcd b (a % b) := by
  obtain (n : Nat) (h2 : b = n + 1) from exists_eq_add_one_of_ne_zero h
  rewrite [h2]   --Goal : gcd a (n + 1) = gcd (n + 1) (a % (n + 1))
  rfl
  done

lemma mod_nonzero_lt (a : Nat) {b : Nat} (h : b ≠ 0) : a % b < b := sorry

lemma dvd_self (n : Nat) : n ∣ n := sorry

One of the most important properties of gcd a b is that it divides both a and b. We prove it by strong induction on b.

theorem gcd_dvd : ∀ (b a : Nat), (gcd a b) ∣ a ∧ (gcd a b) ∣ b := by
  by_strong_induc
  fix b : Nat
  assume ih : ∀ b_1 < b, ∀ (a : Nat), (gcd a b_1) ∣ a ∧ (gcd a b_1) ∣ b_1
  fix a : Nat
  by_cases h1 : b = 0
  · -- Case 1. h1 : b = 0
    rewrite [h1, gcd_base]   --Goal: a ∣ a ∧ a ∣ 0
    apply And.intro (dvd_self a)
    define
    apply Exists.intro 0
    rfl
    done
  · -- Case 2. h1 : b ≠ 0
    rewrite [gcd_nonzero a h1]
      --Goal : gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
    have h2 : a % b < b := mod_nonzero_lt a h1
    have h3 : (gcd b (a % b)) ∣ b ∧ (gcd b (a % b)) ∣ (a % b) :=
      ih (a % b) h2 b
    apply And.intro _ h3.left
    show (gcd b (a % b)) ∣ a from dvd_a_of_dvd_b_mod h3.left h3.right
    done
  done

You may wonder why we didn’t start the proof like this:

theorem gcd_dvd : ∀ (a b : Nat), (gcd a b) ∣ a ∧ (gcd a b) ∣ b := by
  fix a : Nat
  by_strong_induc
  fix b : Nat
  assume ih : ∀ b_1 < b, (gcd a b_1) ∣ a ∧ (gcd a b_1) ∣ b_1

In fact, this approach wouldn’t have worked. It is an interesting exercise to try to complete this version of the proof and see why it fails.

Another interesting question is why we asserted both (gcd a b) ∣ a and (gcd a b) ∣ b in the same theorem. Wouldn’t it have been easier to give separate proofs of the statements ∀ (b a : Nat), (gcd a b) ∣ a and ∀ (b a : Nat), (gcd a b) ∣ b? Again, you might find it enlightening to see why that wouldn’t have worked. However, now that we have proven both divisibility statements, we can state them as separate theorems:

theorem gcd_dvd_left (a b : Nat) : (gcd a b) ∣ a := (gcd_dvd b a).left

theorem gcd_dvd_right (a b : Nat) : (gcd a b) ∣ b := (gcd_dvd b a).right

Next we turn to Theorem 7.1.4 in HTPI, which says that there are integers \(s\) and \(t\) such that \(\text{gcd}(a, b) = s a + t b\). (We say that \(\text{gcd}(a, b)\) can be written as a linear combination of \(a\) and \(b\).) In HTPI, this is proven by using an extended version of the Euclidean algorithm to compute the coefficients \(s\) and \(t\). Here we will use a different recursive procedure to compute \(s\) and \(t\). If \(b = 0\), then \(\text{gcd}(a, b) = a = 1 \cdot a + 0 \cdot b\), so we can use the values \(s = 1\) and \(t = 0\). Otherwise, let \(q\) and \(r\) be the quotient and remainder when \(a\) is divided by \(b\). Then \(a = bq + r\) and \(\text{gcd}(a, b) = \text{gcd}(b, r)\). Now suppose that we have already computed integers \(s'\) and \(t'\) such that \[ \text{gcd}(b, r) = s' b + t' r. \] Then \[\begin{align*} \text{gcd}(a, b) &= \text{gcd}(b, r) = s' b + t' r\\ &= s' b + t' (a - bq) = t' a + (s' - t'q)b. \end{align*}\] Thus, to write \(\text{gcd}(a, b) = s a + t b\) we can use the values \[\begin{equation}\tag{$*$} s = t', \qquad t = s' - t'q. \end{equation}\]

We will use these equations as the basis for recursive definitions of Lean functions gcd_c1 and gcd_c2 such that the required coefficients can be obtained from the formulas s = gcd_c1 a b and t = gcd_c2 a b. Notice that s and t could be negative, so they must have type Int, not Nat. As a result, in definitions and theorems involving gcd_c1 and gcd_c2 we will sometimes have to deal with coercion of natural numbers to integers.

The functions gcd_c1 and gcd_c2 will be mutually recursive; in other words, each will be defined not only in terms of itself but also in terms of the other. Fortunately, Lean allows for such mutual recursion. Here are the definitions we will use.

mutual
  def gcd_c1 (a b : Nat) : Int :=
    match b with
      | 0 => 1
      | n + 1 => 
        have : a % (n + 1) < n + 1 := mod_succ_lt a n
        gcd_c2 (n + 1) (a % (n + 1))
          --Corresponds to s = t' in (*)

  def gcd_c2 (a b : Nat) : Int :=
    match b with
      | 0 => 0
      | n + 1 =>
        have : a % (n + 1) < n + 1 := mod_succ_lt a n
        gcd_c1 (n + 1) (a % (n + 1)) -
          (gcd_c2 (n + 1) (a % (n + 1))) * ↑(a / (n + 1))
          --Corresponds to t = s' - t'q in (*)
end
  termination_by
    gcd_c1 a b => b
    gcd_c2 a b => b

Notice that in the definition of gcd_c2, the quotient a / (n + 1) is computed using natural-number division, but it is then coerced to be an integer so that it can be multiplied by the integer gcd_c2 (n + 1) (a % (n + 1)).

Our main theorem about these functions is that they give the coefficients needed to write gcd a b as a linear combination of a and b. As usual, stating a few lemmas first helps with the proof. We leave the proofs of two of them as exercises for you (hint: imitate the proof of gcd_nonzero above).

lemma gcd_c1_base (a : Nat) : gcd_c1 a 0 = 1 := by rfl

lemma gcd_c1_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :
    gcd_c1 a b = gcd_c2 b (a % b) := sorry

lemma gcd_c2_base (a : Nat) : gcd_c2 a 0 = 0 := by rfl

lemma gcd_c2_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :
    gcd_c2 a b = gcd_c1 b (a % b) - (gcd_c2 b (a % b)) * ↑(a / b) := sorry

With that preparation, we are ready to prove that gcd_c1 a b and gcd_c2 a b give coefficients for expressing gcd a b as a linear combination of a and b. Of course, the theorem is proven by strong induction. For clarity, we’ll write the coercions explicitly in this proof. We’ll make a few comments after the proof that may help you follow the details.

theorem gcd_lin_comb : ∀ (b a : Nat),
    (gcd_c1 a b) * ↑a + (gcd_c2 a b) * ↑b = ↑(gcd a b) := by
  by_strong_induc
  fix b : Nat
  assume ih : ∀ b_1 < b, ∀ (a : Nat),
    (gcd_c1 a b_1) * ↑a + (gcd_c2 a b_1) * ↑b_1 = ↑(gcd a b_1)
  fix a : Nat
  by_cases h1 : b = 0
  · -- Case 1. h1 : b = 0
    rewrite [h1, gcd_c1_base, gcd_c2_base, gcd_base]
      --Goal : 1 * ↑a + 0 * ↑0 = ↑a
    ring
    done
  · -- Case 2. h1 : b ≠ 0
    rewrite [gcd_c1_nonzero a h1, gcd_c2_nonzero a h1, gcd_nonzero a h1]
      --Goal : gcd_c2 b (a % b) * ↑a +
      -- (gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)) * ↑b =
      -- ↑(gcd b (a % b))
    set r : Nat := a % b
    set q : Nat := a / b
    set s : Int := gcd_c1 b r
    set t : Int := gcd_c2 b r
      --Goal : t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
    have h2 : r < b := mod_nonzero_lt a h1
    have h3 : s * ↑b + t * ↑r = ↑(gcd b r) := ih r h2 b
    have h4 : b * q + r = a := Nat.div_add_mod a b
    rewrite [←h3, ←h4]
    rewrite [Nat.cast_add, Nat.cast_mul]
      --Goal : t * (↑b * ↑q + ↑r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r
    ring
    done
  done

In case 2, we have introduced the variables r, q, s, and t to simplify the notation. Notice that the set tactic automatically plugs in this notation in the goal. After the step rewrite [←h3, ←h4], the goal contains the expression ↑(b * q + r). You can use the #check command to see why Nat.cast_add and Nat.cast_mul convert this expression to first ↑(b * q) + ↑r and then ↑b * ↑q + ↑r. Without those steps, the ring tactic would not have been able to complete the proof.

We can try out the functions gcd_c1 and gcd_c2 as follows:

++#eval:: gcd_c1 672 161  --Answer: 6
++#eval:: gcd_c2 672 161  --Answer: -25
  --Note 6 * 672 - 25 * 161 = 4032 - 4025 = 7 = gcd 672 161

Finally, we turn to Theorem 7.1.6 in HTPI, which expresses one of the senses in which gcd a b is the greatest common divisor of a and b. Our proof follows the strategy of the proof in HTPI, with one additional step: we begin by using the theorem Int.coe_nat_dvd to change the goal from d ∣ gcd a b to ↑d ∣ ↑(gcd a b) (where the coercions are from Nat to Int), so that the rest of the proof can work with integer algebra rather than natural-number algebra.

theorem Theorem_7_1_6 {d a b : Nat} (h1 : d ∣ a) (h2 : d ∣ b) :
    d ∣ gcd a b := by
  rewrite [←Int.coe_nat_dvd]    --Goal : ↑d ∣ ↑(gcd a b)
  set s : Int := gcd_c1 a b
  set t : Int := gcd_c2 a b
  have h3 : s * ↑a + t * ↑b = ↑(gcd a b) := gcd_lin_comb b a
  rewrite [←h3]                 --Goal : ↑d ∣ s * ↑a + t * ↑b
  obtain (j : Nat) (h4 : a = d * j) from h1
  obtain (k : Nat) (h5 : b = d * k) from h2
  rewrite [h4, h5, Nat.cast_mul, Nat.cast_mul]
    --Goal : ↑d ∣ s * (↑d * ↑j) + t * (↑d * ↑k)
  define
  apply Exists.intro (s * ↑j + t * ↑k)
  ring
  done

We will ask you in the exercises to prove that, among the common divisors of a and b, gcd a b is the greatest with respect to the usual ordering of the natural numbers (as long as gcd a b ≠ 0).

Exercises

theorem dvd_a_of_dvd_b_mod {a b d : Nat}
    (h1 : d ∣ b) (h2 : d ∣ (a % b)) : d ∣ a := sorry

lemma gcd_comm_lt {a b : Nat} (h : a < b) : gcd a b = gcd b a := sorry

theorem gcd_comm (a b : Nat) : gcd a b = gcd b a := sorry

theorem Exercise_7_1_5 (a b : Nat) (n : Int) :
    (∃ (s t : Int), s * a + t * b = n) ↔ (↑(gcd a b) : Int) ∣ n := sorry

theorem Exercise_7_1_6 (a b c : Nat) :
    gcd a b = gcd (a + b * c) b := sorry

theorem gcd_is_nonzero {a b : Nat} (h : a ≠ 0 ∨ b ≠ 0) :
    gcd a b ≠ 0 := sorry

theorem gcd_greatest {a b d : Nat} (h1 : gcd a b ≠ 0)
    (h2 : d ∣ a) (h3 : d ∣ b) : d ≤ gcd a b := sorry

lemma Lemma_7_1_10a {a b : Nat}
    (n : Nat) (h : a ∣ b) : (n * a) ∣ (n * b) := sorry

lemma Lemma_7_1_10b {a b n : Nat}
    (h1 : n ≠ 0) (h2 : (n * a) ∣ (n * b)) : a ∣ b := sorry

lemma Lemma_7_1_10c {a b : Nat}
    (h1 : a ∣ b) (h2 : b ∣ a) : a = b := sorry

theorem Exercise_7_1_10 (a b n : Nat) :
    gcd (n * a) (n * b) = n * gcd a b := sorry

7.2. Prime Factorization

A natural number \(n\) is said to be prime if it is at least 2 and it cannot be written as a product of two smaller natural numbers. Of course, we can write this definition in Lean.

def prime (n : Nat) : Prop :=
  2 ≤ n ∧ ¬∃ (a b : Nat), a * b = n ∧ a < n ∧ b < n

The main goal of Section 7.2 of HTPI is to prove that every positive integer has a unique prime factorization; that is, it can be written in a unique way as the product of a nondecreasing list of prime numbers. To get started on this goal, we first prove that every number greater than or equal to 2 has a prime factor. We leave one lemma as an exercise for you (it is a natural-number version of Theorem_3_3_7).

def prime_factor (p n : Nat) : Prop := prime p ∧ p ∣ n

lemma dvd_trans {a b c : Nat} (h1 : a ∣ b) (h2 : b ∣ c) : a ∣ c := sorry

lemma exists_prime_factor : ∀ (n : Nat), 2 ≤ n →
    ∃ (p : Nat), prime_factor p n := by
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ (p : Nat), prime_factor p n_1
  assume h1 : 2 ≤ n
  by_cases h2 : prime n
  · -- Case 1. h2 : prime n
    apply Exists.intro n
    define            --Goal : prime n ∧ n ∣ n
    show prime n ∧ n ∣ n from And.intro h2 (dvd_self n)
    done
  · -- Case 2. h2 : ¬prime n
    define at h2
      --h2 : ¬(2 ≤ n ∧ ¬∃ (a b : Nat), a * b = n ∧ a < n ∧ b < n)
    demorgan at h2
    disj_syll h2 h1
    obtain (a : Nat) (h3 : ∃ (b : Nat), a * b = n ∧ a < n ∧ b < n) from h2
    obtain (b : Nat) (h4 : a * b = n ∧ a < n ∧ b < n) from h3
    have h5 : 2 ≤ a := by
      by_contra h6
      have h7 : a ≤ 1 := by linarith
      have h8 : n ≤ b :=
        calc n
          _ = a * b := h4.left.symm
          _ ≤ 1 * b := by rel [h7]
          _ = b := by ring
      linarith        --n ≤ b contradicts b < n
      done
    have h6 : ∃ (p : Nat), prime_factor p a := ih a h4.right.left h5
    obtain (p : Nat) (h7 : prime_factor p a) from h6
    apply Exists.intro p
    define            --Goal : prime p ∧ p ∣ n
    define at h7      --h7 : prime p ∧ p ∣ a
    apply And.intro h7.left
    have h8 : a ∣ n := by
      apply Exists.intro b
      show n = a * b from (h4.left).symm
      done
    show p ∣ n from dvd_trans h7.right h8
    done
  done

Of course, by the well ordering principle, an immediate consequence of this lemma is that every number greater than or equal to 2 has a smallest prime factor.

lemma exists_least_prime_factor {n : Nat} (h : 2 ≤ n) :
    ∃ (p : Nat), prime_factor p n ∧
    ∀ (q : Nat), prime_factor q n → p ≤ q := by
  set S : Set Nat := {p : Nat | prime_factor p n}
  have h2 : ∃ (p : Nat), p ∈ S := exists_prime_factor n h
  show ∃ (p : Nat), prime_factor p n ∧
    ∀ (q : Nat), prime_factor q n → p ≤ q from well_ord_princ S h2
  done

To talk about prime factorizations of positive integers, we’ll need to introduce a new type. If U is any type, then List U is the type of lists of objects of type U. Such a list is written in square brackets, with the entries separated by commas. For example, [3, 7, 1] has type List Nat. The notation [] denotes the empty list, and if a has type U and l has type List U, then a :: l denotes the list consisting of a followed by the entries of l. The empty list is sometimes called the nil list, and the operation of constructing a list a :: l from a and l is called cons (short for construct). Every list can be constructed by applying the cons operation repeatedly, starting with the nil list. For example,

[3, 7, 1] = 3 :: [7, 1] = 3 :: (7 :: [1]) = 3 :: (7 :: (1 :: [])).

If l has type List U and a has type U, then a ∈ l means that a is one of the entries in the list l. For example, 7 ∈ [3, 7, 1]. Lean knows several theorems about this notation:

@List.not_mem_nil : ∀ {α : Type u_1} (a : α),
                        a ∉ []

@List.mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α},
                        a ∈ b :: l ↔ a = b ∨ a ∈ l

@List.mem_cons_self : ∀ {α : Type u_1} (a : α) (l : List α),
                        a ∈ a :: l

@List.mem_cons_of_mem : ∀ {α : Type u_1} (y : α) {a : α} {l : List α},
                        a ∈ l → a ∈ y :: l

The first two theorems give the conditions under which something is a member of the nil list or a list constructed by cons, and the last two are easy consequences of the second.

To define prime factorizations, we must define several concepts first. Some of these concepts are most easily defined recursively.

def all_prime (l : List Nat) : Prop := ∀ p ∈ l, prime p

def nondec (l : List Nat) : Prop :=
  match l with
    | [] => True   --Of course, True is a proposition that is always true
    | n :: L => (∀ m ∈ L, n ≤ m) ∧ nondec L

def nondec_prime_list (l : List Nat) : Prop := all_prime l ∧ nondec l

def prod (l : List Nat) : Nat :=
  match l with
    | [] => 1
    | n :: L => n * (prod L)

def prime_factorization (n : Nat) (l : List Nat) : Prop :=
  nondec_prime_list l ∧ prod l = n

According to these definitions, all_prime l means that every member of the list l is prime, nondec l means that every member of l is less than or equal to all later members, prod l is the product of all members of l, and prime_factorization n l means that l is a nondecreasing list of prime numbers whose product is n. It will be convenient to spell out some consequences of these definitions in several lemmas:

lemma all_prime_nil : all_prime [] := by
  define     --Goal : ∀ p ∈ [], prime p
  fix p : Nat
  contrapos  --Goal : ¬prime p → p ∉ []
  assume h1 : ¬prime p
  show p ∉ [] from List.not_mem_nil p
  done

lemma all_prime_cons (n : Nat) (L : List Nat) :
    all_prime (n :: L) ↔ prime n ∧ all_prime L := by
  apply Iff.intro
  · -- (→)
    assume h1 : all_prime (n :: L)  --Goal : prime n ∧ all_prime L
    define at h1  --h1 : ∀ p ∈ n :: L, prime p
    apply And.intro (h1 n (List.mem_cons_self n L))
    define        --Goal : ∀ p ∈ L, prime p
    fix p : Nat
    assume h2 : p ∈ L
    show prime p from h1 p (List.mem_cons_of_mem n h2)
    done
  · -- (←)
    assume h1 : prime n ∧ all_prime L  --Goal : all_prime (n :: l)
    define : all_prime L at h1
    define
    fix p : Nat
    assume h2 : p ∈ n :: L
    rewrite [List.mem_cons] at h2   --h2 : p = n ∨ p ∈ L
    by_cases on h2
    · -- Case 1. h2 : p = n
      rewrite [h2]
      show prime n from h1.left
      done
    · -- Case 2. h2 : p ∈ L
      show prime p from h1.right p h2
      done
    done
  done

lemma nondec_nil : nondec [] := by
  define  --Goal : True
  trivial --trivial proves some obviously true statements, such as True
  done

lemma nondec_cons (n : Nat) (L : List Nat) :
    nondec (n :: L) ↔ (∀ m ∈ L, n ≤ m) ∧ nondec L := by rfl

lemma prod_nil : prod [] = 1 := by rfl

lemma prod_cons : prod (n :: L) = n * (prod L) := by rfl

Before we can prove the existence of prime factorizations, we will need one more fact: every member of a list of natural numbers divides the product of the list. The proof will be by induction on the length of the list, so we will need to know how to work with lengths of lists in Lean. If l is a list, then the length of l is List.length l, which can also be written more briefly as l.length. We’ll need a few more theorems about lists:

@List.length_eq_zero : ∀ {α : Type u_1} {l : List α},
                      List.length l = 0 ↔ l = []

@List.length_cons : ∀ {α : Type u_1} (a : α) (as : List α),
                      List.length (a :: as) = Nat.succ (List.length as)

@List.exists_cons_of_ne_nil : ∀ {α : Type u_1} {l : List α},
                      l ≠ [] → ∃ (b : α), ∃ (L : List α), l = b :: L

And we’ll need one more lemma, which follows from the three theorems above; we leave the proof as an exercise for you:

lemma exists_cons_of_length_eq_succ {A : Type}
    {l : List A} {n : Nat} (h : l.length = n + 1) :
    ∃ (a : A) (L : List A), l = a :: L ∧ L.length = n := sorry

We can now prove that every member of a list of natural numbers divides the product of the list. After proving it by induction on the length of the list, we restate the lemma in a more convenient form.

lemma list_elt_dvd_prod_by_length (a : Nat) : ∀ (n : Nat),
    ∀ (l : List Nat), l.length = n → a ∈ l → a ∣ prod l := by
  by_induc
  · --Base Case
    fix l : List Nat
    assume h1 : l.length = 0
    rewrite [List.length_eq_zero] at h1     --h1 : l = []
    rewrite [h1]                            --Goal : a ∈ [] → a ∣ prod []
    contrapos
    assume h2 : ¬a ∣ prod []
    show a ∉ [] from List.not_mem_nil a
    done
  · -- Induction Step
    fix n : Nat
    assume ih : ∀ (l : List Nat), List.length l = n → a ∈ l → a ∣ prod l
    fix l : List Nat
    assume h1 : l.length = n + 1            --Goal : a ∈ l → a ∣ prod l
    obtain (b : Nat) (h2 : ∃ (L : List Nat),
      l = b :: L ∧ L.length = n) from exists_cons_of_length_eq_succ h1
    obtain (L : List Nat) (h3 : l = b :: L ∧ L.length = n) from h2
    have h4 : a ∈ L → a ∣ prod L := ih L h3.right
    assume h5 : a ∈ l
    rewrite [h3.left, prod_cons]            --Goal : a ∣ b * prod L
    rewrite [h3.left, List.mem_cons] at h5  --h5 : a = b ∨ a ∈ L
    by_cases on h5
    · -- Case 1. h5 : a = b
      apply Exists.intro (prod L)
      rewrite [h5]
      rfl
      done
    · -- Case 2. h5 : a ∈ L
      have h6 : a ∣ prod L := h4 h5
      have h7 : prod L ∣ b * prod L := by
        apply Exists.intro b
        ring
        done
      show a ∣ b * prod L from dvd_trans h6 h7
      done
    done
  done

lemma list_elt_dvd_prod {a : Nat} {l : List Nat}
    (h : a ∈ l) : a ∣ prod l := by
  set n : Nat := l.length
  have h1 : l.length = n := by rfl
  show a ∣ prod l from list_elt_dvd_prod_by_length a n l h1 h
  done

The proof that every positive integer has a prime factorization is now long but straightforward.

lemma exists_prime_factorization : ∀ (n : Nat), n ≥ 1 →
    ∃ (l : List Nat), prime_factorization n l := by
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, n_1 ≥ 1 →
    ∃ (l : List Nat), prime_factorization n_1 l
  assume h1 : n ≥ 1
  by_cases h2 : n = 1
  · -- Case 1. h2 : n = 1
    apply Exists.intro []
    define
    apply And.intro
    · -- Proof of nondec_prime_list []
      define
      show all_prime [] ∧ nondec [] from
        And.intro all_prime_nil nondec_nil
      done
    · -- Proof of prod [] = n
      rewrite [prod_nil, h2]
      rfl
      done
    done
  · -- Case 2. h2 : n ≠ 1
    have h3 : n ≥ 2 := lt_of_le_of_ne' h1 h2
    obtain (p : Nat) (h4 : prime_factor p n ∧ ∀ (q : Nat),
      prime_factor q n → p ≤ q) from exists_least_prime_factor h3
    have p_prime_factor : prime_factor p n := h4.left
    define at p_prime_factor
    have p_prime : prime p := p_prime_factor.left
    have p_dvd_n : p ∣ n := p_prime_factor.right
    have p_least : ∀ (q : Nat), prime_factor q n → p ≤ q := h4.right
    obtain (m : Nat) (n_eq_pm : n = p * m) from p_dvd_n
    have h5 : m ≠ 0 := by
      contradict h1 with h6
      have h7 : n = 0 :=
        calc n
          _ = p * m := n_eq_pm
          _ = p * 0 := by rw [h6]
          _ = 0 := by ring
      rewrite [h7]
      decide
      done
    have m_pos : 0 < m := Nat.pos_of_ne_zero h5
    have m_lt_n : m < n := by
      define at p_prime
      show m < n from
        calc m
          _ < m + m := by linarith
          _ = 2 * m := by ring
          _ ≤ p * m := by rel [p_prime.left]
          _ = n := n_eq_pm.symm
      done
    obtain (L : List Nat) (h6 : prime_factorization m L)
      from ih m m_lt_n m_pos
    define at h6
    have ndpl_L : nondec_prime_list L := h6.left
    define at ndpl_L
    apply Exists.intro (p :: L)
    define
    apply And.intro
    · -- Proof of nondec_prime_list (p :: L)
      define
      apply And.intro
      · -- Proof of all_prime (p :: L)
        rewrite [all_prime_cons]
        show prime p ∧ all_prime L from And.intro p_prime ndpl_L.left
        done
      · -- Proof of nondec (p :: L)
        rewrite [nondec_cons]
        apply And.intro _ ndpl_L.right
        fix q : Nat
        assume q_in_L : q ∈ L
        have h7 : q ∣ prod L := list_elt_dvd_prod q_in_L
        rewrite [h6.right] at h7   --h7 : q ∣ m
        have h8 : m ∣ n := by
          apply Exists.intro p
          rewrite [n_eq_pm]
          ring
          done
        have q_dvd_n : q ∣ n := dvd_trans h7 h8
        have ap_L : all_prime L := ndpl_L.left
        define at ap_L
        have q_prime_factor : prime_factor q n :=
          And.intro (ap_L q q_in_L) q_dvd_n
        show p ≤ q from p_least q q_prime_factor
        done
      done
    · -- Proof of prod (p :: L) = n
      rewrite [prod_cons, h6.right, n_eq_pm]
      rfl
      done
    done
  done

We now turn to the proof that the prime factorization of a positive integer is unique. In preparation for that proof, HTPI defines two numbers to be relatively prime if their greatest common divisor is 1, and then it uses that concept to prove two theorems, 7.2.2 and 7.2.3. Here are similar proofs of those theorems in Lean, with the proof of one lemma left as an exercise. In the proof of Theorem 7.2.2, we begin, as we did in the proof of Theorem 7.1.6, by converting the goal from natural numbers to integers so that we can use integer algebra.

def rel_prime (a b : Nat) : Prop := gcd a b = 1

theorem Theorem_7_2_2 {a b c : Nat}
    (h1 : c ∣ a * b) (h2 : rel_prime a c) : c ∣ b := by
  rewrite [←Int.coe_nat_dvd]  --Goal : ↑c ∣ ↑b
  define at h1; define at h2; define
  obtain (j : Nat) (h3 : a * b = c * j) from h1
  set s : Int := gcd_c1 a c
  set t : Int := gcd_c2 a c
  have h4 : s * ↑a + t * ↑c = ↑(gcd a c) := gcd_lin_comb c a
  rewrite [h2, Nat.cast_one] at h4  --h4 : s * ↑a + t * ↑c = (1 : Int)
  apply Exists.intro (s * ↑j + t * ↑b)
  show ↑b = ↑c * (s * ↑j + t * ↑b) from
    calc ↑b
      _ = (1 : Int) * ↑b := (one_mul _).symm
      _ = (s * ↑a + t * ↑c) * ↑b := by rw [h4]
      _ = s * (↑a * ↑b) + t * ↑c * ↑b := by ring
      _ = s * (↑c * ↑j) + t * ↑c * ↑b := by
            rw [←Nat.cast_mul a b, h3, Nat.cast_mul c j]
      _ = ↑c * (s * ↑j + t * ↑b) := by ring
  done

lemma dvd_prime {a p : Nat}
    (h1 : prime p) (h2 : a ∣ p) : a = 1 ∨ a = p := sorry

lemma rel_prime_of_prime_not_dvd {a p : Nat}
    (h1 : prime p) (h2 : ¬p ∣ a) : rel_prime a p := by
  have h3 : gcd a p ∣ a := gcd_dvd_left a p
  have h4 : gcd a p ∣ p := gcd_dvd_right a p
  have h5 : gcd a p = 1 ∨ gcd a p = p := dvd_prime h1 h4
  have h6 : gcd a p ≠ p := by
    contradict h2 with h6
    rewrite [h6] at h3
    show p ∣ a from h3
    done
  disj_syll h5 h6
  show rel_prime a p from h5
  done

theorem Theorem_7_2_3 {a b p : Nat}
    (h1 : prime p) (h2 : p ∣ a * b) : p ∣ a ∨ p ∣ b := by
  or_right with h3
  have h4 : rel_prime a p := rel_prime_of_prime_not_dvd h1 h3
  show p ∣ b from Theorem_7_2_2 h2 h4
  done

Theorem 7.2.4 in HTPI extends Theorem 7.2.3 to show that if a prime number divides the product of a list of natural numbers, then it divides one of the numbers in the list. (Theorem 7.2.3 is the case of a list of length two.) The proof in HTPI is by induction on the length of the list, and we could use that method to prove the theorem in Lean. But look back at our proof of the lemma list_elt_dvd_prod_by_length, which also used induction on the length of a list. In the base case, we ended up proving that the nil list has the property stated in the lemma, and in the induction step we proved that if a list L has the property, then so does any list of the form b :: L. We could think of this as a kind of “induction on lists.” As we observed earlier, every list can be constructed by starting with the nil list and applying cons finitely many times. It follows that if the nil list has some property, and applying the cons operation to a list with the property produces another list with the property, then all lists have the property. (In fact, a similar principle was at work in our recursive definitions of nondec l and prod l.)

Lean has a theorem called List.rec that can be used to justify induction on lists. This is a little more convenient than induction on the length of a list, so we’ll use it to prove Theorem 7.2.4. The proof uses two lemmas, whose proofs we leave as exercises for you.

lemma eq_one_of_dvd_one {n : Nat} (h : n ∣ 1) : n = 1 := sorry

lemma prime_not_one {p : Nat} (h : prime p) : p ≠ 1 := sorry

theorem Theorem_7_2_4 {p : Nat} (h1 : prime p) :
    ∀ (l : List Nat), p ∣ prod l → ∃ a ∈ l, p ∣ a := by
  apply List.rec
  · -- Base Case.  Goal : p ∣ prod [] → ∃ a ∈ [], p ∣ a
    rewrite [prod_nil]
    assume h2 : p ∣ 1
    show ∃ a ∈ [], p ∣ a from
      absurd (eq_one_of_dvd_one h2) (prime_not_one h1)
    done
  · -- Induction Step
    fix b : Nat
    fix L : List Nat
    assume ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
      --Goal : p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a
    assume h2 : p ∣ prod (b :: L)
    rewrite [prod_cons] at h2
    have h3 : p ∣ b ∨ p ∣ prod L := Theorem_7_2_3 h1 h2
    by_cases on h3
    · -- Case 1. h3 : p ∣ b
      apply Exists.intro b
      show b ∈ b :: L ∧ p ∣ b from
        And.intro (List.mem_cons_self b L) h3
      done
    · -- Case 2. h3 : p ∣ prod L
      obtain (a : Nat) (h4 : a ∈ L ∧ p ∣ a) from ih h3
      apply Exists.intro a
      show a ∈ b :: L ∧ p ∣ a from
        And.intro (List.mem_cons_of_mem b h4.left) h4.right
      done
    done
  done

In Theorem 7.2.4, if all members of the list l are prime, then we can conclude not merely that p divides some member of l, but that p is one of the members.

lemma prime_in_list {p : Nat} {l : List Nat}
    (h1 : prime p) (h2 : all_prime l) (h3 : p ∣ prod l) : p ∈ l := by
  obtain (a : Nat) (h4 : a ∈ l ∧ p ∣ a) from Theorem_7_2_4 h1 l h3
  define at h2
  have h5 : prime a := h2 a h4.left
  have h6 : p = 1 ∨ p = a := dvd_prime h5 h4.right
  disj_syll h6 (prime_not_one h1)
  rewrite [h6]
  show a ∈ l from h4.left
  done

The uniqueness of prime factorizations follows from Theorem 7.2.5 of HTPI, which says that if two nondecreasing lists of prime numbers have the same product, then the two lists must be the same. In HTPI, a key step in the proof of Theorem 7.2.5 is to show that if two nondecreasing lists of prime numbers have the same product, then the last entry of one list is less than or equal to the last entry of the other. In Lean, because of the way the cons operation works, it is easier to work with the first entries of the lists.

lemma first_le_first {p q : Nat} {l m : List Nat}
    (h1 : nondec_prime_list (p :: l)) (h2 : nondec_prime_list (q :: m))
    (h3 : prod (p :: l) = prod (q :: m)) : p ≤ q := by
  define at h1; define at h2
  have h4 : q ∣ prod (p :: l) := by
    define
    apply Exists.intro (prod m)
    rewrite [←prod_cons]
    show prod (p :: l) = prod (q :: m) from h3
    done
  have h5 : all_prime (q :: m) := h2.left
  rewrite [all_prime_cons] at h5
  have h6 : q ∈ p :: l := prime_in_list h5.left h1.left h4
  have h7 : nondec (p :: l) := h1.right
  rewrite [nondec_cons] at h7
  rewrite [List.mem_cons] at h6
  by_cases on h6
  · -- Case 1. h6 : q = p
    linarith
    done
  · -- Case 2. h6 : q ∈ l
    have h8 : ∀ m ∈ l, p ≤ m := h7.left
    show p ≤ q from h8 q h6
    done
  done

The proof of Theorem 7.2.5 is another proof by induction on lists. It uses a few more lemmas whose proofs we leave as exercises.

lemma nondec_prime_list_tail {p : Nat} {l : List Nat}
    (h : nondec_prime_list (p :: l)) : nondec_prime_list l := sorry

lemma cons_prod_not_one {p : Nat} {l : List Nat}
    (h : nondec_prime_list (p :: l)) : prod (p :: l) ≠ 1 := sorry

lemma list_nil_iff_prod_one {l : List Nat} (h : nondec_prime_list l) :
    l = [] ↔ prod l = 1 := sorry

lemma prime_pos {p : Nat} (h : prime p) : p > 0 := sorry

theorem Theorem_7_2_5 : ∀ (l1 l2 : List Nat),
    nondec_prime_list l1 → nondec_prime_list l2 →
    prod l1 = prod l2 → l1 = l2 := by
  apply List.rec
  · -- Base Case.  Goal : ∀ (l2 : List Nat), nondec_prime_list [] →
    -- nondec_prime_list l2 → prod [] = prod l2 → [] = l2
    fix l2 : List Nat
    assume h1 : nondec_prime_list []
    assume h2 : nondec_prime_list l2
    assume h3 : prod [] = prod l2
    rewrite [prod_nil, eq_comm, ←list_nil_iff_prod_one h2] at h3
    show [] = l2 from h3.symm
    done
  · -- Induction Step
    fix p : Nat
    fix L1 : List Nat
    assume ih : ∀ (L2 : List Nat), nondec_prime_list L1 →
      nondec_prime_list L2 → prod L1 = prod L2 → L1 = L2
    -- Goal : ∀ (l2 : List Nat), nondec_prime_list (p :: L1) →
    -- nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2
    fix l2 : List Nat
    assume h1 : nondec_prime_list (p :: L1)
    assume h2 : nondec_prime_list l2
    assume h3 : prod (p :: L1) = prod l2
    have h4 : ¬prod (p :: L1) = 1 := cons_prod_not_one h1
    rewrite [h3, ←list_nil_iff_prod_one h2] at h4
    obtain (q : Nat) (h5 : ∃ (L : List Nat), l2 = q :: L) from
      List.exists_cons_of_ne_nil h4
    obtain (L2 : List Nat) (h6 : l2 = q :: L2) from h5
    rewrite [h6] at h2    --h2 : nondec_prime_list (q :: L2)
    rewrite [h6] at h3    --h3 : prod (p :: L1) = prod (q :: L2)
    have h7 : p ≤ q := first_le_first h1 h2 h3
    have h8 : q ≤ p := first_le_first h2 h1 h3.symm
    have h9 : p = q := by linarith
    rewrite [h9, prod_cons, prod_cons] at h3
      --h3 : q * prod L1 = q * prod L2
    have h10 : nondec_prime_list L1 := nondec_prime_list_tail h1
    have h11 : nondec_prime_list L2 := nondec_prime_list_tail h2
    define at h2
    have h12 : all_prime (q :: L2) := h2.left
    rewrite [all_prime_cons] at h12
    have h13 : q > 0 := prime_pos h12.left
    have h14 : prod L1 = prod L2 := Nat.eq_of_mul_eq_mul_left h13 h3
    have h15 : L1 = L2 := ih L2 h10 h11 h14
    rewrite [h6, h9, h15]
    rfl
    done
  done

Putting it all together, we can finally prove the fundamental theorem of arithmetic, which is stated as Theorem 7.2.6 in HTPI:

theorem fund_thm_arith (n : Nat) (h : n ≥ 1) :
    ∃! (l : List Nat), prime_factorization n l := by
  exists_unique
  · -- Existence
    show ∃ (l : List Nat), prime_factorization n l from
      exists_prime_factorization n h
    done
  · -- Uniqueness
    fix l1 : List Nat; fix l2 : List Nat
    assume h1 : prime_factorization n l1
    assume h2 : prime_factorization n l2
    define at h1; define at h2
    have h3 : prod l1 = n := h1.right
    rewrite [←h2.right] at h3
    show l1 = l2 from Theorem_7_2_5 l1 l2 h1.left h2.left h3
    done
  done

Exercises

lemma dvd_prime {a p : Nat}
    (h1 : prime p) (h2 : a ∣ p) : a = 1 ∨ a = p := sorry

--Hints:  Start with apply List.rec.
--You may find the theorem mul_ne_zero useful.
theorem prod_nonzero_nonzero : ∀ (l : List Nat),
    (∀ a ∈ l, a ≠ 0) → prod l ≠ 0 := sorry

theorem rel_prime_iff_no_common_factor (a b : Nat) :
    rel_prime a b ↔ ¬∃ (p : Nat), prime p ∧ p ∣ a ∧ p ∣ b := sorry

theorem rel_prime_symm {a b : Nat} (h : rel_prime a b) :
    rel_prime b a := sorry

lemma in_prime_factorization_iff_prime_factor {a : Nat} {l : List Nat}
    (h1 : prime_factorization a l) (p : Nat) :
    p ∈ l ↔ prime_factor p a := sorry

theorem Exercise_7_2_5 {a b : Nat} {l m : List Nat}
    (h1 : prime_factorization a l) (h2 : prime_factorization b m) :
    rel_prime a b ↔ (¬∃ (p : Nat), p ∈ l ∧ p ∈ m) := sorry

theorem Exercise_7_2_6 (a b : Nat) :
    rel_prime a b ↔ ∃ (s t : Int), s * a + t * b = 1 := sorry

theorem Exercise_7_2_7 {a b a' b' : Nat}
    (h1 : rel_prime a b) (h2 : a' ∣ a) (h3 : b' ∣ b) :
    rel_prime a' b' := sorry

theorem Exercise_7_2_9 {a b j k : Nat}
    (h1 : gcd a b ≠ 0) (h2 : a = j * gcd a b) (h3 : b = k * gcd a b) :
    rel_prime j k := sorry

theorem Exercise_7_2_17a (a b c : Nat) :
    gcd a (b * c) ∣ gcd a b * gcd a c := sorry

7.3. Modular Arithmetic

If \(m\) is a positive integer and \(a\) and \(b\) are integers, then HTPI uses the notation \(a \equiv b\pmod m\), or sometimes \(a \equiv_m b\), to indicate that \(a\) is congruent to \(b\) modulo \(m\), which is defined to mean \(m \mid (a - b)\). Congruence modulo \(m\) is an equivalence relation on the integers, and therefore it induces a partition \(\mathbb{Z}/{\equiv_m}\) of the integers, as shown in Section 4.5 of HTPI. The elements of this partition are the equivalence classes \([a]_m\) for \(a \in \mathbb{Z}\); we will call these congruence classes modulo \(m\). Section 7.3 of HTPI defines operations of addition and multiplication of congruence classes and proves algebraic properties of those operations.

For the purpose of working out the rules of modular arithmetic, the only important properties of congruence classes are the following:

1. For every integer \(a\), there is a corresponding congruence class \([a]_m \in \mathbb{Z}/{\equiv_m}\).
2. For every congruence class \(X \in \mathbb{Z}/{\equiv_m}\), there is some integer \(a\) such that \(X = [a]_m\).
3. For all integers \(a\) and \(b\), \([a]_m = [b]_m\) if and only if \(a \equiv_m b\).
4. For all integers \(a\) and \(b\), \([a]_m + [b]_m = [a + b]_m\).
5. For all integers \(a\) and \(b\), \([a]_m \cdot [b]_m = [ab]_m\).

To study congruence modulo m in Lean, we will declare m to have type Nat, which allows for the possibility that m = 0, but we will mostly focus on the case m ≠ 0. For a and b of type Int, we define congr_mod m a b to mean that a is congruent to b modulo m. Notice that to define this relation in Lean, we must coerce m to be an integer so that we can use it in the divisibility relation on the integers.

def congr_mod (m : Nat) (a b : Int) : Prop := (↑m : Int) ∣ (a - b)

We can teach Lean to use more familiar notation for congruence modulo m by giving the following command:

notation:50 a " ≡ " b " (MOD " m ")" => congr_mod m a b

This tells Lean that if we type a ≡ b (MOD m), then Lean should interpret it as congr_mod m a b. (To enter the symbol ≡, type \==. Don’t worry about the :50 in the notation command above. It is there to help Lean parse this new notation when it occurs together with other notation.)

We can now prove that congruence modulo m is reflexive, symmetric, and transitive. In these proofs, we leave it to Lean to fill in coercions when they are necessary, and as usual, we leave some details as exercises.

theorem congr_refl (m : Nat) : ∀ (a : Int), a ≡ a (MOD m) := sorry

theorem congr_symm {m : Nat} : ∀ {a b : Int},
    a ≡ b (MOD m) → b ≡ a (MOD m) := by
  fix a : Int; fix b : Int
  assume h1 : a ≡ b (MOD m)
  define at h1                 --h1 : ∃ (c : Int), a - b = ↑m * c
  define                       --Goal : ∃ (c : Int), b - a = ↑m * c
  obtain (c : Int) (h2 : a - b = m * c) from h1
  apply Exists.intro (-c)
  show b - a = m * (-c) from
    calc b - a
      _ = -(a - b) := by ring
      _ = -(m * c) := by rw [h2]
      _ = m * (-c) := by ring
  done

theorem congr_trans {m : Nat} : ∀ {a b c : Int},
    a ≡ b (MOD m) → b ≡ c (MOD m) → a ≡ c (MOD m) := sorry

We could now repeat the entire development of \(\mathbb{Z}/{\equiv_m}\) in Lean, but there is no need to do so; such a development is already included in Lean’s library of definitions and theorems. For each natural number m, Lean has a type ZMod m, and the objects of that type are Lean’s version of the congruence classes modulo m. We should warn you that Lean’s way of defining ZMod m differs in some ways from HTPI’s definition of \(\mathbb{Z}/{\equiv_m}\). In particular, objects of type ZMod m are not sets of integers. Thus, if X has type ZMod m and a has type Int, then Lean will not understand what you mean if you write a ∈ X. However, Lean’s congruence classes have the properties 1–5 listed above, and that’s all that will matter to us.

Property 1 says that if a has type Int, then there should be a corresponding congruence class in ZMod m. In fact, you can find the corresponding congruence class by simply coercing a to have type ZMod m. But for the sake of clarity, we will introduce a function for computing the congruence class modulo m of a:

def cc (m : Nat) (a : Int) : ZMod m := (↑a : ZMod m)

Thus, cc m a is the congruence class modulo m of a. Once again, it will be convenient to teach Lean to use more familiar notation for congruence classes, so we give the command:

notation:max "["a"]_"m:max => cc m a

Now if we type [a]_m, then Lean will interpret it as cc m a. Thus, from now on, [a]_m will be our notation in Lean for the congruence class modulo m of a; it corresponds to the HTPI notation \([a]_m\). (Once again, you can ignore the two occurrences of :max in the notation command above.)

Properties 2–5 of congruence classes are established by the following theorems:

theorem cc_rep {m : Nat} (X : ZMod m) : ∃ (a : Int), X = [a]_m

theorem cc_eq_iff_congr (m : Nat) (a b : Int) :
    [a]_m = [b]_m ↔ a ≡ b (MOD m)

theorem add_class (m : Nat) (a b : Int) :
    [a]_m + [b]_m = [a + b]_m

theorem mul_class (m : Nat) (a b : Int) :
    [a]_m * [b]_m = [a * b]_m

We won’t discuss the proofs of these theorems, since they depend on details of Lean’s representation of objects of type ZMod m that are beyond the scope of this book. But these theorems are all we will need to use to develop the theory of modular arithmetic.

In many of our theorems about ZMod m, we will need to include a hypothesis that m ≠ 0. We will usually state this hypothesis in the form NeZero m, which is a proposition that is equivalent to m ≠ 0. Indeed, there is a theorem in Lean’s library that asserts this equivalence:

@neZero_iff : ∀ {R : Type u_1} [inst : Zero R] {n : R},
              NeZero n ↔ n ≠ 0

What distinguishes NeZero m from m ≠ 0 is that NeZero m is what is called a type class. What this means is that, once Lean has a proof of NeZero m for some natural number m, it will remember that proof and be able to recall it when necessary. As a result, NeZero m can be used as a new kind of implicit argument in the statement of a theorem. To make it an implicit argument, we write it in square brackets, like this: [NeZero m]. When applying a theorem that includes this hypothesis, there is no need to supply a proof that m ≠ 0; as long as Lean knows about such a proof, it will recall that proof on its own. When you are proving a theorem that includes the hypothesis [NeZero m], Lean will recognize NeZero.ne m as a proof that m ≠ 0.

The first theorem in Section 7.3 of HTPI, Theorem 7.3.1, says that if m ≠ 0, then every integer a is congruent modulo m to exactly one integer r satisfying 0 ≤ r < m. As explained in HTPI, we say that {0, 1, ..., m - 1} is a complete residue system modulo m. This implies that the objects of type ZMod m are precisely the congruence classes [0]_m, [1]_m, …, [m - 1]_m.

The proof of Theorem 7.3.1 makes use of the quotient and remainder when a is divided by m. In Section 6.4, we learned about the Lean theorems Nat.div_add_mod and Nat.mod_lt, but those theorems concerned quotients and remainders when dividing natural numbers. Fortunately, Lean has similar theorems for dealing with division of integers:

Int.ediv_add_emod : ∀ (a b : ℤ), b * (a / b) + a % b = a

Int.emod_lt_of_pos : ∀ (a : ℤ) {b : ℤ}, 0 < b → a % b < b

Int.emod_nonneg : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → 0 ≤ a % b

We now have all the background we need to prove Theorem 7.3.1 in Lean. We begin with a few lemmas, some of which require the hypothesis [NeZero m]. The proof of the theorem closely follows the proof in HTPI. Note that all of the proofs below involve the expression a % m. Since a is an integer, the operator % in this expression must be the integer version of the mod operator, and therefore m must be coerced to be an integer. Thus, Lean interprets a % m as a % ↑m

lemma mod_nonneg (m : Nat) [NeZero m] (a : Int) : 0 ≤ a % m := by
  have h1 : (↑m : Int) ≠ 0 := (Nat.cast_ne_zero).rtl (NeZero.ne m)
  show 0 ≤ a % m from Int.emod_nonneg a h1
  done

lemma mod_lt (m : Nat) [NeZero m] (a : Int) : a % m < m := sorry

lemma congr_mod_mod (m : Nat) (a : Int) : a ≡ a % m (MOD m) := by
  define
  have h1 : m * (a / m) + a % m = a := Int.ediv_add_emod a m
  apply Exists.intro (a / m)
  show a - a % m = m * (a / m) from
    calc a - (a % m)
      _ = m * (a / m) + a % m - a % m := by rw [h1]
      _ = m * (a / m) := by ring
  done

lemma mod_cmpl_res (m : Nat) [NeZero m] (a : Int) :
    0 ≤ a % m ∧ a % m < m ∧ a ≡ a % m (MOD m) :=
  And.intro (mod_nonneg m a) (And.intro (mod_lt m a) (congr_mod_mod m a))

theorem Theorem_7_3_1 (m : Nat) [NeZero m] (a : Int) :
    ∃! (r : Int), 0 ≤ r ∧ r < m ∧ a ≡ r (MOD m) := by
  exists_unique
  · -- Existence
    apply Exists.intro (a % m)
    show 0 ≤ a % m ∧ a % m < m ∧ a ≡ a % m (MOD m)
      from mod_cmpl_res m a
    done
  · -- Uniqueness
    fix r1 : Int; fix r2 : Int
    assume h1 : 0 ≤ r1 ∧ r1 < m ∧ a ≡ r1 (MOD m)
    assume h2 : 0 ≤ r2 ∧ r2 < m ∧ a ≡ r2 (MOD m)
    have h3 : r1 ≡ r2 (MOD m) :=
      congr_trans (congr_symm h1.right.right) h2.right.right
    obtain (d : Int) (h4 : r1 - r2 = m * d) from h3
    have h5 : r1 - r2 < m * 1 := by linarith
    have h6 : m * (-1) < r1 - r2 := by linarith
    rewrite [h4] at h5   --h5 : m * d < m * 1
    rewrite [h4] at h6   --h6 : m * -1 < m * d
    have h7 : (↑m : Int) ≥ 0 := Nat.cast_nonneg m
    have h8 : d < 1 := lt_of_mul_lt_mul_of_nonneg_left h5 h7
    have h9 : -1 < d := lt_of_mul_lt_mul_of_nonneg_left h6 h7
    have h10 : d = 0 := by linarith
    show r1 = r2 from
      calc r1
        _ = r1 - r2 + r2 := by ring
        _ = m * 0 + r2 := by rw [h4, h10]
        _ = r2 := by ring
    done
  done

The lemma mod_cmpl_res above says that a % m is an element of the complete residue system {0, 1, ..., m - 1} that is congruent to a modulo m. The lemma requires the hypothesis [NeZero m], because its proof appeals to two previous lemmas, mod_nonneg and mod_lt, that require that hypothesis. But when the proof invokes those previous lemmas, this hypothesis is not mentioned, because it is an implicit argument.

An immediate consequence of the lemma congr_mod_mod is the following lemma, which will be useful to us later.

lemma cc_eq_mod (m : Nat) (a : Int) : [a]_m = [a % m]_m := 
  (cc_eq_iff_congr m a (a % m)).rtl (congr_mod_mod m a)

Theorem 7.3.6 in HTPI states a number of algebraic properties of modular arithmetic. These properties all follow easily from the theorems we have already stated. To illustrate this, we prove two parts of the theorem.

theorem Theorem_7_3_6_1 {m : Nat} (X Y : ZMod m) : X + Y = Y + X := by
  obtain (a : Int) (h1 : X = [a]_m) from cc_rep X
  obtain (b : Int) (h2 : Y = [b]_m) from cc_rep Y
  rewrite [h1, h2]
  have h3 : a + b = b + a := by ring
  show [a]_m + [b]_m = [b]_m + [a]_m from
    calc [a]_m + [b]_m
      _ = [a + b]_m := add_class m a b
      _ = [b + a]_m := by rw [h3]
      _ = [b]_m + [a]_m := (add_class m b a).symm
  done

theorem Theorem_7_3_6_7 {m : Nat} (X : ZMod m) : X * [1]_m = X := by
  obtain (a : Int) (h1 : X = [a]_m) from cc_rep X
  rewrite [h1]
  have h2 : a * 1 = a := by ring
  show [a]_m * [1]_m = [a]_m from
    calc [a]_m * [1]_m
      _ = [a * 1]_m := mul_class m a 1
      _ = [a]_m := by rw [h2]
  done

Theorem_7_3_6_7 shows that [1]_m is the multiplicative identity element for ZMod m. We say that a congruence class Y is a multiplicative inverse of another class X if X * Y = [1]_m, and a congruence class is invertible if it has a multiplicative inverse:

def invertible {m : Nat} (X : ZMod m) : Prop :=
  ∃ (Y : ZMod m), X * Y = [1]_m

Which congruence classes are invertible? The answer is given by Theorem 7.3.7 in HTPI, which says that if \(a\) is a positive integer, then \([a]_m\) is invertible if and only if \(m\) and \(a\) are relatively prime. The proof uses an exercise from the last section. Here is the Lean version of the proof.

theorem Exercise_7_2_6 (a b : Nat) :
    rel_prime a b ↔ ∃ (s t : Int), s * a + t * b = 1 := sorry

lemma gcd_c2_inv {m a : Nat} (h1 : rel_prime m a) :
    [a]_m * [gcd_c2 m a]_m = [1]_m := by
  set s : Int := gcd_c1 m a
  have h2 : s * m + (gcd_c2 m a) * a = gcd m a := gcd_lin_comb a m
  define at h1
  rewrite [h1, Nat.cast_one] at h2  --h2 : s * ↑m + gcd_c2 m a * ↑a = 1
  rewrite [mul_class, cc_eq_iff_congr]
  define     --Goal : ∃ (c : Int), ↑a * gcd_c2 m a - 1 = ↑m * c
  apply Exists.intro (-s)
  show a * (gcd_c2 m a) - 1 = m * (-s) from
    calc a * (gcd_c2 m a) - 1
      _ = s * m + (gcd_c2 m a) * a + m * (-s) - 1 := by ring
      _ = 1 + m * (-s) - 1 := by rw [h2]
      _ = m * (-s) := by ring
  done

theorem Theorem_7_3_7 (m a : Nat) :
    invertible [a]_m ↔ rel_prime m a := by
  apply Iff.intro
  · -- (→)
    assume h1 : invertible [a]_m
    define at h1
    obtain (Y : ZMod m) (h2 : [a]_m * Y = [1]_m) from h1
    obtain (b : Int) (h3 : Y = [b]_m) from cc_rep Y
    rewrite [h3, mul_class, cc_eq_iff_congr] at h2
    define at h2
    obtain (c : Int) (h4 : a * b - 1 = m * c) from h2
    rewrite [Exercise_7_2_6]
      --Goal : ∃ (s t : Int), s * ↑m + t * ↑a = 1
    apply Exists.intro (-c)
    apply Exists.intro b
    show (-c) * m + b * a = 1 from
      calc (-c) * m + b * a
        _ = (-c) * m + (a * b - 1) + 1 := by ring
        _ = (-c) * m + m * c + 1 := by rw [h4]
        _ = 1 := by ring
    done
  · -- (←)
    assume h1 : rel_prime m a
    define
    show ∃ (Y : ZMod m), [a]_m * Y = [1]_m from
      Exists.intro [gcd_c2 m a]_m (gcd_c2_inv h1)
    done
  done

Exercises

theorem congr_trans {m : Nat} : ∀ {a b c : Int},
    a ≡ b (MOD m) → b ≡ c (MOD m) → a ≡ c (MOD m) := sorry

theorem Theorem_7_3_6_3 {m : Nat} (X : ZMod m) : X + [0]_m = X := sorry

theorem Theorem_7_3_6_4 {m : Nat} (X : ZMod m) :
    ∃ (Y : ZMod m), X + Y = [0]_m := sorry

theorem Exercise_7_3_4a {m : Nat} (Z1 Z2 : ZMod m)
    (h1 : ∀ (X : ZMod m), X + Z1 = X)
    (h2 : ∀ (X : ZMod m), X + Z2 = X) : Z1 = Z2 := sorry

theorem Exercise_7_3_4b {m : Nat} (X Y1 Y2 : ZMod m)
    (h1 : X + Y1 = [0]_m) (h2 : X + Y2 = [0]_m) : Y1 = Y2 := sorry

theorem Theorem_7_3_10 (m a : Nat) (b : Int) :
    ¬(↑(gcd m a) : Int) ∣ b → ¬∃ (x : Int), a * x ≡ b (MOD m) := sorry

theorem Theorem_7_3_11 (m n : Nat) (a b : Int) (h1 : n ≠ 0) :
    n * a ≡ n * b (MOD n * m) ↔ a ≡ b (MOD m) := sorry

theorem Exercise_7_3_16 {m : Nat} {a b : Int} (h : a ≡ b (MOD m)) :
    ∀ (n : Nat), a ^ n ≡ b ^ n (MOD m) := sorry

example {m : Nat} [NeZero m] (X : ZMod m) :
    ∃! (a : Int), 0 ≤ a ∧ a < m ∧ X = [a]_m := sorry

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

--Hint: You may find the theorem Int.ofNat_mod_ofNat useful.
theorem rel_prime_mod (m a : Nat) :
    rel_prime m (a % m) ↔ rel_prime m a := sorry

lemma congr_iff_mod_eq_Int (m : Nat) (a b : Int) [NeZero m] :
    a ≡ b (MOD m) ↔ a % ↑m = b % ↑m := sorry

--Hint for next theorem: Use the lemma above,
--together with the theorems Int.ofNat_mod_ofNat and Nat.cast_inj.
theorem congr_iff_mod_eq_Nat (m a b : Nat) [NeZero m] :
    ↑a ≡ ↑b (MOD m) ↔ a % m = b % m := sorry

7.4. Euler’s Theorem

The main result of Section 7.4 of HTPI is Euler’s theorem. The statement of the theorem involves Euler’s totient function \(\varphi\). For any positive integer \(m\), HTPI defines \(\varphi(m)\) to be the number of elements of \(\mathbb{Z}/{\equiv_m}\) that have multiplicative inverses. In order to state and prove Euler’s theorem in Lean, our first task is to define a Lean function phi : Nat → Nat that computes the totient function.

Since {0, 1, ..., m - 1} is a complete residue system modulo m, phi m can be described as the number of natural numbers a < m such that [a]_m is invertible. According to Theorem_7_3_7, [a]_m is invertible if and only if m and a are relatively prime, so phi m is also equal to the number of natural numbers a < m that are relatively prime to m. We begin by defining a function num_rp_below m k that counts the number of natural numbers less than k that are relatively prime to m.

def num_rp_below (m k : Nat) : Nat :=
  match k with
    | 0 => 0
    | j + 1 => if gcd m j = 1 then (num_rp_below m j) + 1
                else num_rp_below m j

This is the first time we have used an if ... then ... else expression in a Lean definition. To prove theorems about such expressions, we will need two theorems from Lean’s library, if_pos and if_neg. The #check command tells us what they say:

@if_pos : ∀ {c : Prop} {h : Decidable c},
          c → ∀ {α : Sort u_1} {t e : α}, (if c then t else e) = t
          
@if_neg : ∀ {c : Prop} {h : Decidable c},
          ¬c → ∀ {α : Sort u_1} {t e : α}, (if c then t else e) = e

Ignoring the implicit arguments, this tells us that if h is a proof of a proposition c, then if_pos h is a proof of (if c then t else e) = t, and if h is a proof of ¬c, then if_neg h is a proof of (if c then t else e) = e. (Technically, the implicit arguments say that c must be a “decidable” proposition, but we won’t worry about that detail.) We often use these theorems with the rewrite tactic to rewrite an expression of the form if c then t else e as either t or e, depending on whether c is true or false.

lemma num_rp_below_base {m : Nat} :
    num_rp_below m 0 = 0 := by rfl

lemma num_rp_below_step_rp {m j : Nat} (h : rel_prime m j) :
    num_rp_below m (j + 1) = (num_rp_below m j) + 1 := by
  have h1 : num_rp_below m (j + 1) =
    if gcd m j = 1 then (num_rp_below m j) + 1
    else num_rp_below m j := by rfl
  define at h     --h : gcd m j = 1
  rewrite [if_pos h] at h1
                  --h1 : num_rp_below m (j + 1) = num_rp_below m j + 1
  show num_rp_below m (j + 1) = num_rp_below m j + 1 from h1
  done

lemma num_rp_below_step_not_rp {m j : Nat} (h : ¬rel_prime m j) :
    num_rp_below m (j + 1) = num_rp_below m j := by
  have h1 : num_rp_below m (j +1) =
    if gcd m j = 1 then (num_rp_below m j) + 1
    else num_rp_below m j := by rfl
  define at h     --h : ¬gcd m j = 1
  rewrite [if_neg h] at h1
                  --h1 : num_rp_below m (j + 1) = num_rp_below m j
  show num_rp_below m (j + 1) = num_rp_below m j from h1
  done

We can now use num_rp_below to define the totient function.

def phi (m : Nat) : Nat := num_rp_below m m

lemma phi_def (m : Nat) : phi m = num_rp_below m m := by rfl

#eval phi 10   --Answer: 4

With this preparation, we can now state the theorem we will prove:

theorem Theorem_7_4_2 {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    [a]_m ^ (phi m) = [1]_m

In preparation for proving this theorem, HTPI first shows that the set of invertible congruence classes is closed under inverses and multiplication. For our purposes, we will find it useful to prove a slightly different lemma. Note that Lean knows all of the basic algebraic laws of addition and multiplication of congruence classes, and as a result the ring tactic can be used to do algebraic reasoning in ZMod m, as illustrated in the proof below.

lemma prod_inv_iff_inv {m : Nat} {X : ZMod m}
    (h1 : invertible X) (Y : ZMod m) :
    invertible (X * Y) ↔ invertible Y := by
  apply Iff.intro
  · -- (→)
    assume h2 : invertible (X * Y)
    obtain (Z : ZMod m) (h3 : X * Y * Z = [1]_m) from h2
    apply Exists.intro (X * Z)
    rewrite [←h3]  --Goal : Y * (X * Z) = X * Y * Z
    ring     --Note that ring can do algebra in ZMod m
    done
  · -- (←)
    assume h2 : invertible Y
    obtain (Xi : ZMod m) (h3 : X * Xi = [1]_m) from h1
    obtain (Yi : ZMod m) (h4 : Y * Yi = [1]_m) from h2
    apply Exists.intro (Xi * Yi)
    show (X * Y) * (Xi * Yi) = [1]_m from
      calc X * Y * (Xi * Yi)
        _ = (X * Xi) * (Y * Yi) := by ring
        _ = [1]_m * [1]_m := by rw [h3, h4]
        _ = [1]_m := Theorem_7_3_6_7 [1]_m
    done
  done

One of the key ideas in the proof of Theorem 7.4.2 in HTPI involves computing the product of all invertible congruence classes. To compute this product in Lean, we begin by defining a function F m : Nat → ZMod m as follows:

def F (m i : Nat) : ZMod m := if gcd m i = 1 then [i]_m else [1]_m

lemma F_rp_def {m i : Nat} (h : rel_prime m i) :
    F m i = [i]_m := by
  have h1 : F m i = if gcd m i = 1 then [i]_m else [1]_m := by rfl
  define at h      --h : gcd m i = 1
  rewrite [if_pos h] at h1
  show F m i = [i]_m from h1
  done

lemma F_not_rp_def {m i : Nat} (h : ¬rel_prime m i) :
    F m i = [1]_m := sorry

Note that F is defined as a function of two natural numbers, m and i, but as we discussed in Section 5.4, it follows that the partial application F m is a function from Nat to ZMod m.

Now consider the product (F m 0) * (F m 1) * ... * (F m (m - 1)); we will call this the F-product. If m and i are not relatively prime, then F m i = [1]_m, and since [1]_m is the multiplicative identity element of ZMod m, the factor F m i contributes nothing to the product. Thus, the F-product is equal to the product of the factors F m i for which m and i are relatively prime. But for those values of i, F m i = [i]_m, so the product is equal to the product of all congruence classes [i]_m with m and i relatively prime. By Theorem_7_3_7, that is the product of all invertible congruence classes.

To express the F-product in Lean, we imitate our approach to summations, as described in Chapter 6. We begin by defining prod_seq j k f to be the product of a sequence of j consecutive values of the function f, starting with f k:

def prod_seq {m : Nat}
    (j k : Nat) (f : Nat → ZMod m) : ZMod m :=
  match j with
    | 0 => [1]_m
    | n + 1 => prod_seq n k f * f (k + n)

lemma prod_seq_base {m : Nat}
    (k : Nat) (f : Nat → ZMod m) : prod_seq 0 k f = [1]_m := by rfl

lemma prod_seq_step {m : Nat}
    (n k : Nat) (f : Nat → ZMod m) :
    prod_seq (n + 1) k f = prod_seq n k f * f (k + n) := by rfl

lemma prod_seq_zero_step {m : Nat}
    (n : Nat) (f : Nat → ZMod m) :
    prod_seq (n + 1) 0 f = prod_seq n 0 f * f n := sorry

Using this notation, the expression prod_seq m 0 (F m) denotes the F-product, which, as we saw earlier, is equal to the product of the invertible congruence classes.

Now suppose a is a natural number that is relatively prime to m. The next step in the proof in HTPI is to multiply each factor in the product of the invertible congruence classes by [a]_m. To do this, we define a function G as follows:

def G (m a i : Nat) : Nat := (a * i) % m

Consider the following product, which we will call the FG-product:

(F m (G m a 0)) * (F m (G m a 1)) * ... * (F m (G m a (m - 1))).

Using the partial application G m a, which is a function from Nat to Nat, we can express this in Lean as prod_seq m 0 ((F m) ∘ (G m a)). To understand this product we will need two facts about G.

lemma cc_G (m a i : Nat) : [G m a i]_m = [a]_m * [i]_m :=
  calc [G m a i]_m
    _ = [(a * i) % m]_m := by rfl
    _ = [a * i]_m := (cc_eq_mod m (a * i)).symm
    _ = [a]_m * [i]_m := (mul_class m a i).symm

lemma G_rp_iff {m a : Nat} (h1 : rel_prime m a) (i : Nat) :
    rel_prime m (G m a i) ↔ rel_prime m i := by
  have h2 : invertible [a]_m := (Theorem_7_3_7 m a).rtl h1
  show rel_prime m (G m a i) ↔ rel_prime m i from
    calc rel_prime m (G m a i)
      _ ↔ invertible [G m a i]_m := (Theorem_7_3_7 m (G m a i)).symm
      _ ↔ invertible ([a]_m * [i]_m) := by rw [cc_G]
      _ ↔ invertible [i]_m := prod_inv_iff_inv h2 ([i]_m)
      _ ↔ rel_prime m i := Theorem_7_3_7 m i
  done

Now let’s analyze the FG-product. If i is not relatively prime to m, then by G_rp_iff, G m a i is also not relatively prime to m, so F m (G m a i) = [1]_m. As before, this means that these terms contribute nothing to the FG-product. If i is relatively prime to m, then so is G m a i, and therefore, by cc_G,

F m (G m a i) = [G m a i]_m = [a]_m * [i]_m = [a]_m * (F m i).

This means that, in the FG-product, each factor contributed by a value of i that is relatively prime to m is [a]_m times the corresponding factor in the F-product. Since the number of such factors is phi m, it follows that the FG-product is [a]_m ^ (phi m) times the F-product.

Let’s see if we can prove this in Lean.

lemma FG_rp {m a i : Nat} (h1 : rel_prime m a) (h2 : rel_prime m i) :
    F m (G m a i) = [a]_m * F m i := by
  have h3 : rel_prime m (G m a i) := (G_rp_iff h1 i).rtl h2
  show F m (G m a i) = [a]_m * F m i from
    calc F m (G m a i)
      _ = [G m a i]_m := F_rp_def h3
      _ = [a]_m * [i]_m := cc_G m a i
      _ = [a]_m * F m i := by rw [F_rp_def h2]
  done

lemma FG_not_rp {m a i : Nat} (h1 : rel_prime m a) (h2 : ¬rel_prime m i) :
    F m (G m a i) = [1]_m := sorry

lemma FG_prod {m a : Nat} (h1 : rel_prime m a) :
    ∀ (k : Nat), prod_seq k 0 ((F m) ∘ (G m a)) =
      [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) := by
  by_induc
  · -- Base Case
    show prod_seq 0 0 ((F m) ∘ (G m a)) =
          [a]_m ^ (num_rp_below m 0) * prod_seq 0 0 (F m) from
      calc prod_seq 0 0 ((F m) ∘ (G m a))
        _ = [1]_m := prod_seq_base _ _
        _ = [a]_m ^ 0 * [1]_m := by ring
        _ = [a]_m ^ (num_rp_below m 0) * prod_seq 0 0 (F m) := by
              rw [num_rp_below_base, prod_seq_base]
    done
  · -- Induction Step
    fix k : Nat
    assume ih : prod_seq k 0 ((F m) ∘ (G m a)) =
      [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m)
    by_cases h2 : rel_prime m k
    · -- Case 1. h2 : rel_prime m k
      show prod_seq (k + 1) 0 ((F m) ∘ (G m a)) =
          [a]_m ^ (num_rp_below m (k + 1)) *
          prod_seq (k + 1) 0 (F m) from
        calc prod_seq (k + 1) 0 ((F m) ∘ (G m a))
          _ = prod_seq k 0 ((F m) ∘ (G m a)) *
              F m (G m a k) := prod_seq_zero_step _ _
          _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
              F m (G m a k) := by rw [ih]
          _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
              ([a]_m * F m k) := by rw [FG_rp h1 h2]
          _ = [a]_m ^ ((num_rp_below m k) + 1) *
              ((prod_seq k 0 (F m)) * F m k) := by ring
          _ = [a]_m ^ (num_rp_below m (k + 1)) *
              prod_seq (k + 1) 0 (F m) := by
                rw [num_rp_below_step_rp h2, prod_seq_zero_step]
      done
    · -- Case 2. h2 : ¬rel_prime m k
      show prod_seq (k + 1) 0 ((F m) ∘ (G m a)) =
          [a]_m ^ (num_rp_below m (k + 1)) *
          prod_seq (k + 1) 0 (F m) from
        calc prod_seq (k + 1) 0 ((F m) ∘ (G m a))
          _ = prod_seq k 0 ((F m) ∘ (G m a)) *
              F m (G m a k) := prod_seq_zero_step _ _
          _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
              F m (G m a k) := by rw [ih]
          _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
              ([1]_m) := by rw [FG_not_rp h1 h2]
          _ = [a]_m ^ (num_rp_below m k) *
              (prod_seq k 0 (F m) * ([1]_m)) := by ring
          _ = [a]_m ^ (num_rp_below m (k + 1)) *
              prod_seq (k + 1) 0 (F m) := by
                rw [num_rp_below_step_not_rp h2, prod_seq_zero_step,
                F_not_rp_def h2]
      done
    done
  done

The lemma FG_prod, in the case k = m, tells us that

prod_seq m 0 ((F m) ∘ (G m a)) = [a]_m ^ (phi m) * prod_seq m 0 (F m).

In other words, we have proven that the FG-product is [a]_m ^ (phi m) times the F-product.

And now we come to the central idea in the proof of Theorem_7_4_2: the congruence classes that are multiplied in the FG-product are exactly the same as the congruence classes multiplied in the F-product, but listed in a different order. The reason for this is that the function G m a permutes the natural numbers less than m. Since multiplication of congruence classes is commutative and associative, it follows that the FG-product and the F-product are equal.

To prove these claims, we first define what it means for a function to permute the natural numbers less than a natural number n.

def maps_below (n : Nat) (g : Nat → Nat) : Prop := ∀ i < n, g i < n

def one_one_below (n : Nat) (g : Nat → Nat) : Prop :=
  ∀ i1 < n, ∀ i2 < n, g i1 = g i2 → i1 = i2

def onto_below (n : Nat) (g : Nat → Nat) : Prop :=
  ∀ k < n, ∃ i < n, g i = k

def perm_below (n : Nat) (g : Nat → Nat) : Prop :=
  maps_below n g ∧ one_one_below n g ∧ onto_below n g

The proofs of our next two lemmas are somewhat long. We state them now, but put off discussion of their proofs until the end of the section. The first lemma says that, if m and a are relatively prime, then G m a permutes the natural numbers less than m, and the second says that permuting the terms of a product does not change the value of the product.

lemma G_perm_below {m a : Nat} [NeZero m]
    (h1 : rel_prime m a) : perm_below m (G m a)

lemma perm_prod {m : Nat} (f : Nat → ZMod m) :
    ∀ (n : Nat), ∀ (g : Nat → Nat), perm_below n g →
      prod_seq n 0 f = prod_seq n 0 (f ∘ g)

There is just one more fact we need before we can prove Theorem_7_4_2: all of the factors in the F-product are invertible, and therefore the F-product is invertible:

lemma F_invertible (m i : Nat) : invertible (F m i) := by
  by_cases h : rel_prime m i
  · -- Case 1. h : rel_prime m i
    rewrite [F_rp_def h]
    show invertible [i]_m from (Theorem_7_3_7 m i).rtl h
    done
  · -- Case 2. h : ¬rel_prime m i
    rewrite [F_not_rp_def h]
    apply Exists.intro [1]_m
    show [1]_m * [1]_m = [1]_m from Theorem_7_3_6_7 [1]_m
    done
  done

lemma Fprod_invertible (m : Nat) :
    ∀ (k : Nat), invertible (prod_seq k 0 (F m)) := by
  by_induc
  · -- Base Case
    apply Exists.intro [1]_m
    show prod_seq 0 0 (F m) * [1]_m = [1]_m from
      calc prod_seq 0 0 (F m) * [1]_m
        _ = [1]_m * [1]_m := by rw [prod_seq_base]
        _ = [1]_m := Theorem_7_3_6_7 ([1]_m)
    done
  · -- Induction Step
    fix k : Nat
    assume ih : invertible (prod_seq k 0 (F m))
    rewrite [prod_seq_zero_step]
    show invertible (prod_seq k 0 (F m) * (F m k)) from
      (prod_inv_iff_inv ih (F m k)).rtl (F_invertible m k)
    done
  done

We now have everything we need to prove Theorem_7_4_2:

theorem Theorem_7_4_2 {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    [a]_m ^ (phi m) = [1]_m := by
  have h2 : invertible (prod_seq m 0 (F m)) := Fprod_invertible m m
  obtain (Y : ZMod m) (h3 : prod_seq m 0 (F m) * Y = [1]_m) from h2
  show [a]_m ^ (phi m) = [1]_m from
    calc [a]_m ^ (phi m)
      _ = [a]_m ^ (phi m) * [1]_m := (Theorem_7_3_6_7 _).symm
      _ = [a]_m ^ (phi m) * (prod_seq m 0 (F m) * Y) := by rw [h3]
      _ = ([a]_m ^ (phi m) * prod_seq m 0 (F m)) * Y := by ring
      _ = prod_seq m 0 (F m ∘ G m a) * Y := by rw [FG_prod h1 m, phi_def]
      _ = prod_seq m 0 (F m) * Y := by
            rw [perm_prod (F m) m (G m a) (G_perm_below h1)]
      _ = [1]_m := by rw [h3]
  done

Rephrasing this theorem in terms of numbers gives us the usual statement of Euler’s theorem:

lemma Exercise_7_4_5_Int (m : Nat) (a : Int) :
    ∀ (n : Nat), [a]_m ^ n = [a ^ n]_m := sorry

lemma Exercise_7_4_5_Nat (m a n : Nat) :
    [a]_m ^ n = [a ^ n]_m := by
  rewrite [Exercise_7_4_5_Int]
  rfl
  done

theorem Euler's_theorem {m a : Nat} [NeZero m]
    (h1 : rel_prime m a) : a ^ (phi m) ≡ 1 (MOD m) := by
  have h2 : [a]_m ^ (phi m) = [1]_m := Theorem_7_4_2 h1
  rewrite [Exercise_7_4_5_Nat m a (phi m)] at h2
    --h2 : [a ^ phi m]_m = [1]_m
  show a ^ (phi m) ≡ 1 (MOD m) from (cc_eq_iff_congr _ _ _).ltr h2
  done

#eval gcd 10 7     --Answer: 1.  So 10 and 7 are relatively prime

#eval 7 ^ phi 10   --Answer: 2401, which is congruent to 1 mod 10.

We now turn to the two lemmas whose proofs we skipped over, G_perm_below and perm_prod. To prove G_perm_below, we must prove three facts: maps_below m (G m a), one_one_below m (G m a), and onto_below m (G m a). The first is straightforward:

lemma G_maps_below (m a : Nat) [NeZero m] : maps_below m (G m a) := by
  define             --Goal : ∀ i < m, G m a i < m
  fix i : Nat
  assume h1 : i < m
  rewrite [G_def]    --Goal : a * i % m < m
  show a * i % m < m from mod_nonzero_lt (a * i) (NeZero.ne m)
  done

For the second and third, we start with lemmas that are reminiscent of Theorem 5.3.3.

lemma right_inv_onto_below {n : Nat} {g g' : Nat → Nat}
    (h1 : ∀ i < n, g (g' i) = i) (h2 : maps_below n g') :
    onto_below n g := by
  define at h2; define
  fix k : Nat
  assume h3 : k < n
  apply Exists.intro (g' k)
  show g' k < n ∧ g (g' k) = k from And.intro (h2 k h3) (h1 k h3)
  done

lemma left_inv_one_one_below {n : Nat} {g g' : Nat → Nat}
    (h1 : ∀ i < n, g' (g i) = i) : one_one_below n g := sorry

To apply these lemmas with g = G m a, we need a function to play the role of g'. A natural choice is G m a', where a' is chosen so that [a']_m is the multiplicative inverse of [a]_m. We know from earlier work that if m and a are relatively prime then the multiplicative inverse of [a]_m is [gcd_c2 m a]_m. However, in the notation G m a', we can’t let a' = gcd_c2 m a, because a' must be a natural number and gcd_c2 a is an integer. And we can’t simply coerce an integer to be a natural number—what if it’s negative? But we know [gcd_c2 m a]_m = [(gcd_c2 m a) % m]_m and 0 ≤ (gcd_c2 m a) % m, and there is a function, Int.toNat, that will convert a nonnegative integer to a natural number. So we make the following definitions:

def inv_mod (m a : Nat) : Nat := Int.toNat ((gcd_c2 m a) % m)

def Ginv (m a i : Nat) : Nat := G m (inv_mod m a) i

Now Ginv m a can play the role of g' in the last two lemmas. We’ll skip the details and just summarize the results.

lemma Ginv_right_inv {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    ∀ i < m, G m a (Ginv m a i) = i := sorry

lemma Ginv_left_inv {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    ∀ i < m, Ginv m a (G m a i) = i := sorry

lemma Ginv_maps_below (m a : Nat) [NeZero m] :
    maps_below m (Ginv m a) := G_maps_below m (inv_mod m a)

lemma G_one_one_below {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    one_one_below m (G m a) :=
  left_inv_one_one_below (Ginv_left_inv h1)

lemma G_onto_below {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    onto_below m (G m a) :=
  right_inv_onto_below (Ginv_right_inv h1) (Ginv_maps_below m a)

lemma G_perm_below {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    perm_below m (G m a) := And.intro (G_maps_below m a)
  (And.intro (G_one_one_below h1) (G_onto_below h1))

Finally, we turn to the proof of perm_prod. Our proof will be by mathematical induction. In the induction step, our induction hypothesis will be

∀ (g : Nat → Nat), perm_below n g →
    prod_seq n 0 f = prod_seq n 0 (f ∘ g),

and we will have to prove

∀ (g : Nat → Nat), perm_below (n + 1) g →
    prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g).

To prove this, we’ll introduce an arbitrary function g : Nat → Nat and assume perm_below (n + 1) g. How can we make use of the inductive hypothesis? Here’s the key idea: Since g permutes the numbers below n + 1, there must be some u ≤ n such that g u = n. Now let s be a function that swaps u and n, but leaves all other numbers fixed. In other words, s u = n, s n = u, and s i = i if i ≠ u and i ≠ n. It is not hard to show that s permutes the numbers below n + 1, and using that fact we can prove that g ∘ s permutes the numbers below n + 1. But notice that

(g ∘ s) n = g (s n) = g u = n.

In other words, g ∘ s leaves n fixed. Using that fact, we’ll be able to prove that g ∘ s permutes the numbers below n. We can therefore apply the inductive hypothesis to g ∘ s, which leads to the conclusion

prod_seq n 0 f = prod_seq n 0 (f ∘ g ∘ s).

Since we also have (f ∘ g ∘ s) n = f ((g ∘ s) n) = f n, we can extend this to

prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g ∘ s).

Finally, we can then reach the required conclusion by proving

prod_seq (n + 1) 0 (f ∘ g ∘ s) = prod_seq (n + 1) 0 (f ∘ g).

To carry out this plan, we begin by defining our “swapping” function and proving its properties.

def swap (u v i : Nat) : Nat :=
  if i = u then v else if i = v then u else i

lemma swap_fst (u v : Nat) : swap u v u = v := by
  define : swap u v u
    --Goal : (if u = u then v else if u = v then u else u) = v
  have h : u = u := by rfl
  rewrite [if_pos h]
  rfl
  done

lemma swap_snd (u v : Nat) : swap u v v = u := sorry

lemma swap_perm_below {u v n} (h1 : u < n) (h2 : v < n) :
    perm_below n (swap u v) := sorry

For the swapping function s in the proof outline above, we’ll use swap u n. To prove that g ∘ swap u n permutes the numbers below n, we’ll need two lemmas:

lemma comp_perm_below {n : Nat} {f g : Nat → Nat}
    (h1 : perm_below n f) (h2 : perm_below n g) :
    perm_below n (f ∘ g) := sorry

lemma perm_below_fixed {n : Nat} {g : Nat → Nat}
    (h1 : perm_below (n + 1) g) (h2 : g n = n) : perm_below n g := sorry

For the final step of the proof, we’ll need several lemmas

lemma break_prod_twice  {m u j n : Nat} (f : Nat → ZMod m)
    (h1 : n = u + 1 + j) : prod_seq (n + 1) 0 f =
      prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n := sorry

lemma swap_prod_eq_prod_below {m u n : Nat} (f : Nat → ZMod m)
    (h1 : u ≤ n) : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f := sorry

lemma swap_prod_eq_prod_between {m u j n : Nat} (f : Nat → ZMod m)
    (h1 : n = u + 1 + j) : prod_seq j (u + 1) (f ∘ swap u n) =
      prod_seq j (u + 1) f := sorry

lemma trivial_swap (u : Nat) : swap u u = id := sorry

Using these lemmas, we can prove the fact we’ll need in the final step.

lemma swap_prod_eq_prod {m u n : Nat} (f : Nat → ZMod m) (h1 : u ≤ n) :
    prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f := by
  by_cases h2 : u = n
  · -- Case 1. h2 : u = n
    rewrite [h2, trivial_swap n]
      --Goal : prod_seq (n + 1) 0 (f ∘ id) = prod_seq (n + 1) 0 f
    rfl
    done
  · -- Case 2. h2 : ¬u = n
    have h3 : u + 1 ≤ n := Nat.lt_of_le_of_ne h1 h2
    obtain (j : Nat) (h4 : n = u + 1 + j) from Nat.exists_eq_add_of_le h3
    have break_f : prod_seq (n + 1) 0 f =
      prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n :=
      break_prod_twice f h4
    have break_fs : prod_seq (n + 1) 0 (f ∘ swap u n) =
      prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u *
      prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n :=
      break_prod_twice (f ∘ swap u n) h4
    have f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) =
      prod_seq u 0 f := swap_prod_eq_prod_below f h1
    have f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) =
      prod_seq j (u + 1) f := swap_prod_eq_prod_between f h4
    show prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f from
      calc prod_seq (n + 1) 0 (f ∘ swap u n)
        _ = prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u *
            prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n :=
              break_fs
        _ = prod_seq u 0 f * (f ∘ swap u n) u *
            prod_seq j (u + 1) f * (f ∘ swap u n) n := by
              rw [f_eq_fs_below, f_eq_fs_btwn]
        _ = prod_seq u 0 f * f (swap u n u) *
            prod_seq j (u + 1) f * f (swap u n n) := by rfl
        _ = prod_seq u 0 f * f n * prod_seq j (u + 1) f * f u := by
              rw [swap_fst, swap_snd]
        _ = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n := by ring
        _ = prod_seq (n + 1) 0 f := break_f.symm
    done
  done

We finally have all the pieces in place to prove perm_prod:

lemma perm_prod {m : Nat} (f : Nat → ZMod m) :
    ∀ (n : Nat), ∀ (g : Nat → Nat), perm_below n g →
      prod_seq n 0 f = prod_seq n 0 (f ∘ g) := by
  by_induc
  · -- Base Case
    fix g : Nat → Nat
    assume h1 : perm_below 0 g
    rewrite [prod_seq_base, prod_seq_base]
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : ∀ (g : Nat → Nat), perm_below n g →
      prod_seq n 0 f = prod_seq n 0 (f ∘ g)
    fix g : Nat → Nat
    assume g_pb : perm_below (n + 1) g
    define at g_pb
    have g_ob : onto_below (n + 1) g := g_pb.right.right
    define at g_ob
    have h1 : n < n + 1 := by linarith
    obtain (u : Nat) (h2 : u < n + 1 ∧ g u = n) from g_ob n h1
    have s_pb : perm_below (n + 1) (swap u n) :=
      swap_perm_below h2.left h1
    have gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n) :=
      comp_perm_below g_pb s_pb
    have gs_fix_n : (g ∘ swap u n) n = n :=
      calc (g ∘ swap u n) n
        _ = g (swap u n n) := by rfl
        _ = g u := by rw [swap_snd]
        _ = n := h2.right
    have gs_pb_n : perm_below n (g ∘ swap u n) :=
      perm_below_fixed gs_pb_n1 gs_fix_n
    have gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ (g ∘ swap u n)) :=
      ih (g ∘ swap u n) gs_pb_n
    have h3 : u ≤ n := by linarith
    show prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g) from
      calc prod_seq (n + 1) 0 f
        _ = prod_seq n 0 f * f n := prod_seq_zero_step n f
        _ = prod_seq n 0 (f ∘ (g ∘ swap u n)) *
            f ((g ∘ swap u n) n) := by rw [gs_prod, gs_fix_n]
        _ = prod_seq n 0 (f ∘ g ∘ swap u n) *
            (f ∘ g ∘ swap u n) n := by rfl
        _ = prod_seq (n + 1) 0 (f ∘ g ∘ swap u n) :=
              (prod_seq_zero_step n (f ∘ g ∘ swap u n)).symm
        _ = prod_seq (n + 1) 0 ((f ∘ g) ∘ swap u n) := by rfl
        _ = prod_seq (n + 1) 0 (f ∘ g) := swap_prod_eq_prod (f ∘ g) h3
    done
  done

There is one more theorem that is proven in Section 7.4 of HTPI: Theorem 7.4.4, which says that \(\varphi\) is a multiplicative function. The proof requires ideas that we will not develop in Lean until Chapter 8, so we will put off the proof until Section 8.1½.

Exercises

--Hint:  Use induction.
--For the base case, compute [a]_m ^ 0 * [1]_m in two ways:
--by Theorem_7_3_6_7, [a] ^ 0 * [1]_m = [a]_m ^ 0
--by ring, [a]_m ^ 0 * [1]_m = [1]_m.
lemma Exercise_7_4_5_Int (m : Nat) (a : Int) :
    ∀ (n : Nat), [a]_m ^ n = [a ^ n]_m := sorry

lemma left_inv_one_one_below {n : Nat} {g g' : Nat → Nat}
    (h1 : ∀ i < n, g' (g i) = i) : one_one_below n g := sorry

lemma comp_perm_below {n : Nat} {f g : Nat → Nat}
    (h1 : perm_below n f) (h2 : perm_below n g) :
    perm_below n (f ∘ g) := sorry

lemma perm_below_fixed {n : Nat} {g : Nat → Nat}
    (h1 : perm_below (n + 1) g) (h2 : g n = n) : perm_below n g := sorry

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

example {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    a ^ (phi m + 1) ≡ a (MOD m) := sorry

theorem Like_Exercise_7_4_11 {m a p : Nat} [NeZero m]
    (h1 : rel_prime m a) (h2 : p + 1 = phi m) :
    [a]_m * [a ^ p]_m = [1]_m := sorry

theorem Like_Exercise_7_4_12 {m a p q k : Nat} [NeZero m]
    (h1 : rel_prime m a) (h2 : p = q + (phi m) * k) :
    a ^ p ≡ a ^ q (MOD m) := sorry

7.5. Public-Key Cryptography

Section 7.5 of HTPI discusses the RSA public-key cryptography system. The system is based on the following theorem:

theorem Theorem_7_5_1 (p q n e d k m c : Nat)
    (p_prime : prime p) (q_prime : prime q) (p_ne_q : p ≠ q)
    (n_pq : n = p * q) (ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1)
    (h1 : [m]_n ^ e = [c]_n) : [c]_n ^ d = [m]_n

For an explanation of how the RSA system works and why Theorem_7_5_1 justifies it, see HTPI. Here we will focus on proving the theorem in Lean.

We will be applying Euler’s theorem to the prime numbers p and q, so we will need to know how to compute phi p and phi q. Fortunately, there is a simple formula we can use.

lemma num_rp_prime {p : Nat} (h1 : prime p) :
    ∀ k < p, num_rp_below p (k + 1) = k := sorry

lemma phi_prime {p : Nat} (h1 : prime p) : phi p = p - 1 := by
  have h2 : 1 ≤ p := prime_pos h1
  have h3 : p - 1 + 1 = p := Nat.sub_add_cancel h2
  have h4 : p - 1 < p := by linarith
  have h5 : num_rp_below p (p - 1 + 1) = p - 1 :=
    num_rp_prime h1 (p - 1) h4
  rewrite [h3] at h5
  show phi p = p - 1 from h5
  done

We will also need to use Lemma 7.4.5 from HTPI. To prove that lemma in Lean, we will use Theorem_7_2_2, which says that for natural numbers a, b, and c, if c ∣ a * b and c and a are relatively prime, then c ∣ b. But we will need to extend the theorem to allow b to be an integer rather than a natural number. To prove this extension, we use the Lean function Int.natAbs : Int → Nat, which computes the absolute value of an integer. Lean knows several theorems about this function:

@Int.coe_nat_dvd_left : ∀ {n : ℕ} {z : ℤ}, ↑n ∣ z ↔ n ∣ Int.natAbs z

Int.natAbs_mul : ∀ (a b : ℤ),
                  Int.natAbs (a * b) = Int.natAbs a * Int.natAbs b

Int.natAbs_ofNat : ∀ (n : ℕ), Int.natAbs ↑n = n

With the help of these theorems, our extended version of Theorem_7_2_2 follows easily from the original version:

theorem Theorem_7_2_2_Int {a c : Nat} {b : Int}
    (h1 : ↑c ∣ ↑a * b) (h2 : rel_prime a c) : ↑c ∣ b := by
  rewrite [Int.coe_nat_dvd_left, Int.natAbs_mul,
    Int.natAbs_ofNat] at h1        --h1 : c ∣ a * Int.natAbs b
  rewrite [Int.coe_nat_dvd_left]   --Goal : c ∣ Int.natAbs b
  show c ∣ Int.natAbs b from Theorem_7_2_2 h1 h2
  done

With that preparation, we can now prove Lemma_7_4_5.

lemma Lemma_7_4_5 {m n : Nat} (a b : Int) (h1 : rel_prime m n) :
    a ≡ b (MOD m * n) ↔ a ≡ b (MOD m) ∧ a ≡ b (MOD n) := by
  apply Iff.intro
  · -- (→)
    assume h2 : a ≡ b (MOD m * n)
    obtain (j : Int) (h3 : a - b = (m * n) * j) from h2
    apply And.intro
    · -- Proof of a ≡ b (MOD m)
      apply Exists.intro (n * j)
      show a - b = m * (n * j) from
        calc a - b
          _ = m * n * j := h3
          _ = m * (n * j) := by ring
      done
    · -- Proof of a ≡ b (MOD n)
      apply Exists.intro (m * j)
      show a - b = n * (m * j) from
        calc a - b
          _ = m * n * j := h3
          _ = n * (m * j) := by ring
      done
    done
  · -- (←)
    assume h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
    obtain (j : Int) (h3 : a - b = m * j) from h2.left
    have h4 : (↑n : Int) ∣ a - b := h2.right
    rewrite [h3] at h4      --h4 : ↑n ∣ ↑m * j
    have h5 : ↑n ∣ j := Theorem_7_2_2_Int h4 h1
    obtain (k : Int) (h6 : j = n * k) from h5
    apply Exists.intro k    --Goal : a - b = ↑(m * n) * k
    rewrite [Nat.cast_mul]  --Goal : a - b = ↑m * ↑n * k
    show a - b = (m * n) * k from
      calc a - b
        _ = m * j := h3
        _ = m * (n * k) := by rw [h6]
        _ = (m * n) * k := by ring
    done
  done

Finally, we will need an exercise from Section 7.2, and we will need to know NeZero p for prime numbers p:

theorem rel_prime_symm {a b : Nat} (h : rel_prime a b) :
    rel_prime b a := sorry

lemma prime_NeZero {p : Nat} (h : prime p) : NeZero p := by
  rewrite [neZero_iff]     --Goal : p ≠ 0
  define at h
  linarith
  done

Much of the reasoning about modular arithmetic that we need for the proof of Theorem_7_5_1 is contained in a technical lemma:

lemma Lemma_7_5_1 {p e d m c s : Nat} {t : Int}
    (h1 : prime p) (h2 : e * d = (p - 1) * s + 1)
    (h3 : m ^ e - c = p * t) :
    c ^ d ≡ m (MOD p) := by
  have h4 : m ^ e ≡ c (MOD p) := Exists.intro t h3
  have h5 : [m ^ e]_p = [c]_p := (cc_eq_iff_congr _ _ _).rtl h4
  rewrite [←Exercise_7_4_5_Nat] at h5  --h5 : [m]_p ^ e = [c]_p
  by_cases h6 : p ∣ m
  · -- Case 1. h6 : p ∣ m
    have h7 : m ≡ 0 (MOD p) := by
      obtain (j : Nat) (h8 : m = p * j) from h6
      apply Exists.intro (↑j : Int)   --Goal : ↑m - 0 = ↑p * ↑j
      rewrite [h8, Nat.cast_mul]
      ring
      done
    have h8 : [m]_p = [0]_p := (cc_eq_iff_congr _ _ _).rtl h7
    have h9 : 0 < (e * d) := by
      rewrite [h2]
      have h10 : 0 ≤ (p - 1) * s := Nat.zero_le _
      linarith
      done
    have h10 : (0 : Int) ^ (e * d) = 0 := zero_pow h9
    have h11 : [c ^ d]_p = [m]_p :=
      calc [c ^ d]_p
        _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
        _ = ([m]_p ^ e) ^ d := by rw [h5]
        _ = [m]_p ^ (e * d) := by ring
        _ = [0]_p ^ (e * d) := by rw [h8]
        _ = [0 ^ (e * d)]_p := Exercise_7_4_5_Int _ _ _
        _ = [0]_p := by rw [h10]
        _ = [m]_p := by rw [h8]
    show c ^ d ≡ m (MOD p)  from (cc_eq_iff_congr _ _ _).ltr h11
    done
  · -- Case 2. h6 : ¬p ∣ m
    have h7 : rel_prime m p := rel_prime_of_prime_not_dvd h1 h6
    have h8 : rel_prime p m := rel_prime_symm h7
    have h9 : NeZero p := prime_NeZero h1
    have h10 : (1 : Int) ^ s = 1 := by ring
    have h11 : [c ^ d]_p = [m]_p :=
      calc [c ^ d]_p
        _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
        _ = ([m]_p ^ e) ^ d := by rw [h5]
        _ = [m]_p ^ (e * d) := by ring
        _ = [m]_p ^ ((p - 1) * s + 1) := by rw [h2]
        _ = ([m]_p ^ (p - 1)) ^ s * [m]_p := by ring
        _ = ([m]_p ^ (phi p)) ^ s * [m]_p := by rw [phi_prime h1]
        _ = [1]_p ^ s * [m]_p := by rw [Theorem_7_4_2 h8]
        _ = [1 ^ s]_p * [m]_p := by rw [Exercise_7_4_5_Int]
        _ = [1]_p * [m]_p := by rw [h10]
        _ = [m]_p * [1]_p := by ring
        _ = [m]_p := Theorem_7_3_6_7 _
    show c ^ d ≡ m (MOD p)  from (cc_eq_iff_congr _ _ _).ltr h11
    done
  done

Here, finally, is the proof of Theorem_7_5_1:

theorem Theorem_7_5_1 (p q n e d k m c : Nat)
    (p_prime : prime p) (q_prime : prime q) (p_ne_q : p ≠ q)
    (n_pq : n = p * q) (ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1)
    (h1 : [m]_n ^ e = [c]_n) : [c]_n ^ d = [m]_n := by
  rewrite [Exercise_7_4_5_Nat, cc_eq_iff_congr] at h1
    --h1 : m ^ e ≡ c (MOD n)
  rewrite [Exercise_7_4_5_Nat, cc_eq_iff_congr]
    --Goal : c ^ d ≡ m (MOD n)
  obtain (j : Int) (h2 : m ^ e - c = n * j) from h1
  rewrite [n_pq, Nat.cast_mul] at h2
    --h2 : m ^ e - c = p * q * j
  have h3 : e * d = (p - 1) * (k * (q - 1)) + 1 := by
    rewrite [ed_congr_1]
    ring
    done
  have h4 : m ^ e - c = p * (q * j) := by
    rewrite [h2]
    ring
    done
  have congr_p : c ^ d ≡ m (MOD p) := Lemma_7_5_1 p_prime h3 h4
  have h5 : e * d = (q - 1) * (k * (p - 1)) + 1 := by
    rewrite [ed_congr_1]
    ring
    done
  have h6 : m ^ e - c = q * (p * j) := by
    rewrite [h2]
    ring
    done
  have congr_q : c ^ d ≡ m (MOD q) := Lemma_7_5_1 q_prime h5 h6
  have h7 : ¬q ∣ p := by
    by_contra h8
    have h9 : q = 1 ∨ q = p := dvd_prime p_prime h8
    disj_syll h9 (prime_not_one q_prime)
    show False from p_ne_q h9.symm
    done
  have h8 : rel_prime p q := rel_prime_of_prime_not_dvd q_prime h7
  rewrite [n_pq, Lemma_7_4_5 _ _ h8]
  show c ^ d ≡ m (MOD p) ∧ c ^ d ≡ m (MOD q) from
    And.intro congr_p congr_q
  done

Exercises

--Hint:  Use induction.
lemma num_rp_prime {p : Nat} (h1 : prime p) :
    ∀ k < p, num_rp_below p (k + 1) = k := sorry

lemma three_prime : prime 3 := sorry

--Hint:  Use the previous exercise, Exercise_7_2_7, and Theorem_7_4_2.
theorem Exercise_7_5_13a (a : Nat) (h1 : rel_prime 561 a) :
    a ^ 560 ≡ 1 (MOD 3) := sorry

--Hint:  Imitate the way Theorem_7_2_2_Int was proven from Theorem_7_2_2.
lemma Theorem_7_2_3_Int {p : Nat} {a b : Int}
    (h1 : prime p) (h2 : ↑p ∣ a * b) : ↑p ∣ a ∨ ↑p ∣ b := sorry

--Hint:  Use the previous exercise.
theorem Exercise_7_5_14b (n : Nat) (b : Int)
    (h1 : prime n) (h2 : b ^ 2 ≡ 1 (MOD n)) :
    b ≡ 1 (MOD n) ∨ b ≡ -1 (MOD n) := sorry