what is wrong with my code, Distributive Law

Stream: new members

[Shaun Modipane]

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]

Can you try editing your post with #backticks?

[Chris B]

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]

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

[Kevin Buzzard]

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.