Prove $(p → (q → r)) ↔ ((p ∧ q) → r)$ with lean4 [closed]

I try to solve the examples from chapter for from the online guide while learning lean4. But I can't solve this one. I'm as far as:

example : (p → (q → r)) ↔ (p ∧ q → r) := 
  Iff.intro
    (
      fun h : (p → q → r)=>
      (sorry)
    )
    (sorry)

I don't understand how I can get a proof for p in the "→" case, or maybe an assumption.

Here is a logic proof: \begin{align*} (p\to(q\to r)) & \Longleftrightarrow (\neg p\vee(q\to r))\\\\ & \Longleftrightarrow (\neg p\vee(\neg q\vee r))\\\\ & \Longleftrightarrow ((\neg p\vee \neg q) \vee r)\\\\ & \Longleftrightarrow (\neg(p\wedge q)\vee r)\\\\ & \Longleftrightarrow (p \wedge q)\to r \end{align*}