natural-number-game

Solututions to the Natural Number Game
power.lean (1311B)

 1 lemma zero_pow_zero : 0 ^ 0 = 1 :=
 2 begin
 3   rw pow_zero,
 4   refl,
 5 end
 6 
 7 lemma zero_pow_succ (m : ℕ) : 0 ^ (succ m) = 0 :=
 8 begin
 9   rw pow_succ,
10   rw mul_zero,
11   refl,
12 end
13 
14 lemma pow_one (a : ℕ) : a ^ 1 = a :=
15 begin
16   rw one_eq_succ_zero,
17   rw pow_succ,
18   rw pow_zero,
19   rw one_mul,
20   refl,
21 end
22 
23 lemma one_pow (m : ℕ) : 1 ^ m = 1 :=
24 begin
25   induction m,
26   rw pow_zero,
27   refl,
28   rw pow_succ,
29   rw m_ih,
30   rw mul_one,
31   refl,
32 end
33 
34 lemma pow_add (a m n : ℕ) : a ^ (m + n) = a ^ m * a ^ n :=
35 begin
36   induction n,
37   rw add_zero,
38   rw pow_zero,
39   rw mul_one,
40   refl,
41   rw add_succ,
42   repeat {rw pow_succ},
43   rw ← mul_assoc,
44   rw n_ih,
45   refl,
46 end
47 
48 lemma mul_pow (a b n : ℕ) : (a * b) ^ n = a ^ n * b ^ n :=
49 begin
50   induction n,
51   repeat {rw pow_zero},
52   rw mul_one,
53   refl,
54   repeat {rw pow_succ},
55   rw n_ih,
56   simp,
57 end
58 
59 lemma pow_pow (a m n : ℕ) : (a ^ m) ^ n = a ^ (m * n) :=
60 begin
61   induction n,
62   rw mul_zero,
63   repeat {rw pow_zero},
64   rw mul_succ,
65   rw pow_add,
66   rw pow_succ,
67   rw n_ih,
68   refl,
69 end
70 
71 lemma add_squared (a b : ℕ) : (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b :=
72 begin
73   rw two_eq_succ_one,
74   rw one_eq_succ_zero,
75   repeat {rw pow_succ},
76   repeat {rw pow_zero},
77   repeat {rw one_mul},
78   repeat {rw succ_mul},
79   rw zero_mul,
80   rw zero_add,
81   rw mul_add,
82   repeat {rw add_mul},
83   simp,
84 end