编辑“︁Lean战术系统”︁（章节）

== 基础战术 ==
以下是初学者必须掌握的6个核心战术：

=== `intro` ===
用于消除目标中的全称量词或蕴含前提：
<syntaxhighlight lang="lean">
example : ∀ (P Q : Prop), P → Q → P :=
begin
  intro P Q hP hQ,  -- 将命题变量和假设引入上下文
  exact hP          -- 直接使用假设P
end
</syntaxhighlight>

=== `apply` ===
反向应用已知定理：
<syntaxhighlight lang="lean">
lemma modus_ponens (P Q : Prop) (h1 : P → Q) (h2 : P) : Q :=
begin
  apply h1,  -- 目标Q变为证明P
  exact h2
end
</syntaxhighlight>

=== `rw`（重写） ===
基于等式或等价关系进行替换：
<syntaxhighlight lang="lean">
example (a b : ℕ) (h : a = b) : b = a :=
begin
  rw h,  -- 将b替换为a
  -- 目标变为a = a，自动通过refl解决
end
</syntaxhighlight>