# Zulip Chat Archive

## Stream: new members

### Topic: distributing `or`

#### Iocta (Dec 29 2019 at 01:36):

This clearly isn't on the right track,

def factor_or : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) := (λ h, or.elim (and.left h) -- p is true. or.inl -- If p is false, q and r are true. -- But we don't really know that p is false. (λ z, (or.inr (and.intro z _))) )

but lean doesn't like `or.elim (p \or \not p)`

either.

def factor_or : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) := (λ h, or.elim (p ∨ ¬p) -- p is true. or.inl -- p is false, so q and r are true. (λ z, (or.inr (and.intro z _))) )

How can I go about this?

#### Kenny Lau (Dec 29 2019 at 02:02):

the `p or not p`

needs to be replaced with a **proof** of `p or not p`

#### Kenny Lau (Dec 29 2019 at 02:02):

which is `classical.em p`

#### Kenny Lau (Dec 29 2019 at 02:02):

or maybe `classical.em`

, I don't remember

#### Iocta (Dec 29 2019 at 05:24):

This is in the section of the exercises that I think isn't supposed to require `classical`

. Is there a way to do it without?

#### Joe (Dec 29 2019 at 05:42):

lemma factor_or : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) := λh, or.elim h.left or.inl $ λhq, or.elim h.right or.inl $ λhr, or.inr $ and.intro hq hr

#### Yury G. Kudryashov (Dec 29 2019 at 05:43):

Try to do `or.elim`

on both `and.left h`

and `and.right h`

.

#### Iocta (Dec 29 2019 at 06:12):

Got it, thanks.

def factor_or : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) := (λ h, (or.elim h.left or.inl (λ qq, or.elim h.right or.inl (λ rr, (or.inr (and.intro qq rr))))))

#### Yury G. Kudryashov (Dec 29 2019 at 06:14):

BTW, it makes sense to use `theorem`

/`lemma`

in this case because the conclusion is a proposition, not a `Type`

.

#### Iocta (Dec 29 2019 at 06:37):

Ok

#### Luis O'Shea (Jan 04 2020 at 15:28):

Below is the same proof written in a slightly different way. It illustrates

- Using dot syntax to deal with
`and`

followed by`or`

:`h.left.elim`

and`h.right.elim`

- Letting Lean infer the
`and`

constructor by using angle brackets:`⟨hq,hr⟩`

I'm not saying it's stylistically better (it's just an example of some Lean syntax which may be of interest).

example (h: (p ∨ q) ∧ (p ∨ r)) : p ∨ (q ∧ r) := h.left.elim or.inl (assume hq, h.right.elim or.inl (assume hr, or.inr ⟨hq,hr⟩))

Last updated: May 11 2021 at 14:11 UTC