begin/end 块的写法属于 lean 3 的语法。在 Lean 4 中，要进入策略模式，应使用关键字 by，例如:
example (a b c : Prop) : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) := by sorry
现在没有对应的 end，因为作用域由空白决定，不过可以选择以 done 结束，如果还有未解决的目标，它就会报错。
即使你很熟悉 lean 3，我也建议浏览手册（https://lean-lang.org/lean4/doc/ ）以及 Theorem Proving in Lean/Functional Programming in Lean 中的一本或两本（手册第 4 和第 5 章），因为变化和改进相当多。
关键字 end 仍然用于结束节和命名空间，这解释了你在这里使用 end 时看到的诊断信息。
从英语翻译·查看原文The begin/end block notation belongs to lean 3. To start tactic mode with Lean 4, use the keyword by, for example:
example (a b c : Prop) : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) := by sorry
There is no corresponding end now because white space determines the scope, although an optional final done produces an error when a goal remains open.
Even with substantial lean 3 experience, I'd suggest looking through the manual (https://lean-lang.org/lean4/doc/) and/or Theorem Proving in Lean/Functional Programming in Lean (chapters 4 and 5 of the manual), given the considerable improvements and changes.
The end keyword still closes sections and namespaces, explaining the diagnostic you see when using end here.
