即使 {x y ε : ℝ} 是隐式的，intro 仍然会引入它们。
隐式只影响使用时是否需要写，不影响证明时是否需要引入。
apply 战术：应用定理
-- 给定定理theorem my_lemma : ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < εvariable (a b : ℝ) (δ : ℝ) (h₀ : 0 < δ) (h₁ : δ ≤ 1) (ha : |a| < δ) (hb : |b| < δ)-- 应用方式#check my_lemma a b δ -- 需要提供所有参数#check my_lemma a b δ h₀ h₁ -- 提供部分假设#check my_lemma a b δ h₀ h₁ ha hb -- 完全应用
在 tactic 中使用 apply：
example : |a * b| < δ := by apply my_lemma a b δ h₀ h₁ ha hb -- 直接关闭目标-- 或者分步example : |a * b| < δ := by apply my_lemma -- 目标变成四个子目标 · exact h₀ -- 证明 0 < δ · exact h₁ -- 证明 δ ≤ 1 · exact ha -- 证明 |a| < δ · exact hb -- 证明 |b| < δ
示例中使用的自定义定义
下文示例使用两个辅助定义（来自原教程）：
def FnUb (f : ℝ → ℝ) (a : ℝ) := ∀ x, f x ≤ a -- f 以 a 为上界def FnHasUb (f : ℝ → ℝ) := ∃ a, FnUb f a -- f 有上界def FnLb (f : ℝ → ℝ) (a : ℝ) := ∀ x, a ≤ f x -- f 以 a 为下界
dsimp：展开定义
example (hfa : FnUb f a) (hgb : FnUb g b) : FnUb (fun x ↦ f x + g x) (a + b) := by intro x dsimp -- 展开 lambda：(fun x ↦ f x + g x) x → f x + g x apply add_le_add apply hfa apply hgb
dsimp vs change
dsimp 自动展开定义和 beta 规约
change 手动指定目标应该变成什么：
change f x + g x ≤ a + b
Monotone：隐藏的全称量词
def Monotone (f : ℝ → ℝ) := ∀ {a b}, a ≤ b → f a ≤ f b-- ↑ 隐式的全称量词
使用 Monotone f 时：
example (mf : Monotone f) : ∀ {a b}, a ≤ b → f a ≤ f b := @h-- @h 显式展开隐式参数
证明项 vs Tactic 对照
variable (f g : ℝ → ℝ)-- Tactic 版本example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x := by intro a b aleb -- 任取 a ≤ b apply add_le_add -- f a + g a ≤ f b + g b 可由 f a ≤ f b 和 g a ≤ g b 推出 · apply mf aleb -- mf : Monotone f，aleb : a ≤ b，得 f a ≤ f b · apply mg aleb -- mg : Monotone g，aleb : a ≤ b，得 g a ≤ g b-- 证明项版本example (mf : Monotone f) (mg : Monotone g) : Monotone fun x ↦ f x + g x := fun a b aleb ↦ add_le_add (mf aleb) (mg aleb)-- ↑ intro 对应 fun，apply 对应函数应用
证明项技巧
写 fun a b aleb ↦ _ 然后看 Lean 的错误提示，它会告诉你 _ 需要什么类型。
集合与子集
-- 子集的定义：s ⊆ t 表示 ∀ {x : α}, x ∈ s → x ∈ t-- ↑ 隐式的全称量词
variable {α : Type*} (s t : Set α)example : s ⊆ s := by intro x xs -- 任取 x ∈ s exact xs -- 目标是 x ∈ s，假设 xs 正好就是
Injective：单射
def Injective (f : α → β) := ∀ {x₁ x₂}, f x₁ = f x₂ → x₁ = x₂
证明单射：
-- add_left_inj c : ∀ x y, x + c = y + c ↔ x = y（加 c 是单射的等价刻画）example (c : ℝ) : Injective fun x ↦ x + c := by intro x₁ x₂ h' -- 引入 x₁, x₂ 和假设 h' : x₁ + c = x₂ + c exact (add_left_inj c).mp h' -- 用 iff 的正向：x₁ + c = x₂ + c → x₁ = x₂
3.2 The Existential Quantifier
核心洞见
证明 ∃：用 use 提供见证
使用 ∃：用 rcases 解包
证明存在：use 战术
example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 -- 提供见证 norm_num -- 验证性质
匿名构造器
-- 证明项版本example : ∃ x : ℝ, 2 < x ∧ x < 3 := ⟨5 / 2, by norm_num⟩-- ↑ 用尖括号构造
使用存在假设：rcases
variable (f g : ℝ → ℝ)-- fnUb_add：若 f 以 a 为上界，g 以 b 为上界，则 f+g 以 a+b 为上界example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x ↦ f x + g x := by rcases ubf with ⟨a, ubfa⟩ -- 解包：a 是上界，ubfa : ∀ x, f x ≤ a rcases ubg with ⟨b, ubgb⟩ -- 解包：b 是上界，ubgb : ∀ x, g x ≤ b use a + b -- 提供 witness：f x + g x ≤ a + b intro x -- 任取 x dsimp -- 展开 (fun x ↦ f x + g x) x = f x + g x apply add_le_add -- f x ≤ a 且 g x ≤ b ⇒ f x + g x ≤ a + b · exact ubfa x · exact ubgb x
variable (a b c : ℕ)-- a ∣ b 实际上是 ∃ d, b = a * dexample (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by rcases divab with ⟨d, rfl⟩ -- 用 rfl 技巧：d 是商，且 b = a * d rcases divbc with ⟨e, rfl⟩ -- e 是商，且 c = b * e = a * d * e use d * e; ring -- c = a * (d * e)，所以 a ∣ c
Surjective：满射
def Surjective (f : α → β) := ∀ y, ∃ x, f x = y-- ↑ 全称 + 存在
证明满射同时用 intro 和 use：
example {c : ℝ} : Surjective fun x ↦ x + c := by intro x -- 引入任意 y use x - c -- 提供见证 dsimp; ring -- 验证
使用满射假设
example {f : ℝ → ℝ} (h : Surjective f) : ∃ x, f x ^ 2 = 4 := by rcases h 2 with ⟨x, hx⟩ -- 对 y=2 使用满射 use x rw [hx]; norm_num
field_simp：清除分母
example (x y : ℝ) (h : x - y ≠ 0) : (x ^ 2 - y ^ 2) / (x - y) = x + y := by field_simp [h] -- 清除分母 ring -- 证明剩余等式
3.3 Negation
核心洞见
¬ A 定义为 A → False。
证明 ¬A：引入 h : A，导出矛盾
使用 ¬A：对 h : ¬A 和 h’ : A 应用得到 False
证明否定
example (h : a < b) : ¬b < a := by intro h' -- 假设 b < a have : a < a := lt_trans h h' -- 导出 a < a apply lt_irrefl a this -- 矛盾
模式：intro h' → 导出矛盾 → 关闭目标
have 的简写
have : a < a := lt_trans h h'-- ↑ 不写名字时，自动用 "this"
linarith：线性算术
variable (f : ℝ → ℝ)example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by intro fnub -- 假设 f 有上界 rcases fnub with ⟨a, fnuba⟩ -- a 是上界，fnuba : ∀ x, f x ≤ a rcases h a with ⟨x, hx⟩ have : f x ≤ a := fnuba x linarith -- 自动从线性不等式导出矛盾
否定的等价变换
#check (not_le_of_gt : a > b → ¬a ≤ b)#check (not_lt_of_ge : a ≥ b → ¬a < b)#check (lt_of_not_ge : ¬a ≥ b → a < b)#check (le_of_not_gt : ¬a > b → a ≤ b)
push_neg：推进否定
-- 原始：¬∀ a, ∃ x, f x > a-- push_neg 后：∃ a, ∀ x, f x ≤ aexample (h : ¬∀ a, ∃ x, f x > a) : FnHasUb f := by push_neg at h exact h
push_neg 的直觉
把 ¬ 推进到最内层，同时翻转量词和比较：
¬∀ → ∃¬
¬∃ → ∀¬
¬(≤) → >
¬(<) → ≥
contrapose：逆否命题
-- 目标 A → B 变成 ¬B → ¬Aexample (h : ¬FnHasUb f) : ∀ a, ∃ x, f x > a := by contrapose! h -- ! 表示同时应用 push_neg exact h
经典逻辑：by_contra
variable {α : Type*} (P : α → Prop)-- 反证法example (h : ¬∀ x, P x) : ∃ x, ¬P x := by by_contra h' -- 假设 ¬(∃ x, ¬P x)，即 ∀ x, P x apply h -- 目标是 ¬∀ x, P x，即证 ∀ x, P x → False intro x -- 任取 x show P x -- 目标是 P x by_contra h'' -- 假设 ¬P x exact h' ⟨x, h''⟩ -- h' 说 ¬∃ x, ¬P x，但 ⟨x, h''⟩ 证明了 ∃ x, ¬P x，矛盾
variable (a : ℝ)-- lt_irrefl : ∀ a, ¬(a < a)，即 a < a 是假的example (h : 0 < 0) : a > 37 := by exfalso -- 从矛盾假设推出任何结论 apply lt_irrefl 0 h -- 0 < 0 与自反性矛盾
3.4 Conjunction and Iff
核心洞见
证明 A ∧ B：用 constructor 分成两个目标
使用 A ∧ B：用 rcases 或 .left/.right
证明合取
variable (x y : ℝ) (h₀ : x ≤ y) (h₁ : x ≠ y)example : x ≤ y ∧ x ≠ y := by constructor · exact h₀ -- 证明左边：x ≤ y · exact h₁ -- 证明右边：x ≠ y
或用匿名构造器：
example : x ≤ y ∧ x ≠ y := ⟨h₀, fun h ↦ ...⟩
使用合取
-- 方式1：rcasesrcases h with ⟨h₀, h₁⟩-- 方式2：点语法h.left -- 第一个分量h.right -- 第二个分量h.1 -- 等价h.2 -- 等价
双蕴含 ↔
-- 证明 ↔：用 constructor（和 ∧ 一样）-- 示例：x ≤ y ∧ y ≤ x ↔ x = y（≤ 的反对称性）example : x ≤ y ∧ y ≤ x ↔ x = y := by constructor · -- 正向 rintro ⟨h₁, h₂⟩ -- h₁ : x ≤ y, h₂ : y ≤ x exact le_antisymm h₁ h₂ -- le_antisymm : x ≤ y → y ≤ x → x = y · -- 反向 intro h₁ rw [h₁] exact ⟨le_refl y, le_refl y⟩
使用 ↔：
h.mp -- 正向 A → Bh.mpr -- 反向 B → Ah.1 -- 同 mph.2 -- 同 mpr