Lean4中证明(p → ¬q) → ¬(p ∧ q)：已完成部分步骤求指导

当前代码执行到intro hpw后，目标为⊢ False，可以按以下步骤完成证明：

• 拆分合取假设hpw：
  使用cases命令分离出p和q两个子假设，代码如下：

  cases hpw with
  | intro p q =>
  

  执行后会新增假设p : Prop和q : Prop。

• 推导¬q：
  利用已有的hp : p → ¬q和刚得到的p，通过have命令得到¬q：

  have hnq := hp p
  

  此时hnq的类型是¬q，等价于q → False。

• 导出矛盾完成证明：
  用hnq和q直接推导出False，满足目标要求：

  exact hnq q
  

完整的证明代码：

theorem problem_2 : (p → ¬ q) → ¬ (p ∧ q) := by
   intro hp 
   intro hpw 
   cases hpw with
   | intro p q =>
     have hnq := hp p
     exact hnq q

你也可以用更简洁的写法，直接通过模式匹配拆分合取假设，省略cases步骤：

theorem problem_2 : (p → ¬ q) → ¬ (p ∧ q) := by
   intro hp ⟨p, q⟩
   exact hp p q

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