Lean : Proof that \ not p \to (p \ to q) or similar false \to p

Question

I am new at lean - prover and I am trying to solve the examples on the online tutorial.

I am stuck at this example and I need to prove that "false implies q" or something like that. My code is :

variables p q : Prop
example : ¬ p → (p → q) := 
    assume h : ¬ p,
    assume hp : p,
    --have hnpq : ¬ p ∨ q, from or.inl h,
    have hf : false, from h hp,
    --show q, from hf
    sorry

I do not think that defining hnpq can help because this proof is part of the (¬ p ∨ q) → (p → q). In set theory I think that false implies everything.

Any suggestions or thoughts?