Prove (p → ¬ q) → ¬ (p ∧ q) in Lean4

I get as far as this

theorem problem_2 : (p → ¬ q) → ¬ (p ∧ q) := by
   intro hp 
   intro hpw 

which gets me to ⊢ False

Not p, or ¬p, is the negation of p. It is defined to be p → False, so if your goal is ¬p you can use intro h to turn the goal into h : p ⊢ False, and if you have hn : ¬p and h : p then hn h : False and (hn h).elim will prove anything. For more information: Propositional Logic.

de Moura, Leonardo, Mario Carneiro et al. “Init.Prelude.” Mathlib4 Docs. Accessed Feb 10, 2023. https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Not.

We can solve the problem as follows:

theorem problem_2 : (p → ¬q) → ¬(p ∧ q) := by
  intro hpnq hpq
  have hp : p := hpq.1
  have hnq : ¬q := hpnq hp
  have hq : q := hpq.2  
  exact hnq hq