Lean 3含assume的证明如何转换为Lean 4证明？

很多Lean 3的证明会用assume语法引入变量或前提，比如下面这个示例：

theorem WetTheorem : 
forall Rain Hydrant Wet: Prop, 
    (Rain ∨ Hydrant) → -- raining or hydrant on;
    (Rain → Wet) →     -- if raining then wet;
    (Hydrant → Wet) →  -- if hydrant on then wet;
    Wet                -- then wet
:=
begin
-- setup
  assume Rain Hydrant Wet,
  assume RainingOrHydrantRunning: (Rain ∨ Hydrant),
  assume RainMakesWet: (Rain → Wet),
  assume HydrantMakesWet: (Hydrant → Wet),
-- the core of the proof
  cases RainingOrHydrantRunning with raining running,
    show Wet, from RainMakesWet raining,
    show Wet, from HydrantMakesWet running,
end

Lean 4移除了assume语法，下面是通用的转换方法：

转换步骤 #

• 替换assume为intro：Lean 4用intro实现assume的全部功能，不管是引入全称量词变量还是蕴含式前提：
  • 单个变量：assume x → intro x
  • 多个变量：assume x y z → intro x y z
  • 带类型标注：assume h : P → Q → intro h : P → Q
• 核心战术逻辑基本保留：cases、apply这类核心战术的用法在Lean 4里和Lean 3几乎一致，无需修改。
• show可按需简化：Lean 4仍支持show明确目标，但多数场景下Lean能自动推断目标，可直接用exact给出结果省略show。

转换后的Lean 4示例 #

theorem WetTheorem : 
forall Rain Hydrant Wet: Prop, 
    (Rain ∨ Hydrant) → -- raining or hydrant on;
    (Rain → Wet) →     -- if raining then wet;
    (Hydrant → Wet) →  -- if hydrant on then wet;
    Wet                -- then wet
:=
begin
-- setup
  intro Rain Hydrant Wet,
  intro RainingOrHydrantRunning: (Rain ∨ Hydrant),
  intro RainMakesWet: (Rain → Wet),
  intro HydrantMakesWet: (Hydrant → Wet),
-- the core of the proof
  cases RainingOrHydrantRunning with raining running,
    exact RainMakesWet raining,
    exact HydrantMakesWet running,
end

如果喜欢更紧凑的写法，还可以把多个intro合并成一行：

begin
  intro Rain Hydrant Wet RainingOrHydrantRunning RainMakesWet HydrantMakesWet,
  cases RainingOrHydrantRunning with raining running,
  exact RainMakesWet raining,
  exact HydrantMakesWet running,
end

内容的提问来源于stack exchange，提问作者n-0