17.2.1. 基本流程🔗

gcongr 的工作分为三步：

目标: a₁ * c ≤ b₁ * c          （假设 h : a₁ ≤ b₁, hc : 0 ≤ c）

第一步 —— 对齐: (·) * c ≤ (·) * c
  不同位置: 左侧 a₁  vs  右侧 b₁            -- ❶
  相同位置: c = c

第二步 —— 搜索引理:
  在 @[gcongr] 引理中找到:                    -- ❷
  mul_le_mul_of_nonneg_right : a ≤ b → 0 ≤ c → a * c ≤ b * c

第三步 —— 生成子目标:
  · a₁ ≤ b₁   （由 h 关闭）                  -- ❸
  · 0 ≤ c      （由 hc 关闭）

• ❶ 对齐两侧结构，定位差异的子表达式。

• ❷ 在 @[gcongr] 标记的引理库中搜索匹配的单调性定理。

• ❸ 将原目标拆成更简单的子目标，尝试自动关闭或留给用户。

17.2.2. 多位置分解🔗

当两侧有多个不同位置时，gcongr 逐一分解：

分解树：

目标: a * c ≤ b * d

对齐: (·) * (·) ≤ (·) * (·)
├── 位置 1: a vs b → 子目标 a ≤ b             -- ❶
├── 位置 2: c vs d → 子目标 c ≤ d             -- ❷
├── 侧条件: 0 ≤ a （由 ha 自动关闭）          -- ❸
└── 侧条件: 0 ≤ c （由 hc 自动关闭）          -- ❹

• ❶❷ 主要不等式子目标。❸❹ 单调性引理所需的侧条件。

注意：gcongr 不只是"照着原假设机械拆分"——它搜索的单调性引理 可能引入你意想不到的额外 side goals。例如，目标 a * c ≤ b * d 拆分时，引理可能要求 0 ≤ a 或 0 ≤ c，即使你的假设中并没有 直接提供这些条件。遇到 gcongr 留下未关闭的子目标时， 用 gcongr? 查看它实际调用了哪条引理，以理解额外条件的来源。

17.3.1. 算术运算🔗

17.3.2. 其他运算🔗

gcongr 还覆盖集合（⊆）、求和（Finset.sum）、积分等：

17.3.3. 注册自定义引理🔗

-- [示意] 为自定义函数注册单调性
@[gcongr]
theorem myFunc_le_myFunc (h : a ≤ b) (ha : 0 ≤ a) : myFunc a ≤ myFunc b := ...

@[gcongr] 的要求：结论必须是 _ ≤ _、_ < _ 或 _ ⊆ _ 形式， 且参数中变化的部分对应相同的关系。

17.5.1. 混合关系链🔗

gcongr 同时支持 ≤ 和 <，自动搜索严格/非严格版本的单调性引理。

17.7.1. 失败 1：两侧结构不匹配🔗

-- [会报错] 两侧的函数头不同
example (a b : ℝ) (h : a ≤ b) : a ^ 2 ≤ b ^ 3 := by gcongr
  -- ▸ gcongr failed: 左侧 (·)^2 vs 右侧 (·)^3，结构不一致
  -- ▸ 修复：用 calc 拆成两步，或直接用 nlinarith

gcongr 要求两侧有相同的外层结构——只有"洞"里的值不同。 a ^ 2 和 b ^ 3 的指数不同，无法对齐。

17.7.2. 失败 2：缺少侧条件🔗

-- [会报错] 乘法单调性需要非负条件
example (a b c : ℝ) (h : a ≤ b) : a * c ≤ b * c := by gcongr
  -- ▸ gcongr failed: 缺少 0 ≤ c
  -- ▸ 修复：添加假设 (hc : 0 ≤ c) 或在上下文中提供

这是最常见的失败——单调性引理有侧条件（如底数非负、乘数非负）， 但上下文中找不到对应的假设。

-- [会报错] 幂需要底数非负
example (a b : ℝ) (h : a ≤ b) : a ^ 3 ≤ b ^ 3 := by gcongr
  -- ▸ 修复：添加 (ha : 0 ≤ a)

17.7.3. 失败 3：找不到注册的引理🔗

-- [会报错] 目标关系没有对应的 @[gcongr] 引理
example (a b : ℝ) (h : a ≤ b) : Real.log a ≤ Real.log b := by gcongr
  -- ▸ 修复：log 的单调性需要 0 < a 的条件且可能没有注册 @[gcongr]
  -- ▸ 改用 Real.log_le_log 手动引用

不是所有函数都注册了 @[gcongr] 引理。可在 Mathlib 中搜索确认。

17.7.4. 失败 4：目标不是不等式🔗

-- [会报错] gcongr 只处理 ≤、<、⊆ 等序关系
example (a b : ℝ) (h : a = b) : a + 1 = b + 1 := by gcongr
  -- ▸ 修复：等式用 congr 或 rw，不用 gcongr

gcongr 是不等式的合同性工具。等式有专门的 congr tactic。

17.7.5. 失败 5：表达式方向反了🔗

-- [会报错] 假设方向和目标不一致
example (a b c : ℝ) (h : b ≤ a) (hc : 0 ≤ c) : a * c ≤ b * c := by gcongr
  -- ▸ gcongr 需要 a ≤ b，但假设是 b ≤ a
  -- ▸ 修复：目标方向可能有误，或用 gcongr; exact h.le / linarith

gcongr 不会翻转假设方向。如果目标需要 a ≤ b 但只有 b ≤ a， 需要手动检查目标是否正确。

17.8.1. 技巧 1：用 gcongr? 查看分解🔗

gcongr? 输出具体的引理调用，可用于理解分解过程或替换为显式证明。

17.8.2. 技巧 2：用 calc 拆步定位失败🔗

-- [示意] 一次性 gcongr 失败时，拆成两步定位问题
example (a b c d : ℝ) (h1 : a ≤ b) (h2 : c ≤ d)
    (ha : 0 ≤ a) (hc : 0 ≤ c) :
    a ^ 2 * c ≤ b ^ 2 * d := by
  calc a ^ 2 * c
      ≤ b ^ 2 * c := by gcongr    -- ✓ 先处理底数
    _ ≤ b ^ 2 * d := by gcongr    -- ✓ 再处理乘数

17.10.1. 练习 1（基础）：判断 gcongr 能否成功🔗

判断以下哪些能被 gcongr 证明，不能的说明原因：

example (a b : ℝ) (h : a ≤ b) : a + 3 ≤ b + 3 := by sorry          -- (a)
example (a b : ℝ) (h : a ≤ b) : a * b ≤ b * b := by sorry          -- (b)
example (a b : ℝ) (h : a ≤ b) : a ^ 2 ≤ b ^ 3 := by sorry          -- (c)
example (a b c : ℝ) (h : a ≤ b) : a * c ≤ b * c := by sorry        -- (d)
example (a b : ℝ) (h : a ≤ b) (ha : 0 ≤ a) : a ^ 4 ≤ b ^ 4 := by sorry -- (e)

提示：(a) ✓ 加法无条件单调；(b) 需要 0 ≤ b 作为侧条件； (c) ✗ 指数不同，结构不匹配；(d) 需要 0 ≤ c 侧条件； (e) ✓ 有底数非负假设。

17.10.2. 练习 2（calc 链）：分步不等式🔗

example (a b c : ℝ) (h1 : a ≤ b) (h2 : b ≤ c)
    (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) :
    a ^ 2 + a ≤ c ^ 2 + c := by
  sorry

提示：用 gcongr 直接尝试，或用 calc 拆成 a^2+a ≤ b^2+b ≤ c^2+c， 每步用 gcongr + linarith。

17.10.3. 练习 3（侧条件修复）：补充假设🔗

-- 添加最少的假设使 gcongr 成功
example (a b c d : ℝ) (h1 : a ≤ b) (h2 : c ≤ d)
    /- 补充假设 -/ : a * c ≤ b * d := by
  gcongr

提示：需要 (ha : 0 ≤ a) (hc : 0 ≤ c)——乘法两侧都需非负。 注意是较小的那侧（a 和 c）需要非负，不是较大侧。

17.10.4. 练习 4（positivity 配合）：复合不等式🔗

example (x y : ℝ) (hx : 0 < x) (hxy : x ≤ y) :
    x ^ 2 * Real.exp x ≤ y ^ 2 * Real.exp y := by
  sorry

提示：gcongr 可以分解，侧条件由 positivity 或 linarith 关闭。 注意 exp 的单调性可能需要 Real.exp_le_exp.mpr。

17.10.5. 练习 5（实战）：从 calc 链构建证明🔗

example (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a ≤ b) :
    a ^ 3 + a ^ 2 ≤ b ^ 3 + b ^ 2 := by
  sorry

提示：gcongr 直接在 + 上分解：a^3 ≤ b^3 和 a^2 ≤ b^2， 每个子目标再由 gcongr 或 gcongr; assumption 处理。

17.10.6. 练习 6（进阶）：模式模板🔗

example (a b c : ℝ) (h : a ≤ b) (ha : 0 ≤ a) (hc : 0 ≤ c) :
    (a + c) ^ 2 ≤ (b + c) ^ 2 := by
  sorry

提示：使用 gcongr (?_ + c) ^ 2 指定只有 ?_ 位置变化， 然后关闭子目标 a ≤ b 和侧条件 0 ≤ a + c（用 linarith 或 positivity）。