natural-number-game

Solututions to the Natural Number Game
proposition.lean (1293B)

 1 example (P Q : Prop) (p : P) (h : P → Q) : Q :=
 2 begin
 3   apply h,
 4   exact p,
 5 end
 6 
 7 lemma imp_self (P : Prop) : P → P :=
 8 begin
 9   intro p,
10   exact p,
11 end
12 
13 lemma maze (P Q R S T U: Prop)
14            (p : P)
15            (h : P → Q)
16            (i : Q → R)
17            (j : Q → T)
18            (k : S → T)
19            (l : T → U) : U :=
20 begin
21   apply l,
22   apply j,
23   apply h,
24   exact p,
25 end
26 
27 example (P Q : Prop) : P → (Q → P) :=
28 begin
29   intros p q,
30   exact p,
31 end
32 
33 example (P Q R : Prop) : (P → (Q → R)) → ((P → Q) → (P → R)) :=
34 begin
35   intros h1 h2 p,
36   apply h1,
37   exact p,
38   apply h2,
39   exact p,
40 end
41 
42 lemma imp_trans (P Q R : Prop) : (P → Q) → ((Q → R) → (P → R)) :=
43 begin
44   intros hpq hqr p,
45   apply hqr,
46   apply hpq,
47   exact p,
48 end
49 
50 lemma contrapositive (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) :=
51 begin
52   repeat {rw not_iff_imp_false},
53   intros hpq not_q p,
54   apply not_q,
55   apply hpq,
56   exact p,
57 end
58 
59 example (A B C D E F G H I J K L : Prop)
60         ( f1 : A → B) ( f2 : B → E) ( f3 : E → D) 
61         ( f4 : D → A) ( f5 : E → F) ( f6 : F → C) 
62         ( f7 : B → C) ( f8 : F → G) ( f9 : G → J)
63         (f10 : I → J) (f11 : J → I) (f12 : I → H) 
64         (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L :=
65 begin
66   cc,
67 end
68