Representing a theorem with multiple hypotheses in Lean (propositional logic)

Real beginners question here. How do I represent a problem with multiple hypotheses in Lean? For example:

Given

A
A→B
A→C
B→D
C→D

Prove the proposition D.

(Problem taken from The Incredible Proof Machine, Session 2 problem 3. I was actually reading Logic and Proof, Chapter 4, Propositional Logic in Lean but there are less exercises available there)

Obviously this is completely trivial to prove by applying modus ponens twice, my question is how do I represent the problem in the first place?! Here's my proof:

variables A B C D : Prop

example : (( A    )
    /\     ( A->B )
    /\     ( A->C )
    /\     ( B->D )
    /\     ( C->D ))
-> D :=
assume h,
have given1: A, from and.left h,
have given2: A -> B, from and.left (and.right h),
have given3: A -> C, from and.left (and.right (and.right h)),
have given4: B -> D, from and.left (and.right (and.right (and.right h))),
have given5: C -> D, from and.right (and.right (and.right (and.right h))),
show D, from given4 (given2 given1)

Try it!

I think I've made far too much a meal of packaging up the problem then unpacking it, could someone show me a better way of representing this problem please?

Solution

I think it is a lot clearer by not using And in the hypotheses instead using ->. here are 2 equivalent proofs, I prefer the first

def s2p3 {A B C D : Prop} (ha : A)
      (hab : A -> B) (hac : A -> C)
      (hbd : B -> D) (hcd : C -> D) : D
  := show D, from (hbd (hab ha))

The second is the same as the first except using example, I believe you have to specify the names of the parameters using assume rather than inside the declaration

example : A -> (A -> B) -> (A -> C) -> (B -> D) -> (C -> D) -> D :=
assume ha : A,
assume hab : A -> B,
assume hac, -- You can actually just leave the types off the above 2
assume hbd, 
assume hcd,
show D, from (hbd (hab ha))

if you want to use the def syntax but the problem is e.g. specified using example syntax

example : A -> (A -> B) -> (A -> C)
            -> (B -> D) -> (C -> D) -> D := s2p3

Also, when using and in your proof, in the unpacking stage You unpack given3, and given 5 but never use them in your "show" proof. So you don't need to unpack them e.g.

example : (( A    )
    /\     ( A->B )
    /\     ( A->C )
    /\     ( B->D )
    /\     ( C->D ))
-> D :=
assume h,
have given1: A, from and.left h,
have given2: A -> B, from and.left (and.right h),
have given4: B -> D, from and.left (and.right (and.right (and.right h))),
show D, from given4 (given2 given1)