TPIL Chap 3 exercise help

Stream: new members

[Luca Seemungal]

Hi, the following

example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro
(assume h : p ∧ (q ∨ r),
    or.elim h.right,
    (assume hq : q,
      or.inl (and.intro h.left hq))
    (assume hr : r,
      or.inr (and.intro h.left hr)))
(assume h : (p ∧ q) ∨ (p ∧ r), sorry)

gives me errors at h.left, with unknown identifier h.left

But I get h.left from the assume h : p ∧ (q ∨ r) line! What is the issue here? This is all module the sorry, obviously. Thanks!

[Koundinya Vajjha]

Get rid of the comma after h.right