Lean4代码报‘unknown identifier 'begin'’等错误的原因咨询

• 核心原因：Lean4已移除Lean3里的begin/end战术块语法，改用by关键字触发战术证明模式，所以输入begin会被判定为未定义标识符，单独的end也因无对应作用域报错，属于语法使用错误，并非配置问题。

• 修复后的示例代码：

example (p q r : Prop) : ((p ∨ q) → r) ↔ ((p → r) ∧ (q → r)) :=
by
  apply Iff.intro
  · intro h
    apply And.intro
    · intro hp; exact h (Or.inl hp)
    · intro hq; exact h (Or.inr hq)
  · intro h hpq
    cases hpq with
    | inl hp => exact h.left hp
    | inr hq => exact h.right hq

• 补充说明：若习惯Lean3写法，可在文件开头添加open Lean Lean.Meta Lean.Elab.Tactic in启用兼容模式，但官方更推荐直接使用by的新语法。

内容的提问来源于stack exchange，提问作者then999