https://adam.math.hhu.de/#/g/leanprover-community/nng4
Tutorial World
Level 1 / 8 : The rfl tactic
rfl
Level 2 / 8 : the rw tactic
rw[h]
rfl
Level 3 / 8 : Numbers
rw[two_eq_succ_one]
rw[one_eq_succ_zero]
rfl
Level 4 / 8 : rewriting backwards
rw[← one_eq_succ_zero]
rw[← two_eq_succ_one]
rfl
Level 5 / 8 : Adding zero
rw[add_zero b]
rw[add_zero c]
rfl
Level 6 / 8 : Precision rewriting
rw[add_zero b]
rw[add_zero c]
rfl
Level 7 / 8 : add_succ
rw[one_eq_succ_zero]
rw[add_succ]
rw[add_zero]
rfl
Level 8 / 8 : 2+2=4
nth_rewrite 2 [two_eq_succ_one]
rw[add_succ 2]
nth_rewrite 1 [one_eq_succ_zero]
rw[add_succ 2]
rw[add_zero 2]
rw[<- three_eq_succ_two]
rw[<- four_eq_succ_three]
rfl
Addition World
Level 1 / 5 : zero_add
induction n with d hd
rw[add_zero]
rfl
rw[add_succ 0]
rw[hd]
rfl
Level 2 / 5 : succ_add
induction b with d hd
rw[succ_eq_add_one]
rw[succ_eq_add_one]
rw[add_zero]
rw[add_zero]
rfl
rw[add_succ]
rw[add_succ]
rw[hd]
rfl
Level 3 / 5 : add_comm (level boss)
induction b with d hd
rw[add_zero]
rw[zero_add]
rfl
rw[add_succ]
rw[hd]
rw[succ_add]
rfl
Level 4 / 5 : add_assoc (associativity of addition)
induction b with d hd
rw[add_zero]
rw[zero_add]
rfl
rw[succ_add]
rw[add_succ]
rw[succ_add]
rw[add_succ]
rw[hd]
rfl
Level 5 / 5 : add_right_comm
induction b with d hd
rw[add_zero]
rw[add_zero]
rfl
rw[add_succ]
rw[succ_add]
rw[hd]
rw[add_succ]
rfl