## Stream: new members

### Topic: TPIL Chap 3 exercise help

#### Luca Seemungal (Aug 30 2019 at 16:06):

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 (Aug 30 2019 at 16:28):

Get rid of the comma after h.right

Last updated: May 11 2021 at 00:31 UTC