## Stream: new members

### Topic: what is wrong with my code, Distributive Law

#### Shaun Modipane (Jan 31 2022 at 09:13):

What is wrong with my proof here, Lean says the problem is in line 8.

example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.elim
-- prove that p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r)
(
assume hpqr : p ∧ (q ∨ r),
have hp : p, from and.elim_left hpqr,
have hqr : (q ∨ r), from and.elim_right hpqr,
or.elim hqr -- here is the problem
-- prove that q → (p ∧ q) ∨ (p ∧ r)
(
assume hq : q,
show (p ∧ q) ∨ (p ∧ r), from or.intro_left (p ∧ r) (and.intro hp hq)
)
-- prove that r → (p ∧ q) ∨ (p ∧ r)
(
assume hr : r,
show (p ∧ q) ∨ (p ∧ r), from or.intro_right (p ∧ q) (and.intro hp hr)
)
)
-- prove that (p ∧ q) ∨ (p ∧ r) → p ∧ (q ∨ r)
(
assume hpqpr : (p ∧ q) ∨ (p ∧ r),
or.elim hpqpr
-- prove that (p ∧ q) → p ∧ (q ∨ r)
(
assume hpq : p ∧ q,
have hp : p, from and.elim_left hpq,
have hq : q, from and.elim_right hpq,
show p ∧ (q ∨ r), from and.intro hp (or.intro_left r hq)
)
-- prove that (p ∧ r) → p ∧ (q ∨ r)
(
assume hpr : p ∧ r,
have hp : p, from and.elim_left hpr,
have hr : r, from and.elim_right hpr,
show p ∧ (q ∨ r), from and.intro hp (or.intro_right q hr)
)
)

apologise for the pour formating

#### Ruben Van de Velde (Jan 31 2022 at 09:20):

Can you try editing your post with #backticks?

#### Chris B (Jan 31 2022 at 09:39):

iff.elim should be iff.intro, since you're trying to produce a proof of an iff, not use one you already have (which is what elim is for).

#### Chris B (Jan 31 2022 at 09:43):

There's enough going on that it just wasn't able to produce a great error message.

#### Kevin Buzzard (Jan 31 2022 at 09:44):

If you really insist on writing these monstrous term proofs instead of proving the example in tactic mode (where you can manage all the goals far more easily), you should build them very carefully using _ to fill in any holes, and stop the moment there is an error.

Last updated: Dec 20 2023 at 11:08 UTC