Question about types

Stream: new members

[Travis Rivera Petit]

Hi,
I am a beginner in Lean and have an elementary question. I am doing the exercises for the Lean textbook of chapter three, and have trouble proving

((p ∨ q) → r) → (p → r) ∧ (q → r)

You can see my attempt below.

example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
iff.intro
  (assume hpq: p ∨ q,
  assume hr: r,
  -- help here
  have hpr: p → r, from ???
  --
  )
  (
    assume h: (p → r) ∧ (q → r),
    have hpr: p → r, from and.left h,
    have hqr: q → r, from and.right h,
    assume hpq: p ∨ q,
    or.elim hpq
    (assume hp: p, show r, from hpr hp)
    (assume hq: q, show r, from hqr hq)
  )

The problem is that unlike conjunctions or disjuntcions, implications do not have any introduction/elimination rules, so I do not know how to construct a type p → r from p and r. What should I do?

[Reid Barton]

You already know how to construct an implication: assume. However, you've gone wrong in another way in the first section

[Ruben Van de Velde]

You can use an underscore in the place where you're stuck, and try to make sense of the error message:

example {p q r : Prop}  : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
iff.intro
  (
    assume hpq: p ∨ q,
    _
  )
  (
    assume h: (p → r) ∧ (q → r),
    have hpr: p → r, from and.left h,
    have hqr: q → r, from and.right h,
    assume hpq: p ∨ q,
    or.elim hpq
    (assume hp: p, show r, from hpr hp)
    (assume hq: q, show r, from hqr hq)
  )

type mismatch at application
  iff.intro (λ (hpq : p ∨ q), ?m_1[hpq])
term
  λ (hpq : p ∨ q), ?m_1[hpq]
has type
  p ∨ q → (p → r) ∧ (q → r)
but is expected to have type
  (p ∨ q → r) → (p → r) ∧ (q → r)