一道高考压轴数学题的 Lean 形式化证明

Some content in this article was created with AI assistance. Please verify as needed.

数学题目

问题（2008 年江西）

已知函数
$$
f(x) = \frac{1}{\sqrt{1+x}} + \frac{1}{\sqrt{1+a}} + \sqrt{\frac{ax}{ax+8}}, \qquad x\in(0,+\infty).
$$
求证：对任意正数 $a$，始终有 $1<f(x)<2$.

原问题可以自然转换为如下的三元不等式：

对任意满足 $u,v,w>0$, $uvw=8$ 的实数 $u,v,w$，证明
$$
1 < \frac1{\sqrt{1+u}} + \frac1{\sqrt{1+v}} + \frac1{\sqrt{1+w}} < 2.
$$

自然语言证明

下面用自然语言给出这道题的证明。

从证明的角度来说，下面的推导会显得非常啰嗦，但是这里的目的是为了与 Lean 代码中的四个引理/定理的证明内容保持对应。

根式改写（引理）

对任意 $t>0$，有恒等式

$$
\sqrt{\frac{t}{t+8}} = \frac1{\sqrt{1+\frac8t}}.
$$

这是因为 $1 + 8/t = (t+8)/t$，两边取平方根的倒数即得。

三元不等式下界（引理）

已知 $u,v,w>0$ 且 $uvw=8$. 令

$$
p=\frac1{\sqrt{1+u}}, \qquad q=\frac1{\sqrt{1+v}}, \qquad r=\frac1{\sqrt{1+w}}.
$$

由 $u>0$ 知 $\sqrt{1+u}>1$，从而 $p\in(0,1)$. 对 $q,r$ 同理，因此

$$
0<p,q,r<1.
$$

由 $p^2 = 1/(1+u)$ 得

$$
1-p^2 = u p^2.
$$

同理

$$
1-q^2 = v q^2, 1-r^2 = w r^2.
$$

三式相乘并利用 $uvw=8$：

$$
(1-p^2)(1-q^2)(1-r^2) = 8p^2q^2r^2. \tag{1}
$$

下面证明 $p+q+r>1$. 反设 $p+q+r \le 1$.

由 $q(1-r)>0$, $r(1-q)>0$ 相加得

$$
2qr < q+r.
$$

结合假设有

$$
2qr < 1-p.
$$

又因为

$$
1-p^2 = (1-p)(1+p) > 1-p.
$$

故

$$
2qr < 1-p^2.
$$

循环得

$$
2pr < 1-q^2, 2pq < 1-r^2.
$$

三式相乘：

$$
(2qr)(2pr)(2pq) < (1-p^2)(1-q^2)(1-r^2).
$$

左边即 $8p^2q^2r^2$，与式 (1) 矛盾。故 $p+q+r>1$.

三元不等式上界（引理）

前置条件与下界相同（同一定义 $p,q,r$，同一乘积恒等式 (1)）。下面证明 $p+q+r<2$.

反设 $p+q+r \ge 2$.

由 $(1-q)(1-r)>0$ 得

$$
q+r-1 < qr.
$$

结合假设有 $1-p < qr$.

又因为

$$
1+p<2.
$$

故

$$
1-p^2 = (1-p)(1+p) < 2qr.
$$

循环得

$$
1-q^2 < 2pr, 1-r^2 < 2pq.
$$

三式相乘：

$$
(1-p^2)(1-q^2)(1-r^2) < (2qr)(2pr)(2pq) = 8p^2q^2r^2,
$$

与式 (1) 矛盾。故 $p+q+r<2$.

原题（定理）

取 $u=x$, $v=a$, $w=8/(ax)$. 由 $a,x>0$ 知 $u,v,w>0$，且 $uvw = 8$.

原式第三项可以改写为：

$$
\sqrt{(a x)/(a x+8)} = 1/\sqrt{1+8/(a x)}.
$$

于是原式化为

$$
\frac1{\sqrt{1+u}} + \frac1{\sqrt{1+v}} + \frac1{\sqrt{1+w}}.
$$

由下界引理知其 $>1$，由上界引理知其 $<2$，原不等式得证。

Lean 证明

证明分成四个部分：

• sqrt_ratio_eq_inv_sqrt：根式改写引理。
• three_variable_gt_one：三元不等式下界，纯代数证明。
• three_variable_lt_two：三元不等式上界，纯代数证明。
• jiangxi_2008：主定理，完成变量代换并调用以上三个引理。

完整源码如下：

import Mathlib

/-!
# 2008 年江西高考根式不等式

设 a > 0, x > 0，证明

  1 <
    1 / sqrt (1 + x)
      + 1 / sqrt (1 + a)
      + sqrt (a*x / (a*x + 8))
  < 2.

形式化分成四个部分：

1. `sqrt_ratio_eq_inv_sqrt`
   证明第三项所需的根式恒等式。

2. `three_variable_gt_one`
   三元不等式下界 p+q+r > 1（纯代数证明）。

3. `three_variable_lt_two`
   三元不等式上界 p+q+r < 2（纯代数证明）。

4. `jiangxi_2008`
   主定理：完成变量代换，代入以上引理。
-/


/--
# `sqrt_ratio_eq_inv_sqrt`：根式改写

对任意 t > 0，有恒等式：

  √(t/(t+8)) = 1/√(1+8/t).

这是因为 1 + 8/t = (t+8)/t，两边取平方根的倒数即得.
-/
lemma sqrt_ratio_eq_inv_sqrt
    (t : ℝ)
    (ht : 0 < t) :
    Real.sqrt (t / (t + 8))
      =
    1 / Real.sqrt (1 + 8 / t) := by

  have ht8 : 0 < t + 8 := by
    linarith

  /-
  首先证明

    1 + 8/t = (t+8)/t.
  -/

  have hrewrite :
      1 + 8 / t = (t + 8) / t := by
    field_simp [ne_of_gt ht]

  /-
  分别使用

    sqrt(x/y) = sqrt(x)/sqrt(y)

  改写等式两边。
  -/

  rw [Real.sqrt_div (le_of_lt ht)]
  rw [hrewrite]
  rw [Real.sqrt_div (le_of_lt ht8)]

  /-
  为 field_simp 提供两个平方根非零的条件。
  -/

  have hsqrt_t :
      Real.sqrt t ≠ 0 := by
    exact ne_of_gt (Real.sqrt_pos_of_pos ht)

  have hsqrt_t8 :
      Real.sqrt (t + 8) ≠ 0 := by
    exact ne_of_gt (Real.sqrt_pos_of_pos ht8)

  field_simp [hsqrt_t, hsqrt_t8]


/--
# `three_variable_gt_one`：三元不等式下界

已知 u,v,w > 0 且 uvw = 8. 令 p = 1/√(1+u), q = 1/√(1+v), r = 1/√(1+w).

由 u > 0 知 √(1+u) > 1，从而 p ∈ (0,1). 对 q,r 同理.

由 p² = 1/(1+u) 可得 1-p² = u·p². 同理 1-q² = v·q², 1-r² = w·r².
三式相乘并利用 uvw = 8：

  (1-p²)(1-q²)(1-r²) = (uvw)(p²q²r²) = 8p²q²r².

反设 p+q+r ≤ 1，通过不等式放大和相乘导出 8p²q²r² < (1-p²)(1-q²)(1-r²)，
与上式矛盾. 故 1 < p+q+r.
-/
lemma three_variable_gt_one
    {p q r : ℝ}
    (hp0 : 0 < p)
    (hp1 : p < 1)
    (hq0 : 0 < q)
    (hq1 : q < 1)
    (hr0 : 0 < r)
    (hr1 : r < 1)
    (hprod :
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2)
        =
      8 * p ^ 2 * q ^ 2 * r ^ 2) :
    1 < p + q + r := by

  /-
  首先证明各平方差严格为正.
  -/

  have hpSq : 0 < 1 - p ^ 2 := by
    have h :
        0 < (1 - p) * (1 + p) := by
      apply mul_pos
      · exact sub_pos.mpr hp1
      · linarith
    nlinarith

  have hqSq : 0 < 1 - q ^ 2 := by
    have h :
        0 < (1 - q) * (1 + q) := by
      apply mul_pos
      · exact sub_pos.mpr hq1
      · linarith
    nlinarith

  have hrSq : 0 < 1 - r ^ 2 := by
    have h :
        0 < (1 - r) * (1 + r) := by
      apply mul_pos
      · exact sub_pos.mpr hr1
      · linarith
    nlinarith

  /-
  乘积 2*q*r, 2*p*r, 2*p*q 都严格为正.
  -/

  have h2qr : 0 < 2 * q * r := by
    positivity

  have h2pr : 0 < 2 * p * r := by
    positivity

  have h2pq : 0 < 2 * p * q := by
    positivity

  /-
  反设 p+q+r ≤ 1.
  -/

  by_contra h

  have hsum : p + q + r ≤ 1 := by
    exact le_of_not_gt h

  /-
  由 q(1-r) + r(1-q) > 0 得到 2qr < q+r.
  -/

  have hqr : 2 * q * r < q + r := by
    have h1 : 0 < q * (1 - r) := by
      apply mul_pos hq0
      exact sub_pos.mpr hr1

    have h2 : 0 < r * (1 - q) := by
      apply mul_pos hr0
      exact sub_pos.mpr hq1

    nlinarith

  have hpr : 2 * p * r < p + r := by
    have h1 : 0 < p * (1 - r) := by
      apply mul_pos hp0
      exact sub_pos.mpr hr1

    have h2 : 0 < r * (1 - p) := by
      apply mul_pos hr0
      exact sub_pos.mpr hp1

    nlinarith

  have hpq : 2 * p * q < p + q := by
    have h1 : 0 < p * (1 - q) := by
      apply mul_pos hp0
      exact sub_pos.mpr hq1

    have h2 : 0 < q * (1 - p) := by
      apply mul_pos hq0
      exact sub_pos.mpr hp1

    nlinarith

  /-
  由 p+q+r ≤ 1 以及 2qr < q+r，得到 2qr < 1-p.
  循环地得到另外两个不等式.
  -/

  have hp' : 2 * q * r < 1 - p := by
    linarith

  have hq' : 2 * p * r < 1 - q := by
    linarith

  have hr' : 2 * p * q < 1 - r := by
    linarith

  /-
  从 2qr < 1-p 推出 2qr < 1-p^2.
  利用 1-p^2 = (1-p) + p(1-p) 且 p(1-p) > 0.
  -/

  have hp : 2 * q * r < 1 - p ^ 2 := by
    have haux : 0 < p * (1 - p) := by
      apply mul_pos hp0
      exact sub_pos.mpr hp1
    nlinarith

  have hq : 2 * p * r < 1 - q ^ 2 := by
    have haux : 0 < q * (1 - q) := by
      apply mul_pos hq0
      exact sub_pos.mpr hq1
    nlinarith

  have hr : 2 * p * q < 1 - r ^ 2 := by
    have haux : 0 < r * (1 - r) := by
      apply mul_pos hr0
      exact sub_pos.mpr hr1
    nlinarith

  /-
  Lean 不会自动将三个严格不等式直接相乘.
  因此先乘前两个：(2qr)(2pr) < (1-p^2)(1-q^2).
  -/

  have hpq_mul :
      (2 * q * r) * (2 * p * r)
        <
      (1 - p ^ 2) * (1 - q ^ 2) := by
    calc
      (2 * q * r) * (2 * p * r)
          <
      (1 - p ^ 2) * (2 * p * r) := by
        exact mul_lt_mul_of_pos_right hp h2pr

      _ <
      (1 - p ^ 2) * (1 - q ^ 2) := by
        exact mul_lt_mul_of_pos_left hq hpSq

  /-
  再乘第三个不等式.
  -/

  have hpqr_mul :
      (2 * q * r) * (2 * p * r) * (2 * p * q)
        <
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2) := by
    calc
      (2 * q * r) * (2 * p * r) * (2 * p * q)
          <
      ((1 - p ^ 2) * (1 - q ^ 2)) * (2 * p * q) := by
        exact mul_lt_mul_of_pos_right hpq_mul h2pq

      _ <
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2) := by
        exact
          mul_lt_mul_of_pos_left
            hr
            (mul_pos hpSq hqSq)

  /-
  左边整理为 8 p^2 q^2 r^2，与 hprod 矛盾.
  -/

  have hcontra :
      8 * p ^ 2 * q ^ 2 * r ^ 2
        <
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2) := by
    calc
      8 * p ^ 2 * q ^ 2 * r ^ 2
          =
      (2 * q * r) * (2 * p * r) * (2 * p * q) := by
        ring

      _ <
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2) := by
        exact hpqr_mul

  nlinarith [hprod]


/--
# `three_variable_lt_two`：三元不等式上界

前置条件与 `three_variable_gt_one` 相同：0 < p,q,r < 1 且乘积恒等式成立.

反设 p+q+r ≥ 2，通过不等式放大和相乘导出 (1-p²)(1-q²)(1-r²) < 8p²q²r²，
与乘积恒等式矛盾. 故 p+q+r < 2.
-/
lemma three_variable_lt_two
    {p q r : ℝ}
    (hp0 : 0 < p)
    (hp1 : p < 1)
    (hq0 : 0 < q)
    (hq1 : q < 1)
    (hr0 : 0 < r)
    (hr1 : r < 1)
    (hprod :
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2)
        =
      8 * p ^ 2 * q ^ 2 * r ^ 2) :
    p + q + r < 2 := by

  /-
  首先证明各平方差严格为正.
  -/

  have hpSq : 0 < 1 - p ^ 2 := by
    have h :
        0 < (1 - p) * (1 + p) := by
      apply mul_pos
      · exact sub_pos.mpr hp1
      · linarith
    nlinarith

  have hqSq : 0 < 1 - q ^ 2 := by
    have h :
        0 < (1 - q) * (1 + q) := by
      apply mul_pos
      · exact sub_pos.mpr hq1
      · linarith
    nlinarith

  have hrSq : 0 < 1 - r ^ 2 := by
    have h :
        0 < (1 - r) * (1 + r) := by
      apply mul_pos
      · exact sub_pos.mpr hr1
      · linarith
    nlinarith

  /-
  乘积 2*q*r, 2*p*r, 2*p*q 都严格为正.
  -/

  have h2qr : 0 < 2 * q * r := by
    positivity

  have h2pr : 0 < 2 * p * r := by
    positivity

  have h2pq : 0 < 2 * p * q := by
    positivity

  /-
  反设 2 ≤ p+q+r.
  -/

  by_contra h

  have hsum : 2 ≤ p + q + r := by
    exact le_of_not_gt h

  /-
  由 (1-q)(1-r) > 0 得到 q+r-1 < qr.
  -/

  have hqr_aux : q + r - 1 < q * r := by
    have haux :
        0 < (1 - q) * (1 - r) := by
      apply mul_pos
      · exact sub_pos.mpr hq1
      · exact sub_pos.mpr hr1

    nlinarith

  have hpr_aux : p + r - 1 < p * r := by
    have haux :
        0 < (1 - p) * (1 - r) := by
      apply mul_pos
      · exact sub_pos.mpr hp1
      · exact sub_pos.mpr hr1

    nlinarith

  have hpq_aux : p + q - 1 < p * q := by
    have haux :
        0 < (1 - p) * (1 - q) := by
      apply mul_pos
      · exact sub_pos.mpr hp1
      · exact sub_pos.mpr hq1

    nlinarith

  /-
  由 2 ≤ p+q+r 可得 1-p ≤ q+r-1.
  再结合 q+r-1 < qr，得到 1-p < qr.
  -/

  have hp' : 1 - p < q * r := by
    linarith

  have hq' : 1 - q < p * r := by
    linarith

  have hr' : 1 - r < p * q := by
    linarith

  /-
  由 1-p < qr, 1+p < 2 得到 1-p^2 < 2qr.
  -/

  have hp : 1 - p ^ 2 < 2 * q * r := by
    calc
      1 - p ^ 2
          =
      (1 - p) * (1 + p) := by
        ring

      _ <
      (q * r) * (1 + p) := by
        exact
          mul_lt_mul_of_pos_right
            hp'
            (by linarith)

      _ <
      (q * r) * 2 := by
        exact
          mul_lt_mul_of_pos_left
            (by linarith)
            (mul_pos hq0 hr0)

      _ = 2 * q * r := by
        ring

  have hq : 1 - q ^ 2 < 2 * p * r := by
    calc
      1 - q ^ 2
          =
      (1 - q) * (1 + q) := by
        ring

      _ <
      (p * r) * (1 + q) := by
        exact
          mul_lt_mul_of_pos_right
            hq'
            (by linarith)

      _ <
      (p * r) * 2 := by
        exact
          mul_lt_mul_of_pos_left
            (by linarith)
            (mul_pos hp0 hr0)

      _ = 2 * p * r := by
        ring

  have hr : 1 - r ^ 2 < 2 * p * q := by
    calc
      1 - r ^ 2
          =
      (1 - r) * (1 + r) := by
        ring

      _ <
      (p * q) * (1 + r) := by
        exact
          mul_lt_mul_of_pos_right
            hr'
            (by linarith)

      _ <
      (p * q) * 2 := by
        exact
          mul_lt_mul_of_pos_left
            (by linarith)
            (mul_pos hp0 hq0)

      _ = 2 * p * q := by
        ring

  /-
  分两次将三个不等式相乘.
  -/

  have hpq_mul :
      (1 - p ^ 2) * (1 - q ^ 2)
        <
      (2 * q * r) * (2 * p * r) := by
    calc
      (1 - p ^ 2) * (1 - q ^ 2)
          <
      (2 * q * r) * (1 - q ^ 2) := by
        exact mul_lt_mul_of_pos_right hp hqSq

      _ <
      (2 * q * r) * (2 * p * r) := by
        exact mul_lt_mul_of_pos_left hq h2qr

  have hpqr_mul :
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2)
        <
      (2 * q * r) * (2 * p * r) * (2 * p * q) := by
    calc
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2)
          <
      ((2 * q * r) * (2 * p * r)) * (1 - r ^ 2) := by
        exact mul_lt_mul_of_pos_right hpq_mul hrSq

      _ <
      (2 * q * r) * (2 * p * r) * (2 * p * q) := by
        exact
          mul_lt_mul_of_pos_left
            hr
            (mul_pos h2qr h2pr)

  have hcontra :
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2)
        <
      8 * p ^ 2 * q ^ 2 * r ^ 2 := by
    calc
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2)
          <
      (2 * q * r) * (2 * p * r) * (2 * p * q) := by
        exact hpqr_mul

      _ =
      8 * p ^ 2 * q ^ 2 * r ^ 2 := by
        ring

  nlinarith [hprod]


/--
# `jiangxi_2008`：原题

取 u = x, v = a, w = 8/(a*x). 由 a,x > 0 知 u,v,w > 0，且 uvw = x·a·8/(a·x) = 8.

定义 p = 1/√(1+u), q = 1/√(1+v), r = 1/√(1+w).
验证 0 < p,q,r < 1 以及乘积恒等式 (1-p²)(1-q²)(1-r²) = 8p²q²r².

原式第三项按 `sqrt_ratio_eq_inv_sqrt` 改写为 1/√(1+8/(a*x)).
于是原式 = p+q+r，由 `three_variable_gt_one` 知 > 1，由 `three_variable_lt_two` 知 < 2.
-/
theorem jiangxi_2008
    (a x : ℝ)
    (ha : 0 < a)
    (hx : 0 < x) :
    1
        <
      1 / Real.sqrt (1 + x)
        + 1 / Real.sqrt (1 + a)
        + Real.sqrt (a * x / (a * x + 8))
    ∧
      1 / Real.sqrt (1 + x)
        + 1 / Real.sqrt (1 + a)
        + Real.sqrt (a * x / (a * x + 8))
        < 2 := by

  /-
  因为 a > 0 且 x > 0，所以 a*x > 0.
  -/

  have hax : 0 < a * x :=
    mul_pos ha hx

  /-
  改写第三项根式.
  -/

  rw [sqrt_ratio_eq_inv_sqrt (a * x) hax]

  /-
  令 u = x, v = a, w = 8/(a*x) 并定义 p,q,r.
  -/

  let u := x
  let v := a
  let w := 8 / (a * x)

  have hu : 0 < u := hx
  have hv : 0 < v := ha
  have hw : 0 < w := div_pos (by norm_num) hax

  have huvw : u * v * w = 8 := by
    dsimp [u, v, w]
    field_simp [ne_of_gt ha, ne_of_gt hx]

  let p := 1 / Real.sqrt (1 + u)
  let q := 1 / Real.sqrt (1 + v)
  let r := 1 / Real.sqrt (1 + w)

  /-
  证明各平方根严格为正：√(1+u) > 0 等.
  -/

  have hsu0 : 0 < Real.sqrt (1 + u) :=
    Real.sqrt_pos_of_pos (by linarith)

  have hsv0 : 0 < Real.sqrt (1 + v) :=
    Real.sqrt_pos_of_pos (by linarith)

  have hsw0 : 0 < Real.sqrt (1 + w) :=
    Real.sqrt_pos_of_pos (by linarith)

  /-
  证明 √(1+u) > 1 等（由 u > 0 得 1+u > 1，平方根严格单调）.
  -/

  have hsu1 : 1 < Real.sqrt (1 + u) := by
    calc
      1 = Real.sqrt 1 := by norm_num
      _ < Real.sqrt (1 + u) := by
        apply Real.sqrt_lt_sqrt
        · norm_num
        · linarith

  have hsv1 : 1 < Real.sqrt (1 + v) := by
    calc
      1 = Real.sqrt 1 := by norm_num
      _ < Real.sqrt (1 + v) := by
        apply Real.sqrt_lt_sqrt
        · norm_num
        · linarith

  have hsw1 : 1 < Real.sqrt (1 + w) := by
    calc
      1 = Real.sqrt 1 := by norm_num
      _ < Real.sqrt (1 + w) := by
        apply Real.sqrt_lt_sqrt
        · norm_num
        · linarith

  /-
  证明 0 < p,q,r < 1.
  -/

  have hp0 : 0 < p := by
    dsimp [p]; exact div_pos (by norm_num) hsu0

  have hq0 : 0 < q := by
    dsimp [q]; exact div_pos (by norm_num) hsv0

  have hr0 : 0 < r := by
    dsimp [r]; exact div_pos (by norm_num) hsw0

  have hp1 : p < 1 := by
    dsimp [p]; exact (div_lt_one hsu0).2 hsu1

  have hq1 : q < 1 := by
    dsimp [q]; exact (div_lt_one hsv0).2 hsv1

  have hr1 : r < 1 := by
    dsimp [r]; exact (div_lt_one hsw0).2 hsw1

  /-
  计算 p², q², r²：p² = 1/(1+u) 等.
  -/

  have hp2 : p ^ 2 = 1 / (1 + u) := by
    dsimp [p]
    rw [div_pow, Real.sq_sqrt (by linarith : 0 ≤ 1 + u)]
    norm_num

  have hq2 : q ^ 2 = 1 / (1 + v) := by
    dsimp [q]
    rw [div_pow, Real.sq_sqrt (by linarith : 0 ≤ 1 + v)]
    norm_num

  have hr2 : r ^ 2 = 1 / (1 + w) := by
    dsimp [r]
    rw [div_pow, Real.sq_sqrt (by linarith : 0 ≤ 1 + w)]
    norm_num

  /-
  推导 1-p² = u·p² 等（用于代入 uvw = 8）.
  -/

  have hup : 1 - p ^ 2 = u * p ^ 2 := by
    rw [hp2]
    field_simp [ne_of_gt (show 0 < 1 + u by linarith)]
    ring

  have hvq : 1 - q ^ 2 = v * q ^ 2 := by
    rw [hq2]
    field_simp [ne_of_gt (show 0 < 1 + v by linarith)]
    ring

  have hwr : 1 - r ^ 2 = w * r ^ 2 := by
    rw [hr2]
    field_simp [ne_of_gt (show 0 < 1 + w by linarith)]
    ring

  /-
  乘积恒等式：(1-p²)(1-q²)(1-r²) = 8p²q²r².
  -/

  have hprod :
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2)
        =
      8 * p ^ 2 * q ^ 2 * r ^ 2 := by
    calc
      (1 - p ^ 2) * (1 - q ^ 2) * (1 - r ^ 2)
          =
      (u * p ^ 2) * (v * q ^ 2) * (w * r ^ 2) := by
        rw [hup, hvq, hwr]
      _ =
      (u * v * w) * (p ^ 2 * q ^ 2 * r ^ 2) := by
        ring
      _ =
      8 * (p ^ 2 * q ^ 2 * r ^ 2) := by
        rw [huvw]
      _ =
      8 * p ^ 2 * q ^ 2 * r ^ 2 := by
        ring

  /-
  分别应用上下界引理，再展开 p,q,r,u,v,w 的定义.
  -/

  have h_gt_one : 1 < p + q + r :=
    three_variable_gt_one hp0 hp1 hq0 hq1 hr0 hr1 hprod

  have h_lt_two : p + q + r < 2 :=
    three_variable_lt_two hp0 hp1 hq0 hq1 hr0 hr1 hprod

  exact And.intro (by simpa [p, q, r, u, v, w] using h_gt_one)
                  (by simpa [p, q, r, u, v, w] using h_lt_two)

关键命令说明

ring 用于验证交换环中的多项式恒等式。例如

(2 * q * r) * (2 * p * r) * (2 * p * q)
  =
8 * p ^ 2 * q ^ 2 * r ^ 2

对人而言只需直接展开；在 Lean 中可以写成 by ring.

field_simp 用于清除分母。例如证明

$$
1 - \frac1{1+u} = u \frac1{1+u}
$$

Lean 需要明确知道 $1+u \ne 0$。因此代码写成

field_simp [
  ne_of_gt (show 0 < 1 + u by linarith)
]
<;> ring

nlinarith 适合处理多项式形式的等式和不等式。例如，由 $q(1-r)>0$, $r(1-q)>0$ 推出 $2qr<q+r$，可以写成 nlinarith.

不过，nlinarith 通常不会自动完成这样的推理：

$$
a<b,; c<d ;\Longrightarrow; ac<bd,
$$

因为该结论还依赖各个因子的正负性。因此在代码中，严格不等式相乘仍然需要显式使用 mul_lt_mul_of_pos_left 和 mul_lt_mul_of_pos_right.

positivity 用于自动证明由已知正数构成的表达式仍然为正。例如，已知 hq0 : 0 < q 和 hr0 : 0 < r 以后，可以自动证明

have h2qr : 0 < 2 * q * r := by
  positivity

但对于更复杂的正性问题，仍然需要手动给出证明。