How to prove a conditional?

Stream: new members

[debord]

Hello. I am a noobie mathematician and an even bigger noobie with Lean. I've managed to do all the exercises in the 'Propositions and Proofs' chapter in 'Proving Theorems with Lean 4', apart from the ones that have conditionals in their conclusions. For example

example : (p → q ∨ r) → ((p → q) ∨ (p → r)) :=
  λ hpqr : p → q ∨ r => byCases
    (λ hp : p =>
      have hqr : q ∨ r := hpqr hp
      Or.elim hqr
        (λ hq : q =>
          /- I wish I could use "hp hq" here but I seem to be confused about how lambda works.-/)
        (λ hr : r =>
          /- "hp hr" here I feel like should mean assuming p we can prove q ∨ r, and if r is true then p → r is true. Then I could use Or.intro to prove the final statement.-/))
    (λ hnp : ¬p =>
      sorry)

is my current best attempt at one of them. Lambda's are explained as a kind of "conditional introduction" in the text, and as with the other introduction rules I would think you could then prove a conditional with it, but that seems not to be the case, or at least I'm thinking about it wrongly. Could I have at least some hint to what I should be doing to complete these?
I'm also having a very tough time figuring out how to prove the simple ¬(p → q) → p. ¬(p → q) is equivalent to (p → q) → False, and I certainly can see informally why ¬(p → q) → p is the case, ¬(p → q) being true means that p is true while q is false, so therefore p is true, but I am having a hard time figuring out how to articulate this notion of conditionals in lean. What am I missing?
Thanks for your time.

[Bulhwi Cha]

Can you prove the following examples?

open Classical
variable (p q : Prop)

example (hp : p) (hq : q) : p → q :=
  sorry

example (hnp : ¬p) : p → q :=
  sorry

example : ¬(p → q) → p :=
  λ hnpq : ¬(p → q) => byCases
    (λ hp : p => sorry)
    (λ hnp : ¬p =>
      have hpq : p → q := sorry
      sorry)

Solutions

open Classical
variable (p q : Prop)

example (hp : p) (hq : q) : p → q :=
  λ hp' : p => hq

example (hnp : ¬p) : p → q :=
  λ hp : p => absurd hp hnp

example : ¬(p → q) → p :=
  λ hnpq : ¬(p → q) => byCases
    (λ hp : p => hp)
    (λ hnp : ¬p =>
      have hpq : p → q := λ hp : p => absurd hp hnp
      absurd hpq hnpq)

[debord]

Okay I think I'm starting to see it now then. The way to do what I'm trying to do is to make a proof that the assumption is false and then use absurd to prove any arbitrary q including whatever my goal is. This logic was pretty shocking to me but I suppose it is a natural consequence of the principle of explosion. I need more practice to get used to it, thank you for the demonstration Bulhwi.