5. 初等数论

在本章中，我们向你展示如何形式化数论中的一些初等结果。 当我们处理更实质性的数学内容时， 证明会变得更长、更复杂， 以你已经掌握的技能为基础。

5.1. 无理根

让我们从古希腊人知道的一个事实开始，即 2 的平方根是无理数。 如果我们假定并非如此， 则我们可以将其表示为最简分数 \(\sqrt{2} = a / b\). 两边取平方得到 \(a^2 = 2 b^2\), 这意味着 \(a\) 是偶数。 如果我们记 \(a = 2c\), 则有 \(4c^2 = 2 b^2\), 从而 \(b^2 = 2 c^2\). 这意味着 \(b\) 也是偶数， 这和我们假设的事实，即 \(a / b\) 已约分到最简矛盾。

称 \(a / b\) 是最简分数意味着 \(a\) 和 \(b\) 没有任何公因子， 也就是说，它们是 互素 的。 Mathlib 把谓词 Nat.Coprime m n 定义为 Nat.gcd m n = 1. 使用 Lean 的匿名投影记号，如果 s 和 t 是 Nat 类型的表达式， 我们可以用 s.Coprime t 替代 Nat.Coprime s t, 而 Nat.gcd 也有类似的表达方式。 像往常一样，Lean 通常会在必要时自动展开 Nat.Coprime 的定义， 但我们也可以通过重写或简化标识符 Nat.Coprime 来手动操作。 norm_num 策略足够智能，可以计算具体值。

#print Nat.Coprime

example (m n : Nat) (h : m.Coprime n) : m.gcd n = 1 :=
  h

example (m n : Nat) (h : m.Coprime n) : m.gcd n = 1 := by
  rw [Nat.Coprime] at h
  exact h

example : Nat.Coprime 12 7 := by norm_num

example : Nat.gcd 12 8 = 4 := by norm_num

我们已经在 Section 2.4 中遇到过 gcd 函数。 还有一个用于整数的 gcd 版本； 我们将在下面回到不同数系之间关系的讨论中。 甚至还有广义 gcd 函数以及广义 Prime 和 Coprime 的概念， 它们在一般类型的代数结构中有意义。 我们将在下一章了解 Lean 是如何管理这种一般性的。 同时，在本节中，我们将把注意力限制到自然数。

我们还需要素数的概念， Nat.Prime. 定理 Nat.prime_def_lt 提供了一个熟悉的刻画， Nat.Prime.eq_one_or_self_of_dvd 提供了另一个。

#check Nat.prime_def_lt

example (p : ℕ) (prime_p : Nat.Prime p) : 2 ≤ p ∧ ∀ m : ℕ, m < p → m ∣ p → m = 1 := by
  rwa [Nat.prime_def_lt] at prime_p

#check Nat.Prime.eq_one_or_self_of_dvd

example (p : ℕ) (prime_p : Nat.Prime p) : ∀ m : ℕ, m ∣ p → m = 1 ∨ m = p :=
  prime_p.eq_one_or_self_of_dvd

example : Nat.Prime 17 := by norm_num

-- commonly used
example : Nat.Prime 2 :=
  Nat.prime_two

example : Nat.Prime 3 :=
  Nat.prime_three

在自然数中，素数具有不能写成非平凡因子的乘积的性质。 在更广泛的数学背景下，环中具有此性质的元素被称为 不可约 的。 环的元素称为 素元，如果每当它整除一个乘积时，它整除其中一个因子。 自然数的一个重要性质是，对它来说这两个概念是一致的， 这产生了定理 Nat.Prime.dvd_mul.

我们可以利用这个事实建立上面论证中的一个关键性质： 如果一个数的平方是偶数，那么这个数也是偶数。 Mathlib 在 Algebra.Group.Even 中定义了谓词 Even, 但出于下面会澄清的原因， 我们将简单地用 2 ∣ m 表示 m 是偶数。

#check Nat.Prime.dvd_mul
#check Nat.Prime.dvd_mul Nat.prime_two
#check Nat.prime_two.dvd_mul

theorem even_of_even_sqr {m : ℕ} (h : 2 ∣ m ^ 2) : 2 ∣ m := by
  rw [pow_two, Nat.prime_two.dvd_mul] at h
  cases h <;> assumption

example {m : ℕ} (h : 2 ∣ m ^ 2) : 2 ∣ m :=
  Nat.Prime.dvd_of_dvd_pow Nat.prime_two h

随着我们的继续，你将需要熟练地查找所需的事实。 请记住，如果你能猜出名称的前缀并且你已经导入了相关库， 你可以使用制表符补全（有时使用 ctrl-tab）来查找你在寻找的东西。 你可以在任何标识符上使用 ctrl-click 来跳转到文件中它的定义所在位置， 使你能够浏览附近的定义和定理。 你也可以使用 Lean community web pages 里的搜索引擎， 如果其他方法都失败了， 不要羞于向 Zulip 提问。

example (a b c : Nat) (h : a * b = a * c) (h' : a ≠ 0) : b = c :=
  -- apply? suggests the following:
  (mul_right_inj' h').mp h

我们对根号二无理性证明的核心包含在下列定理中。 看看你能不能填补这个证明梗概， 请使用 even_of_even_sqr 以及定理 Nat.dvd_gcd.

example {m n : ℕ} (coprime_mn : m.Coprime n) : m ^ 2 ≠ 2 * n ^ 2 := by
  intro sqr_eq
  have : 2 ∣ m := by
    sorry
  obtain ⟨k, meq⟩ := dvd_iff_exists_eq_mul_left.mp this
  have : 2 * (2 * k ^ 2) = 2 * n ^ 2 := by
    rw [← sqr_eq, meq]
    ring
  have : 2 * k ^ 2 = n ^ 2 :=
    sorry
  have : 2 ∣ n := by
    sorry
  have : 2 ∣ m.gcd n := by
    sorry
  have : 2 ∣ 1 := by
    sorry
  norm_num at this

事实上，只需很少的改变，我们就可以把 2 替换为任意素数。 在下一个例子中试一试。 在证明的末尾，你需要由 p ∣ 1 导出矛盾。 你可以使用 Nat.Prime.two_le, 它是说任意素数大于或等于二， 以及 Nat.le_of_dvd.

example {m n p : ℕ} (coprime_mn : m.Coprime n) (prime_p : p.Prime) : m ^ 2 ≠ p * n ^ 2 := by
  sorry

我们考虑另一种思路。 这是若 \(p\) 是素数则 \(m^2 \ne p n^2\) 的一个快速证明： 如果我们假设 \(m^2 = p n^2\), 考虑 \(m\) 和 \(n\) 的素分解， 则 \(p\) 在等式左边出现偶数次而在右边出现奇数次，矛盾。 注意到这个论证要求 \(n\), 从而 \(m\), 不等于零。 下面的形式化证实了这个假设是充分的。

唯一因子分解定理表明， 任何大于零的自然数可以用唯一的方式写成素数的乘积。 Mathlib 包含其形式化版本，使用函数 Nat.primeFactorsList 表达， 该函数以非递减顺序返回数的素因数列表。 此库证明了 Nat.factors n 的全部元素都是素数， 任意大于零的 n 等于它的因子的乘积， 以及若 n 等于另一列素数的乘积， 则这个列是 Nat.factors n 的一个排列。

#check Nat.primeFactorsList
#check Nat.prime_of_mem_primeFactorsList
#check Nat.prod_primeFactorsList
#check Nat.primeFactorsList_unique

你可以浏览这些定理和附近的其他定理， 即使我们还没有谈到列表成员、乘积或排列。 我们手头的任务不需要这些。 我们会使用 Mathlib 函数 Nat.factorization 作为替代品， 它把同样的数据表示为函数。 特别地，Nat.factorization n p, 也记为 n.factorization p, 返回 n 的素分解中 p 的重数。 我们将用到以下三个事实。

theorem factorization_mul' {m n : ℕ} (mnez : m ≠ 0) (nnez : n ≠ 0) (p : ℕ) :
    (m * n).factorization p = m.factorization p + n.factorization p := by
  rw [Nat.factorization_mul mnez nnez]
  rfl

theorem factorization_pow' (n k p : ℕ) :
    (n ^ k).factorization p = k * n.factorization p := by
  rw [Nat.factorization_pow]
  rfl

theorem Nat.Prime.factorization' {p : ℕ} (prime_p : p.Prime) :
    p.factorization p = 1 := by
  rw [prime_p.factorization]
  simp

事实上，n.factorization 在 Lean 中被定义为有限支集的函数， 这解释了你在逐步查看上述证明时会看到的奇怪符号。 现在不用担心这个。 出于我们这里的目的，我们可以将上面三个定理作为黑盒使用。

下一个示例表明化简器足够智能， 可以把 n^2 ≠ 0 替换为 n ≠ 0. 策略 simpa 不过是先调用 simp 接下来用 assumption.

看看你是否可以用上面的等式来填补证明缺失的部分。

example {m n p : ℕ} (nnz : n ≠ 0) (prime_p : p.Prime) : m ^ 2 ≠ p * n ^ 2 := by
  intro sqr_eq
  have nsqr_nez : n ^ 2 ≠ 0 := by simpa
  have eq1 : Nat.factorization (m ^ 2) p = 2 * m.factorization p := by
    sorry
  have eq2 : (p * n ^ 2).factorization p = 2 * n.factorization p + 1 := by
    sorry
  have : 2 * m.factorization p % 2 = (2 * n.factorization p + 1) % 2 := by
    rw [← eq1, sqr_eq, eq2]
  rw [add_comm, Nat.add_mul_mod_self_left, Nat.mul_mod_right] at this
  norm_num at this

这个证明的一个好处是它的可推广性。 2 没什么特别的；通过少量修改， 证明指出只要我们有 m^k = r * n^k, r 中素数 p 的重数就只能是 k 的倍数。

为了对 r * n^k 使用 Nat.count_factors_mul_of_pos, 我们需要知道 r 是正的。 但当 r 是零时，下面的定理是平凡的， 可使用化简器轻易证明。 所以证明是分情况进行的。 rcases r with _ | r 这一行把目标替换为两个版本： 一个把 r 替换为 0, 另一个把 r 替换为 r 的后继 r.succ. 在第二种情况下，我们可以应用定理 r.succ_ne_zero, 由它可得 r + 1 ≠ 0 （ succ 表示后继）

另请注意，以 have : npow_nz 开头的行提供了 n^k ≠ 0 的简短证明项证明。 要理解它是如何工作的，请尝试用策略证明替换它， 然后思考策略如何描述证明项。

看看你是否可以填补下列证明中缺失的部分。 在最后，你可以使用 Nat.dvd_sub' 和 Nat.dvd_mul_right 来收尾。

example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} :
    k ∣ r.factorization p := by
  rcases r with _ | r
  · simp
  have npow_nz : n ^ k ≠ 0 := fun npowz ↦ nnz (eq_zero_of_pow_eq_zero npowz)
  have eq1 : (m ^ k).factorization p = k * m.factorization p := by
    sorry
  have eq2 : ((r + 1) * n ^ k).factorization p =
      k * n.factorization p + (r + 1).factorization p := by
    sorry
  have : r.succ.factorization p = k * m.factorization p - k * n.factorization p := by
    rw [← eq1, pow_eq, eq2, add_comm, Nat.add_sub_cancel]
  rw [this]
  sorry

我们可能希望通过多种方式来改进这些结果。 首先，根号二是无理数的证明应该涉及一些和根号二相关的结论， 称它是无理数应该提到一些关于有理数的事情，即没有有理数等于它。 此外，我们应该将本节中的定理扩展到整数。 虽然数学上显而易见的是，如果我们可以将二的平方根写为两个整数的商， 那么我们就可以将其写为两个自然数的商， 但形式上证明这一点需要一些努力。

在 Mathlib 中，自然数、整数、有理数、实数和复数用不同的数据类型表示。 把注意力限制在单独的领域中常常是有帮助的： 我们将看到在自然数上做归纳法容易， 涉及整数的整除性的推理也很容易， 但实数就不在这些图景中。 但必须在不同领域中进行协调是我们将不得不面对的一个令人头疼的问题。 我们将在本章后面回到这个问题。

我们还应该期望能把上一个定理的结论加强为数 r 是 k 次幂， 因为它的 k 次根恰好是每个整除 r 的素数以 r 除以 k 的重数为幂次的幂的乘积。 为了能够做到这一点， 我们需要更好的方法来做关于有限集合上的乘积与和的推理， 这也是我们将要回到的话题。

事实上，本节中的结果都已经在 Mathlib 的 Data.Real.Irrational 中以远为广义的方式建立。 multiplicity 的概念在任意的交换幺半环上定义， 它的取值在扩展自然数 enat 中， 即在自然数中添加无穷值。 在下一章中， 我们将开始发展一些方法从而理解 Lean 支持这类一般性的途径。

5.2. 归纳和递归

自然数集 \(\mathbb{N} = \{ 0, 1, 2, \ldots \}\) 不仅仅在自身意义下具有基本的重要性， 也在构造新数学对象中扮演着中心角色。 Lean 底层允许我们声明 归纳类型， 它是由一个给定的 构造器 列表归纳地生成的类型。 在 Lean 中，自然数声明如下。

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

你可以通过输入 #check Nat 然后在标识符 Nat 上使用 ctrl-click 在库中找到这个声明。 这个命令指出 Nat 是由两个构造器 zero : Nat 和 succ : Nat → Nat 自由而归纳地生成的数据类型。 当然，库中引入了记号 ℕ 和 0 以分别表示 nat 和 zero. （数字被转化为二进制表示，但我们现在不必担心这些细节。）

对于当代数学家来说，“自由”意味着类型 Nat 有一个元素 zero 和一个单射后继函数 succ, 其像不包含 zero.

example (n : Nat) : n.succ ≠ Nat.zero :=
  Nat.succ_ne_zero n

example (m n : Nat) (h : m.succ = n.succ) : m = n :=
  Nat.succ.inj h

对于当代数学家来说， “归纳地”一词意味着自然数具有归纳证明法则和递归定义法则。 本节将展示如何运用这些法则。

这是一个阶乘函数的递归定义的示例。

def fac : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n + 1) * fac n

该语法需要一些时间来适应。 请注意，第一行没有 :=. 接下来的两行提供了基本情形和归纳步骤用于递归定义。 这些等式在定义上成立， 但它们也可以通过将名字 fac 送入 simp 或 rw 来手动使用。

example : fac 0 = 1 :=
  rfl

example : fac 0 = 1 := by
  rw [fac]

example : fac 0 = 1 := by
  simp [fac]

example (n : ℕ) : fac (n + 1) = (n + 1) * fac n :=
  rfl

example (n : ℕ) : fac (n + 1) = (n + 1) * fac n := by
  rw [fac]

example (n : ℕ) : fac (n + 1) = (n + 1) * fac n := by
  simp [fac]

阶乘函数实际上已经在 Mathlib 中被定义为 Nat.factorial. 再次提醒，你可以通过输入 #check Nat.factorial 并使用 ctrl-click 跳转到它。 出于演示目的，我们会在示例中继续使用 fac. Nat.factorial 的定义前面的标注 @[simp] 要求定义等式应被添加到化简器默认使用的恒等式数据库中。

归纳原理是说，我们要证明一个关于自然数的一般断言， 可以先证明该断言对 0 成立， 再证明只要它对自然数 \(n\) 成立， 它就对 \(n + 1\) 也成立。 因此下列证明中 induction' n with n ih 这一行将产生两个目标： 第一个是证明 0 < fac 0, 第二个是在附加假设 ih : 0 < fac n 的条件下证明 0 < fac (n + 1). 短语 with n ih 用于为变量和归纳假设命名， 你可以为它们选择你想要的任何名字。

theorem fac_pos (n : ℕ) : 0 < fac n := by
  induction' n with n ih
  · rw [fac]
    exact zero_lt_one
  rw [fac]
  exact mul_pos n.succ_pos ih

induction' 策略足够智能， 足以包含那些依赖于归纳变量，作为归纳假设的一部分的假设。 逐步考察下一个示例，看看发生了什么。

theorem dvd_fac {i n : ℕ} (ipos : 0 < i) (ile : i ≤ n) : i ∣ fac n := by
  induction' n with n ih
  · exact absurd ipos (not_lt_of_ge ile)
  rw [fac]
  rcases Nat.of_le_succ ile with h | h
  · apply dvd_mul_of_dvd_right (ih h)
  rw [h]
  apply dvd_mul_right

下面的例子提供了阶乘函数的一个粗略下界。 事实证明，从分情况证明开始更容易， 因此证明的剩余部分以 \(n = 1\) 这一情况开始。 看看你是否可以使用 pow_succ 或 pow_succ' 通过归纳证明来完成论证。

theorem pow_two_le_fac (n : ℕ) : 2 ^ (n - 1) ≤ fac n := by
  rcases n with _ | n
  · simp [fac]
  sorry

归纳法通常用于证明涉及有限和与乘积的恒等式。 Mathlib 定义了表达式 Finset.sum s f，其中 s : Finset α 是类型 α 的元素的有限集， f 是定义在 α 上的函数。 f 的到达域可以是任何支持交换、结合的加法运算且含有零元素的类型。 如果你导入 Algebra.BigOperators.Ring 并发出命令 open BigOperators，你可以使用更具暗示性的符号 ∑ x ∈ s, f x。当然，对于有限乘积也有类似的运算和符号。

我们将在下一节中讨论 Finset 类型和它支持的运算， 然后在一个后续章节中再次讨论。 现在，我们只会用到 Finset.range n, 它是小于 n 的自然数的有限集。

variable {α : Type*} (s : Finset ℕ) (f : ℕ → ℕ) (n : ℕ)

#check Finset.sum s f
#check Finset.prod s f

open BigOperators
open Finset

example : s.sum f = ∑ x ∈ s, f x :=
  rfl

example : s.prod f = ∏ x ∈ s, f x :=
  rfl

example : (range n).sum f = ∑ x ∈ range n, f x :=
  rfl

example : (range n).prod f = ∏ x ∈ range n, f x :=
  rfl

事实 Finset.sum_range_zero 和 Finset.sum_range_succ 提供了一直加到 \(n\) 的求和的递归描述， 乘积也类似。

example (f : ℕ → ℕ) : ∑ x ∈ range 0, f x = 0 :=
  Finset.sum_range_zero f

example (f : ℕ → ℕ) (n : ℕ) : ∑ x ∈ range n.succ, f x = ∑ x ∈ range n, f x + f n :=
  Finset.sum_range_succ f n

example (f : ℕ → ℕ) : ∏ x ∈ range 0, f x = 1 :=
  Finset.prod_range_zero f

example (f : ℕ → ℕ) (n : ℕ) : ∏ x ∈ range n.succ, f x = (∏ x ∈ range n, f x) * f n :=
  Finset.prod_range_succ f n

每对中的第一个恒等式是定义性成立的，也就是说， 你可以把证明替换为 rfl.

下面把我们定义的阶乘函数表示为乘积。

example (n : ℕ) : fac n = ∏ i ∈ range n, (i + 1) := by
  induction' n with n ih
  · simp [fac]
  simp [fac, ih, prod_range_succ, mul_comm]

我们在简化规则中包含 mul_comm 这一事实值得讨论。 使用恒等式 x * y = y * x 进行简化似乎很危险， 这通常会无限循环。 Lean 的化简器足够智能， 只会在对于任意项的某个固定的序， 结果项具有较小的值时才会应用这一规则。 下面的示例演示使用三个规则 mul_assoc, mul_comm 和 mul_left_comm 进行化简， 从而识别除了括号的位置和变量的顺序以外相同的乘积。

example (a b c d e f : ℕ) : a * (b * c * f * (d * e)) = d * (a * f * e) * (c * b) := by
  simp [mul_comm, mul_left_comm]

粗略地说，规则的工作原理是将括号向右推， 然后对两边的表达式重新排序， 直到两者都遵循相同的规范顺序。 用这些规则，以及相应的加法规则来化简，是一个方便的技巧。

回到求和等式，我们建议一步步完成下面的证明， 即一直加到 \(n\) （包括 \(n\) 在内）的自然数之和为 \(n (n + 1) / 2\). 证明的第一步是去分母。 这在形式化等式时通常很有用， 因为除法计算一般都有附带条件。 (尽可能避免在自然数上使用减法也同样有用）。

theorem sum_id (n : ℕ) : ∑ i ∈ range (n + 1), i = n * (n + 1) / 2 := by
  symm; apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
  induction' n with n ih
  · simp
  rw [Finset.sum_range_succ, mul_add 2, ← ih]
  ring

我们鼓励你证明平方和的类似等式， 以及你可以在网上找到的其他等式。

theorem sum_sqr (n : ℕ) : ∑ i ∈ range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6 := by
  sorry

在 Lean 的核心库中， 加法和乘法本身就是通过递归定义的， 其基本性质是通过归纳法建立的。 如果你喜欢思考这样的基础话题， 那么你可能会喜欢研究乘法和加法的交换性和结合性， 以及乘法对加法的分配性的证明。 你可以按照下面的提纲， 在自然数的副本上进行证明。 请注意，我们可以对 MyNat 使用 induction 策略； Lean 很聪明，知道使用相关的归纳法则 （当然，它与 Nat 的归纳法则相同）。

我们从加法的交换性开始。 一个很好的经验法则是， 由于加法和乘法是通过第二个参数上的递归来定义的， 所以一般来说， 通过对出现在该位置上的变量做归纳来进行证明是有利的。 在结合性证明中决定使用哪个变量有点技巧性。

如果不使用通常的符号来表示零、一、加法和乘法， 书写起来会很混乱。 我们稍后将学习如何定义这种符号。 在命名空间 MyNat 中工作意味着我们可以编写 zero 和 succ 而不是 MyNat.zero 和 MyNat.succ, 而且这些名字解释优先于其他解释。 在命名空间之外，例如，下面定义的 add 的全名是 MyNat.add.

如果你发现自己 真的 喜欢这类问题， 可以尝试定义截断减法和指数运算，并证明它们的一些性质。 请记住，截断减法的终点是零。 要定义截断减法，需要定义一个前继函数 pred, 从任何非零数中减去一并保持零不变。 函数 pred 可以通过一个简单的递归实例来定义。

inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat

namespace MyNat

def add : MyNat → MyNat → MyNat
  | x, zero => x
  | x, succ y => succ (add x y)

def mul : MyNat → MyNat → MyNat
  | _, zero => zero
  | x, succ y => add (mul x y) x

theorem zero_add (n : MyNat) : add zero n = n := by
  induction' n with n ih
  · rfl
  rw [add, ih]

theorem succ_add (m n : MyNat) : add (succ m) n = succ (add m n) := by
  induction' n with n ih
  · rfl
  rw [add, ih]
  rfl

theorem add_comm (m n : MyNat) : add m n = add n m := by
  induction' n with n ih
  · rw [zero_add]
    rfl
  rw [add, succ_add, ih]

theorem add_assoc (m n k : MyNat) : add (add m n) k = add m (add n k) := by
  sorry
theorem mul_add (m n k : MyNat) : mul m (add n k) = add (mul m n) (mul m k) := by
  sorry
theorem zero_mul (n : MyNat) : mul zero n = zero := by
  sorry
theorem succ_mul (m n : MyNat) : mul (succ m) n = add (mul m n) n := by
  sorry
theorem mul_comm (m n : MyNat) : mul m n = mul n m := by
  sorry
end MyNat

5.3. 素数无穷

让我们用另一个标准数学定理继续探索归纳和递归：证明素数有无穷多个。 一种表述方式是，对于每个自然数 \(n\), 都有一个大于 \(n\) 的素数。 为了证明这一点，令 \(p\) 是 \(n! + 1\) 的任意一个素因子。 若 \(p\) 小于等于 \(n\), 则它整除 \(n!\). 由于它也整除 \(n! + 1\), 它整除 1, 矛盾。 因此，\(p\) 大于 \(n\).

为了形式化这个证明， 我们需要论证任何大于或等于 2 的数都有一个素因数。 为此，我们需要证明任何不等于 0 或 1 的自然数都大于或等于 2. 这就给我们带来了形式化的一个古怪特征： 像这样琐碎的语句往往是最难形式化的。 在此，我们考虑几种方法。

首先，我们可以使用 cases 策略， 以及后继函数尊重自然数顺序这一事实。

theorem two_le {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := by
  cases m; contradiction
  case succ m =>
    cases m; contradiction
    repeat apply Nat.succ_le_succ
    apply zero_le

另一种方式是使用策略 interval_cases, 当相关变量包含在自然数或整数的区间内时， 它会自动将目标分割成不同的情况。 请记住，你可以将鼠标悬停在该策略上以查看其文档。

example {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := by
  by_contra h
  push_neg at h
  interval_cases m <;> contradiction

回想一下，interval_cases m 后面的分号表示下一个策略将应用于它生成的每种情况。 还有一种方法是使用 decide 策略， 该策略尝试找到一个决策过程来解决问题。 Lean 知道可以通过对有限个实例逐一进行判定， 来确定一个以有界量词 ∀ x, x < n → ... 或 ∃ x, x < n ∧ ... 开头的语句的真值。

example {m : ℕ} (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := by
  by_contra h
  push_neg at h
  revert h0 h1
  revert h m
  decide

手中有了 two_le 这个定理， 我们就可以从证明每个大于 2 的自然数都有一个素数除数开始。 Mathlib 包含一个函数 Nat.minFac, 它能返回最小的素数除数，但为了学习库的新部分， 我们将避免使用它，而是直接证明定理。

在这里，常规的归纳法是不够的。 我们需要用 强归纳法， 它允许我们通过证明对每个数 \(n\), 若性质 \(P\) 对所有小于 \(n\) 的值都成立， 则对 \(n\) 也成立， 来证明每个自然数 \(n\) 都有性质 \(P\). 在 Lean 中，这个原则被称为 Nat.strong_induction_on, 我们可以使用 using 关键字告诉归纳策略去使用它。 请注意，当我们这样做时，就没有归纳奠基了； 它已被一般归纳步骤所包含。

论证简述如下。假设 \(n≥2\), 如果 \(n\) 是素数，我们的证明就完成了。 如果不是，那么根据何为素数的刻画之一， 它有一个非平凡因子 \(m\), 我们就可以对其应用归纳假设。 分步查看下一个证明以观察其推理过程是如何完成的。

theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p ∣ n := by
  by_cases np : n.Prime
  · use n, np
  induction' n using Nat.strong_induction_on with n ih
  rw [Nat.prime_def_lt] at np
  push_neg at np
  rcases np h with ⟨m, mltn, mdvdn, mne1⟩
  have : m ≠ 0 := by
    intro mz
    rw [mz, zero_dvd_iff] at mdvdn
    linarith
  have mgt2 : 2 ≤ m := two_le this mne1
  by_cases mp : m.Prime
  · use m, mp
  · rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
    use p, pp
    apply pdvd.trans mdvdn

我们现在可以证明我们定理的下列表述形式。 看看你能否填补这个梗概。 你可以使用 Nat.factorial_pos, Nat.dvd_factorial, 以及 Nat.dvd_sub.

theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by
  intro n
  have : 2 ≤ Nat.factorial n + 1 := by
    sorry
  rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
  refine ⟨p, ?_, pp⟩
  show p > n
  by_contra ple
  push_neg at ple
  have : p ∣ Nat.factorial n := by
    sorry
  have : p ∣ 1 := by
    sorry
  show False
  sorry

让我们考虑上述证明的一种变式， 其中为了代替阶乘函数， 我们假设给定了一个有限集 \(\{ p_1, \ldots, p_n \}\), 考虑 \(\prod_{i = 1}^n p_i + 1\) 的一个素因子。 素因子必须不同于各个 \(p_i\), 这表明不存在包含全部素数的有限集。

形式化这一论证要求我们对有限集进行推理。 在 Lean 中，对于任意类型 α, 类型 Finset α 表示类型为 α 的元素的有限集。 要对有限集进行计算性推理，就要有一个流程来测试 α 中的相等性， 这就是为什么下面的片段包含了假设 [DecidableEq α]. 对于像 ℕ, ℤ 和 ℚ 这样的具体数据类型，假设自动成立。 在对实数进行推理时，为满足假设可以使用经典逻辑而放弃计算解释。

我们使用 open Finset 命令来为相关定理提供更短的名称。 不像集合的情况，绝大多数关于有限集的等价不是定义性成立的， 所以它们需要使用诸如 Finset.subset_iff, Finset.mem_union, Finset.mem_inter, 以及 Finset.mem_sdiff 这些等价来手动展开。 我们仍然可以使用 ext 策略， 把证明两个有限集合相等， 还原为证明其中任意一个集合的每个元素都是另一个集合的元素。

open Finset

section
variable {α : Type*} [DecidableEq α] (r s t : Finset α)

example : r ∩ (s ∪ t) ⊆ r ∩ s ∪ r ∩ t := by
  rw [subset_iff]
  intro x
  rw [mem_inter, mem_union, mem_union, mem_inter, mem_inter]
  tauto

example : r ∩ (s ∪ t) ⊆ r ∩ s ∪ r ∩ t := by
  simp [subset_iff]
  intro x
  tauto

example : r ∩ s ∪ r ∩ t ⊆ r ∩ (s ∪ t) := by
  simp [subset_iff]
  intro x
  tauto

example : r ∩ s ∪ r ∩ t = r ∩ (s ∪ t) := by
  ext x
  simp
  tauto

end

我们使用了一个新技巧：tauto 策略 （以及使用经典逻辑的加强版 tauto!） 可以用来免除命题重言式。 看看你能否用这些方法证明下面的两个例子。

example : (r ∪ s) ∩ (r ∪ t) = r ∪ s ∩ t := by
  sorry
example : (r \ s) \ t = r \ (s ∪ t) := by
  sorry

定理 Finset.dvd_prod_of_mem 告诉我们如果 n 是有限集 s 的元素， 那么 n 整除 ∏ i ∈ s, i.

example (s : Finset ℕ) (n : ℕ) (h : n ∈ s) : n ∣ ∏ i ∈ s, i :=
  Finset.dvd_prod_of_mem _ h

我们也需要知道在 n 是素数且 s 是素数集的情况下逆命题成立。 为了说明这一点，我们需要下列引理， 你可以使用定理 Nat.Prime.eq_one_or_self_of_dvd 证明它。

theorem _root_.Nat.Prime.eq_of_dvd_of_prime {p q : ℕ}
      (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) (h : p ∣ q) :
    p = q := by
  sorry

我们可以使用这个引理证明若素数 p 整除有限素数集的乘积， 则它整除其中一个素数。 Mathlib 提供了在有限集上做归纳的一个有用法则： 要证明某性质对任意有限集 s 成立， 先证明其对空集成立， 再证明当添加一个新元素 a ∉ s 时该性质保持成立。 这个法则被称为 Finset.induction_on. 当我们告诉归纳策略使用它时， 我们还可以指定 a 和 s 的名称， 归纳步骤中的假设 a ∉ s 的名称，以及归纳假设的名称。 表达式 Finset.insert a s 表示 s 和单元素集 a 的并。 然后，等式 Finset.prod_empty 和 Finset.prod_insert 为乘积提供了相关的重写法则。 在下面的证明中，第一个 simp 应用了 Finset.prod_empty. 逐步追踪证明的开头，观察归纳的展开，然后完成它。

theorem mem_of_dvd_prod_primes {s : Finset ℕ} {p : ℕ} (prime_p : p.Prime) :
    (∀ n ∈ s, Nat.Prime n) → (p ∣ ∏ n ∈ s, n) → p ∈ s := by
  intro h₀ h₁
  induction' s using Finset.induction_on with a s ans ih
  · simp at h₁
    linarith [prime_p.two_le]
  simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁
  rw [mem_insert]
  sorry

我们需要最后一个有限集性质。 给定一个元素 s : Set α 和 α 上的谓词 P, 在 Chapter 4 中， 我们用 { x ∈ s | P x } 表示满足 P 的元素的集合 s. 给定 s : Finset α, 类似的概念记为 s.filter P.

example (s : Finset ℕ) (x : ℕ) : x ∈ s.filter Nat.Prime ↔ x ∈ s ∧ x.Prime :=
  mem_filter

我们现在证明“素数有无穷多个”这一命题的另一种表述， 即给定任意 s : Finset ℕ, 存在一个素数 p 不是 s 的元素。 为了导出矛盾，我们假设所有素数都在 s 中， 然后缩减为一个仅包含所有素数的集合 s. 取该集合的乘积，加一，然后找到结果的一个素因数， 这通向了我们正在寻找的矛盾。 看看你能否完成下面的概要。 你可以在第一个 have 的证明中使用 Finset.prod_pos.

theorem primes_infinite' : ∀ s : Finset Nat, ∃ p, Nat.Prime p ∧ p ∉ s := by
  intro s
  by_contra h
  push_neg at h
  set s' := s.filter Nat.Prime with s'_def
  have mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime := by
    intro n
    simp [s'_def]
    apply h
  have : 2 ≤ (∏ i ∈ s', i) + 1 := by
    sorry
  rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
  have : p ∣ ∏ i ∈ s', i := by
    sorry
  have : p ∣ 1 := by
    convert Nat.dvd_sub pdvd this
    simp
  show False
  sorry

由此我们已经见过两种表达“有无穷多个素数”的方式： 说素数不以任何 n 为上界，和说它们不包含在任何有限集 s 中。 下面两个证明说明了这些表示方法是等价的。 在第二个证明中，为了构建 s.filter Q, 我们只好假定存在一个能决定 Q 是否成立的过程。Lean知道有一个用于 Nat.Prime 的过程。一般地， 如果我们键入 open Classical 以使用经典逻辑， 我们就可以省略这个假设。

在 Mathlib 中， Finset.sup s f 表示当 x 取遍 s 时 f x 的上确界， 而在 s 为空且 f 的到达域为 ℕ 时返回 0. 在第一个证明中，我们使用 s.sup id 表示 s 的最大值， 其中 id 是恒等函数。

theorem bounded_of_ex_finset (Q : ℕ → Prop) :
    (∃ s : Finset ℕ, ∀ k, Q k → k ∈ s) → ∃ n, ∀ k, Q k → k < n := by
  rintro ⟨s, hs⟩
  use s.sup id + 1
  intro k Qk
  apply Nat.lt_succ_of_le
  show id k ≤ s.sup id
  apply le_sup (hs k Qk)

theorem ex_finset_of_bounded (Q : ℕ → Prop) [DecidablePred Q] :
    (∃ n, ∀ k, Q k → k ≤ n) → ∃ s : Finset ℕ, ∀ k, Q k ↔ k ∈ s := by
  rintro ⟨n, hn⟩
  use (range (n + 1)).filter Q
  intro k
  simpa using hn k

我们对存在无穷多个素数的第二个证明做了一个小的改动， 表明有无穷多个模 4 余 3 的素数。 论证如下。 首先，注意到若两个数 \(m\) 和 \(n\) 的乘积模 4 等于 3, 那么两个数中有一个模 4 余 3. 毕竟，它们都是奇数，若它们都模 4 余 1, 那么它们的乘积也一样。 我们可以使用这个观察证明若某个大于 2 的数模 4 余 3, 那么那个数有一个模 4 余 3 的素因子。

现在假设只有有限多个素数模 4 余 3, 记为 \(p_1, \ldots, p_k\). 不失一般性，我们可以假设 \(p_1 = 3\). 考虑乘积 \(4 \prod_{i = 2}^k p_i + 3\). 容易看出这个乘积模 4 余 3, 因此它有一个模 4 余 3 的素因子 \(p\). 不可能是 \(p = 3\) 的情况； 由于 \(p\) 整除 \(4 \prod_{i = 2}^k p_i + 3\), 若 \(p\) 等于 3, 则它也整除 \(\prod_{i = 2}^k p_i\), 这意味着 \(p\) 等于 \(p_i\), \(i = 2, \ldots, k\) 中的一个； 而我们已经在这个列表中去掉了 3. 因此 \(p\) 只能是其余元素 \(p_i\) 中的一个。 但在那种情况下，\(p\) 整除 \(4 \prod_{i = 2}^k p_i\), 从而整除 3, 这和它不是 3 矛盾。

在 Lean 中，记号 n % m 读作 “n 模 m,” 表示 n 除以 m 的余数。

example : 27 % 4 = 3 := by norm_num

从此以后，我们可以把语句 “n 模 4 余 3” 表示为 n % 4 = 3. 以下示例和定理总结了我们将在下面需要使用的有关此函数的事实。 第一个具名的定理是通过少量情况进行推理的另一个例证。 在第二个具名定理中， 请记住分号表示后续策略块应用于前一个策略创建的所有目标。

example (n : ℕ) : (4 * n + 3) % 4 = 3 := by
  rw [add_comm, Nat.add_mul_mod_self_left]

theorem mod_4_eq_3_or_mod_4_eq_3 {m n : ℕ} (h : m * n % 4 = 3) : m % 4 = 3 ∨ n % 4 = 3 := by
  revert h
  rw [Nat.mul_mod]
  have : m % 4 < 4 := Nat.mod_lt m (by norm_num)
  interval_cases m % 4 <;> simp [-Nat.mul_mod_mod]
  have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
  interval_cases n % 4 <;> simp

theorem two_le_of_mod_4_eq_3 {n : ℕ} (h : n % 4 = 3) : 2 ≤ n := by
  apply two_le <;>
    · intro neq
      rw [neq] at h
      norm_num at h

我们也需要下列事实，它是说若 m 是 n 的一个非平凡因子， 那么 n / m 也是。 看看你能否使用 Nat.div_dvd_of_dvd 和 Nat.div_lt_self 完成证明。

theorem aux {m n : ℕ} (h₀ : m ∣ n) (h₁ : 2 ≤ m) (h₂ : m < n) : n / m ∣ n ∧ n / m < n := by
  sorry

现在把所有的部分放在一起来证明， 任何模 4 余 3 的数都有一个具有相同性质的素数因子。

theorem exists_prime_factor_mod_4_eq_3 {n : Nat} (h : n % 4 = 3) :
    ∃ p : Nat, p.Prime ∧ p ∣ n ∧ p % 4 = 3 := by
  by_cases np : n.Prime
  · use n
  induction' n using Nat.strong_induction_on with n ih
  rw [Nat.prime_def_lt] at np
  push_neg at np
  rcases np (two_le_of_mod_4_eq_3 h) with ⟨m, mltn, mdvdn, mne1⟩
  have mge2 : 2 ≤ m := by
    apply two_le _ mne1
    intro mz
    rw [mz, zero_dvd_iff] at mdvdn
    linarith
  have neq : m * (n / m) = n := Nat.mul_div_cancel' mdvdn
  have : m % 4 = 3 ∨ n / m % 4 = 3 := by
    apply mod_4_eq_3_or_mod_4_eq_3
    rw [neq, h]
  rcases this with h1 | h1
  . sorry
  . sorry

我们已经到了最后阶段。给定一个素数集 s, 我们需要谈论该集合删除 3 (如果存在)的结果。 函数 Finset.erase 可以处理这个问题。

example (m n : ℕ) (s : Finset ℕ) (h : m ∈ erase s n) : m ≠ n ∧ m ∈ s := by
  rwa [mem_erase] at h

example (m n : ℕ) (s : Finset ℕ) (h : m ∈ erase s n) : m ≠ n ∧ m ∈ s := by
  simp at h
  assumption

我们现在已经准备好证明存在无穷多个模 4 余 3 的素数。 填写下面缺失的部分。 我们的解答路径中使用了 Nat.dvd_add_iff_left 和 Nat.dvd_sub'.

theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, Nat.Prime p ∧ p % 4 = 3 := by
  by_contra h
  push_neg at h
  rcases h with ⟨n, hn⟩
  have : ∃ s : Finset Nat, ∀ p : ℕ, p.Prime ∧ p % 4 = 3 ↔ p ∈ s := by
    apply ex_finset_of_bounded
    use n
    contrapose! hn
    rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩
    exact ⟨p, pltn, pp, p4⟩
  rcases this with ⟨s, hs⟩
  have h₁ : ((4 * ∏ i ∈ erase s 3, i) + 3) % 4 = 3 := by
    sorry
  rcases exists_prime_factor_mod_4_eq_3 h₁ with ⟨p, pp, pdvd, p4eq⟩
  have ps : p ∈ s := by
    sorry
  have pne3 : p ≠ 3 := by
    sorry
  have : p ∣ 4 * ∏ i ∈ erase s 3, i := by
    sorry
  have : p ∣ 3 := by
    sorry
  have : p = 3 := by
    sorry
  contradiction

如果你成功完成了证明，那么恭喜你！这是形式化的一个重大成果。

5.4. 更多归纳

在 Section 5.2 中，我们看见了如何通过 对自然数进行递归来定义阶乘函数。

def fac : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n + 1) * fac n

我们也看见了如何使用 induction' 策略来证明定理。

theorem fac_pos (n : ℕ) : 0 < fac n := by
  induction' n with n ih
  · rw [fac]
    exact zero_lt_one
  rw [fac]
  exact mul_pos n.succ_pos ih

induction 策略（不带撇号）允许更具结构化的语法。

example (n : ℕ) : 0 < fac n := by
  induction n
  case zero =>
    rw [fac]
    exact zero_lt_one
  case succ n ih =>
    rw [fac]
    exact mul_pos n.succ_pos ih

example (n : ℕ) : 0 < fac n := by
  induction n with
  | zero =>
    rw [fac]
    exact zero_lt_one
  | succ n ih =>
    rw [fac]
    exact mul_pos n.succ_pos ih

像往常一样，你可以将鼠标悬停在 induction 关键字上以阅读文档。 情形 zero 和 succ 的名字取自类型 ℕ 的定义。 注意 succ 情形允许你为归纳变量和归纳假设 选择任何你想要的名字，这里分别是 n 和 ih。 你甚至可以用与定义递归函数相同的记号来证明一个定理。

theorem fac_pos' : ∀ n, 0 < fac n
  | 0 => by
    rw [fac]
    exact zero_lt_one
  | n + 1 => by
    rw [fac]
    exact mul_pos n.succ_pos (fac_pos' n)

还要注意这里没有 :=，冒号后面没有 ∀ n，每种情形中没有 by 关键字， 以及归纳中调用了 fac_pos' n。 这就好像这个定理是 n 的递归函数，而在归纳步骤中我们做了一个递归调用。

这种定义风格非常灵活。 Lean 的设计者们内置了精密的递归函数定义方法，而这些 方法也延伸到了用归纳法进行证明。 例如，我们可以用多个基本情形来定义斐波那契函数。

@[simp] def fib : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

@[simp] 标注意味着化简器会使用这些定义等式。 你也可以通过写 rw [fib] 来应用它们。 在下面，给 n + 2 的情形一个名字将会很有帮助。

theorem fib_add_two (n : ℕ) : fib (n + 2) = fib n + fib (n + 1) := rfl

example (n : ℕ) : fib (n + 2) = fib n + fib (n + 1) := by rw [fib]

使用 Lean 的递归函数记号，你可以对自然数进行归纳证明， 这些证明反映了 fib 的递归定义。 下面的例子给出了第 n 个斐波那契数关于 黄金比例 φ 及其共轭 φ' 的显式公式。 我们必须告诉 Lean，我们不期望我们的定义生成代码，因为 实数上的算术运算是不可计算的。

noncomputable section

def phi  : ℝ := (1 + √5) / 2
def phi' : ℝ := (1 - √5) / 2

theorem fib_eq : ∀ n, fib n = (phi^n - phi'^n) / √5
  | 0   => by simp
  | 1   => by unfold fib; grind [phi, phi']
  | n+2 => by unfold fib; simp; grind [fib_eq n, fib_eq (n+1), phi, phi']

end

涉及斐波那契函数的归纳证明不必是这种形式。 下面我们重现 Mathlib 中证明相邻斐波那契数互素的证明。

theorem fib_coprime_fib_succ (n : ℕ) : Nat.Coprime (fib n) (fib (n + 1)) := by
  induction n with
  | zero => simp
  | succ n ih =>
    simp only [fib, Nat.coprime_add_self_right]
    exact ih.symm

利用 Lean 的计算解释，我们可以计算斐波那契数。

#eval fib 6
#eval List.range 20 |>.map fib

fib 的直接实现在计算上是低效的。事实上，它的运行时间 随其参数指数增长。（你应该想想为什么。） 在 Lean 中，我们可以实现下面的尾递归版本，其运行时间关于 n 是线性的， 并证明它计算的是同一个函数。

def fib' (n : Nat) : Nat :=
  aux n 0 1
where aux
  | 0,   x, _ => x
  | n+1, x, y => aux n y (x + y)

theorem fib'.aux_eq (m n : ℕ) : fib'.aux n (fib m) (fib (m + 1)) = fib (n + m) := by
  induction n generalizing m with
  | zero => simp [fib'.aux]
  | succ n ih => rw [fib'.aux, ←fib_add_two, ih, add_assoc, add_comm 1]

theorem fib'_eq_fib : fib' = fib := by
  ext n
  erw [fib', fib'.aux_eq 0 n]; rfl

#eval fib' 10000

注意在 fib'.aux_eq 的证明中 generalizing 关键字的作用。 它用来在归纳假设前面插入一个 ∀ m，这样在归纳步骤中， m 可以取不同的值。 你可以逐步查看这个证明，并检验在这种情况下，量词需要在 归纳步骤中被实例化为 m + 1。

还要注意使用 erw （表示“扩展重写”）而不是 rw。 之所以使用它，是因为要重写目标 fib'.aux_eq，需要把 fib 0 和 fib 1 分别化简为 0 和 1。 erw 策略在展开定义以匹配参数方面比 rw 更激进。 这并不总是一个好主意；在某些情况下它会浪费大量时间，所以请谨慎使用 erw。

下面是 generalizing 关键字在另一个 Mathlib 中的恒等式证明里的另一个例子。 该恒等式的一个非形式化证明可以在 这里 找到。 我们提供了形式化证明的两个变体。

theorem fib_add (m n : ℕ) : fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1) := by
  induction n generalizing m with
  | zero => simp
  | succ n ih =>
    specialize ih (m + 1)
    rw [add_assoc m 1 n, add_comm 1 n] at ih
    simp only [fib_add_two, ih]
    ring

theorem fib_add' : ∀ m n, fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
  | _, 0     => by simp
  | m, n + 1 => by
    have := fib_add' (m + 1) n
    rw [add_assoc m 1 n, add_comm 1 n] at this
    simp only [fib_add_two, this]
    ring

作为练习，请使用 fib_add 来证明下面的结论。

example (n : ℕ): (fib n) ^ 2 + (fib (n + 1)) ^ 2 = fib (2 * n + 1) := by
  sorry

Lean 定义递归函数的机制足够灵活，允许任意的 递归调用，只要参数的复杂度按照某种 良基测度下降。 在下一个例子中，我们证明每个自然数 n ≠ 1 都有一个素因子， 利用了如果 n 非零且不是素数，它就有更小的因子这一事实。 （你可以检查 Mathlib 在 Nat 命名空间中有一个同名的定理， 不过它的证明与我们这里给出的不同。）

#check (@Nat.not_prime_iff_exists_dvd_lt :
  ∀ {n : ℕ}, 2 ≤ n → (¬Nat.Prime n ↔ ∃ m, m ∣ n ∧ 2 ≤ m ∧ m < n))

theorem ne_one_iff_exists_prime_dvd : ∀ {n}, n ≠ 1 ↔ ∃ p : ℕ, p.Prime ∧ p ∣ n
  | 0 => by simpa using Exists.intro 2 Nat.prime_two
  | 1 => by simp [Nat.not_prime_one]
  | n + 2 => by
    have hn : n + 2 ≠ 1 := by omega
    simp only [Ne, not_false_iff, true_iff, hn]
    by_cases h : Nat.Prime (n + 2)
    · use n + 2, h
    · have : 2 ≤ n + 2 := by omega
      rw [Nat.not_prime_iff_exists_dvd_lt this] at h
      rcases h with ⟨m, mdvdn, mge2, -⟩
      have : m ≠ 1 := by omega
      rw [ne_one_iff_exists_prime_dvd] at this
      rcases this with ⟨p, primep, pdvdm⟩
      use p, primep
      exact pdvdm.trans mdvdn

rw [ne_one_iff_exists_prime_dvd] at this 这一行就像一个魔术：我们在 自己的证明中使用了我们正在证明的定理本身。 使它起作用的是归纳调用被实例化在 m 上， 当前情形是 n + 2，而上下文中有 m < n + 2。 Lean 可以找到这个假设并用它来证明归纳是良基的。 Lean 非常善于找出什么是递减的；在这种情况下，定理陈述中 n 的选择以及小于关系是显而易见的。 在更复杂的情况下，Lean 提供了显式提供这一信息的机制。 请参阅 Lean 参考手册中关于 良基递归 的章节。

有时，在证明中，你需要根据自然数 n 是零还是后继来分情况，而在后继情形中不需要归纳假设。 为此，你可以使用 cases 和 rcases 策略。

theorem zero_lt_of_mul_eq_one (m n : ℕ) : n * m = 1 → 0 < n ∧ 0 < m := by
  cases n <;> cases m <;> simp

example (m n : ℕ) : n*m = 1 → 0 < n ∧ 0 < m := by
  rcases m with (_ | m); simp
  rcases n with (_ | n) <;> simp

这是一个有用的技巧。 经常你有一个关于自然数 n 的定理，其中零的情形很容易。 如果你对 n 进行分情况并迅速处理零的情形， 你就剩下了原来的目标，只不过 n 被替换成了 n + 1。