How to prove distributivity (propositional validity property 6) in LEAN?

Question

Having gone through most exercises and also solved/proved in LEAN the first five propositional validities/properties at the end of chapter 3 in the LEAN manual, I still have trouble with the following implication (one of the implications needed for the proof of property 6):

theorem Distr_or_L (p q r : Prop) : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
begin
    intros pqpr, 
    have porq : p ∨ q, from pqpr.left,
    have porr : p ∨ r, from pqpr.right,
    sorry
end

The difficulty I face is mainly due to the case when p is not true, as I don't know how to combine, using LEAN tools, the two sides of the and in the hypothesis to obtain the fact that both q and r must hold under that scenario. I would greatly appreciate any help here; please help me understand how to construct this proof in the above setting without importing any other tactics except those in standard LEAN. For completeness, here is my proof of the other direction:

theorem Distr_or_R (p q r : Prop) : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) :=
begin
    intros pqr,
    exact or.elim pqr 
    ( assume hp: p, show (p ∨ q) ∧ (p ∨ r), from 
        and.intro (or.intro_left q hp) (or.intro_left r hp) ) 
    ( assume hqr : (q ∧ r), show (p ∨ q) ∧ (p ∨ r), from 
        and.intro (or.intro_right p hqr.left) (or.intro_right p hqr.right) ) 
end

Answer 1

Hint. Try case splitting on both porq and porr.

Here's a solution

theorem Distr_or_L (p q r : Prop) : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
begin
    intros pqpr, 
    have porq : p ∨ q, from pqpr.left,
    have porr : p ∨ r, from pqpr.right,
    { cases porq with hp hq,
      { exact or.inl hp },
      { cases porr with hp hr,
        { exact or.inl hp },
        { exact or.inr ⟨hq, hr⟩ } } }
end