18.2.1. 关键引理🔗

-- field_simp 使用的核心引理（来自 Mathlib）
theorem div_add_div (a : α) (c : α) {b d : α}          -- ❶
    (hb : b ≠ 0) (hd : d ≠ 0) :
    a / b + c / d = (a * d + b * c) / (b * d)

theorem div_eq_iff {b : α} (hb : b ≠ 0) :              -- ❷
    a / b = c ↔ a = c * b

theorem div_div {a b c : α} :                           -- ❸
    a / b / c = a / (b * c)

• ❶ 通分引理：两个分式相加。

• ❷ 消分母引理：等式两侧同乘分母。

• ❸ 嵌套除法引理：(a/b)/c 化为 a/(b*c)。

18.4.1. 情况 1：field_simp → ring🔗

最常见的模式——field_simp 消分母，ring 处理多项式等式：

18.4.2. 情况 2：field_simp 直接关闭🔗

有时消分母后目标直接成立，不需要 ring：

注意：如果 field_simp 已经关闭目标，再写 ring 会报 no goals。 先试 field_simp，看是否还有剩余目标再决定后续步骤。

18.4.3. 情况 3：需要补充非零条件🔗

• ❶ a ^ 2 ≠ 0 不总能被自动推导，有时需要手动提供。

18.4.4. 工作流决策树🔗

field_simp 之后：
  │
  ├─ 目标已关闭？     → 结束（不要写 ring）
  │
  ├─ 剩余多项式等式？ → 接 ring
  │
  ├─ 剩余不等式？     → 接 linarith / nlinarith / positivity
  │
  └─ 产生 side goals（x ≠ 0 等）？ → 用假设 / positivity / norm_num 关闭

18.5.1. 失败 1：缺少非零条件🔗

-- [会报错] 分母非零性无法推导
example (x : ℝ) : 1 / x * x = 1 := by field_simp
  -- ▸ field_simp 无法证明 x ≠ 0
  -- ▸ 修复：添加假设 (hx : x ≠ 0)

这是最常见的失败。field_simp 不会"假设"分母非零—— 它必须从上下文中证明每一个分母非零。

18.5.2. 失败 2：复合分母不被识别🔗

-- [会报错] x + y 的非零性无法自动推导
example (x y : ℝ) : 1 / (x + y) + 1 = (x + y + 1) / (x + y) := by
  field_simp
  -- ▸ 修复方案 1：添加假设 (h : x + y ≠ 0)
  -- ▸ 修复方案 2：field_simp [show x + y ≠ 0 from ...]

field_simp 能自动推导 a * b ≠ 0（从 a ≠ 0 和 b ≠ 0）， 但对 a + b ≠ 0 这类条件需要显式提供。

18.5.3. 失败 3：ring 收尾失败🔗

-- [会报错] field_simp 成功但 ring 无法关闭
example (x : ℝ) (hx : x ≠ 0) (h : x > 1) :
    1 / x < 1 := by
  field_simp
  -- ⊢ 1 < x （这不是多项式等式！）
  -- ring  -- ❌ ring 只处理等式
  linarith  -- ✓ 不等式用 linarith

field_simp 后不一定接 ring——要看剩余目标的类型选择合适的 tactic。

18.5.4. 失败 4：目标中没有分式🔗

-- [不会报错但无效果] 没有分母可消
example (a b : ℝ) : a + b = b + a := by
  field_simp     -- ▸ 什么都没做，目标不变
  ring           -- ▸ 实际由 ring 完成

field_simp 在没有分式的目标上是空操作（no-op），不会报错但浪费一行。 如果目标已经是多项式等式，直接用 ring。

18.5.5. 失败 5：除法语义冲突（ℕ / ℤ 上的整除）🔗

-- [会报错] 自然数除法是截断除法，不是域除法
-- example (n : ℕ) (hn : n ≠ 0) : n / n = 1 := by field_simp
  -- ▸ field_simp 需要域结构（Field），ℕ 不是域
  -- ▸ 修复：用 Nat.div_self（自然数除法引理）或转换到 ℚ/ℝ
example (n : ℕ) (hn : 0 < n) : n / n = 1 := Nat.div_self hn

field_simp 只在 Field（或 DivisionRing）上工作。 ℕ 和 ℤ 上的 / 是整数除法，不在其适用范围内。

18.6.1. 模式 1：field_simp + ring（最常见）🔗

18.6.2. 模式 2：不等式用 rw + 消分母引理🔗

• ❶ field_simp 对不等式支持有限，rw [div_lt_one h] 更直接。

• ❷ positivity 证明 x ^ 2 + 1 > 0，为 div_le_one 提供侧条件。

18.6.3. 模式 3：push_cast + field_simp + ring🔗

18.7.1. 技巧 1：用 field_simp? 查看使用的引理🔗

example (a b : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) :
    1/a + 1/b = (a + b) / (a * b) := by
  field_simp?    -- ▸ 建议：simp only [one_div, ne_eq, ...]; ring

18.7.2. 技巧 2：检查 Infoview 中的剩余目标🔗

field_simp 之后把光标放在下一行，查看剩余目标—— 这决定了该用 ring（多项式等式）、linarith（不等式）还是其他 tactic。

18.7.3. 技巧 3：显式传入非零条件🔗

• ❶ field_simp 无法自动推导 a + b ≠ 0，用 [hab] 显式提供。

18.9.1. 练习 1（基础）：field_simp + ring🔗

-- (a) 通分
example (a b : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) :
    a / b + b / a = (a ^ 2 + b ^ 2) / (a * b) := by
  sorry

-- (b) 嵌套分式
example (x : ℝ) (hx : x ≠ 0) :
    1 / (1 + 1 / x) = x / (x + 1) := by
  sorry
  -- 提示：可能需要 field_simp [show x + 1 ≠ 0 from ...]

提示：(a) 直接 field_simp; ring。 (b) 需要 x + 1 ≠ 0 的假设或证明。

18.9.2. 练习 2（判断）：field_simp 能否成功🔗

判断以下哪些 field_simp 能处理（假设非零条件已提供），不能的说明原因：

example (x : ℝ) (hx : x ≠ 0) : x / x = 1 := by sorry              -- (a)
example (n : ℕ) (hn : 0 < n) : n / n = 1 := by sorry               -- (b)
example (x : ℝ) (hx : x ≠ 0) : 1/x + 1/x = 2/x := by sorry       -- (c)
example (x : ℝ) (hx : 0 < x) : 1/x > 0 := by sorry                -- (d)

提示：(a) ✓ 域上的除法；(b) ✗ ℕ 不是域； (c) ✓ field_simp; ring；(d) 部分——field_simp 可消分母但剩余不等式需 linarith。

18.9.3. 练习 3（非零条件）：补充假设🔗

-- 添加最少的假设使证明成立
example (a b : ℝ) /- 补充假设 -/ :
    1 / a + 1 / b = (a + b) / (a * b) := by
  field_simp
  ring

提示：需要 (ha : a ≠ 0) (hb : b ≠ 0)。 注意 a * b ≠ 0 可以从这两个条件自动推导。

18.9.4. 练习 4（组合 tactic）：分式不等式🔗

example (x : ℝ) (hx : 2 ≤ x) : 1 / x ≤ 1 / 2 := by
  sorry

提示：用 div_le_div_of_nonneg_left 或 rw [div_le_div_iff] 消分母后用 linarith。 注意需要证明 0 < x 和 0 < 2。

18.9.5. 练习 5（实战）：复合分式等式🔗

example (x y : ℝ) (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x + y ≠ 0) :
    1 / x + 1 / y - 1 / (x + y) =
    (x ^ 2 + x * y + y ^ 2) / (x * y * (x + y)) := by
  sorry

提示：field_simp [hxy]; ring。hxy 必须显式传入， 因为 field_simp 无法从 hx 和 hy 推导 x + y ≠ 0。

18.9.6. 练习 6（进阶）：field_simp 在假设上🔗

example (x : ℝ) (hx : x ≠ 0) (h : 1 / x + x = 5 / 2) :
    2 * x ^ 2 - 5 * x + 2 = 0 := by
  sorry

提示：先 field_simp at h 对假设消分母， 然后 linarith 或 nlinarith 从化简后的 h 得到结论。