Tutorial World

Level 1: the refl tactic.

refl,

Level 2: The rewrite (rw) tactic.

rw h,
refl,

Level 3: Peano’s axioms.

rw h,
refl,

Level 4: addition

rw add_succ,
rw add_zero,
refl,

Addition World

Level 1: the induction tactic.

induction n with d hd,
rw add_zero,
refl,

rw add_succ,
rw hd,
refl,

Level 2: add_assoc — associativity of addition.

induction c with d hd,
rw add_zero,
rw add_zero,
refl,

rw add_succ,
rw add_succ,
rw add_succ,
rw hd,
refl,

Level 3: succ_add

induction b with d hd,
rw add_zero,
rw add_zero,
refl,

rw add_succ,
rw hd,
rw add_succ,
refl,

Level 4: add_comm (boss level)

induction a with d hd,
rw zero_add,
rw add_zero,
refl,

rw succ_add,
rw add_succ,
rw hd,
refl,

Level 5: succ_eq_add_one

induction n with d hd,
rw zero_add,
refl,

rw succ_add,
rw hd,
refl,

Level 6: add_right_comm

induction c with d hd,
rw add_comm,
rw add_comm (a + 0),
rw zero_add,
rw add_zero,
rw add_comm,
refl,

rw add_succ,
rw add_succ,
rw succ_add,
rw hd,
refl,

Function World

Level 1: the exact tactic.

exact h(p),

Level 2: the intro tactic.

intro n,
exact n+1,

Level 3: the have tactic.

have q:=h(p),
have t:=j(q),
have u:=l(t),
exact u,

Level 4: the apply tactic.

apply l,
apply j,
apply h,
exact p,

Level 5: P → (Q → P).

intros p q,
exact p,

Level 6: (P → (Q → R)) → ((P → Q) → (P → R)).

intros f1 f2 p,
have j := f1 p,
apply j,
apply f2,
exact p,

Level 7: (P → Q) → ((Q → F) → (P → F))

intros f1 f2 p,
apply f2,
apply f1,
exact p,

Level 8: (P → Q) → ((Q → empty) → (P → empty))

intros f1 f2 p,
apply f2,
apply f1,
exact p,

Level 9: a big maze.

intro a,
apply f15,
apply f11,
apply f9,
apply f8,
apply f5,
apply f2,
apply f1,
exact a,

Proposition World

Level 1: the exact tactic.

apply h,
exact p,

Level 2: intro.

intro p,
exact p,

Level 3: have.

have q := h(p),
have t := j(q),
have u := l(t),
exact u,

Level 4: apply.

apply l,
apply j,
apply h,
exact p,

Level 5 : P → (Q → P).

intros p q,
exact p,

Level 6: (P → (Q → R)) → ((P → Q) → (P → R)).

intros f1 f2 p,
apply f1,
exact p,

apply f2,
exact p,

Level 7: (P → Q) → ((Q → R) → (P → R))

intros pq qr p,
apply qr,
apply pq,
exact p,

Level 8 : (P → Q) → (¬ Q → ¬ P)

repeat {rw not_iff_imp_false},
intros pq qf p,
apply qf,
apply pq,
exact p,

Level 9: a big maze.

intro a,
apply f15,
apply f11,
apply f9,
apply f8,
apply f5,
apply f2,
apply f1,
exact a,

Advanced Proposition World

Level 1: the split tactic.

split,
exact p,
exact q,

Level 2: the cases tactic.

intro h,
cases h with p q,
split,
exact q,
exact p,

Level 3: and_trans.

intros pq qr,
cases pq with p q,
cases qr with q r,
split,
exact p,
exact r,

Level 4: iff_trans.

intros cpq cqr,
cases cpq with pq qp,
cases cqr with qr rq,
split,
intro p,
apply qr,
apply pq,
exact p,

intro r,
apply qp,
apply rq,
exact r,

Level 5: iff_trans easter eggs.

intros hpq hqr,
split,
intro p,
apply hqr.1,
apply hpq.1,
exact p,

intro r,
apply hpq.2,
apply hqr.2,
exact r,

Level 6: Or, and the left and right tactics.

intro q,
right,
exact q,

Level 7: or_symm

intro pq,
cases pq with p q,
right,
exact p,

left,
exact q,

Level 8: and_or_distrib_left

split,
intro pqr,
cases pqr with p qr,
cases qr with q r,
left,
split,
exact p,
exact q,

right,
split,
exact p,
exact r,

intro pqpr,
cases pqpr with pq pr,
cases pq with p q,
split,
exact p,

left,
exact q,

cases pr with p r,
split,
exact p,

right,
exact r,

Level 9: exfalso and proof by contradiction.

intro pnp,
cases pnp with p np,
rw not_iff_imp_false at np,
exfalso,
apply np,
exact p,

Level 10: the law of the excluded middle.

by_cases p : P; by_cases q : Q,
repeat {cc},

Advanced Addition World

Level 1: succ_inj. A function.

exact succ_inj(hs),

Level 2: succ_succ_inj.

apply succ_inj,
apply succ_inj,
exact h,

Level 3: succ_eq_succ_of_eq.

intro ab,
cases ab with a b,
refl,

Level 4: eq_iff_succ_eq_succ

split,
exact succ_inj,
exact succ_eq_succ_of_eq,

Level 5: add_right_cancel

intro atbt,
induction t with d hd,
cases atbt with a b,
rw add_zero at atbt,
refl,

rw add_succ at atbt,
rw add_succ at atbt,
cc,

Level 6: add_left_cancel

intro tatb,
induction t with d hd,
rw zero_add at tatb,
rw zero_add at tatb,
cc,

rw succ_add at tatb,
rw succ_add at tatb,
cc,

Level 7: add_right_cancel_iff

split,
exact add_right_cancel _ _ _,
cc,