import MyNat.Power
import MyNat.Multiplication
import PowerWorld.Level5 -- pow_add
namespace MyNat
open MyNat

Power World

Level 7: pow_pow

Boss level! What will the collectible be?

Lemma

For all naturals a, m, n, we have (a ^ m) ^ n = a ^ {mn}.

lemma 
pow_pow: ∀ (a m n : MyNat), (a ^ m) ^ n = a ^ (m * n)
pow_pow (
a: MyNat
a 
m: MyNat
m 
n: MyNat
n : 
MyNat: Type
MyNat) : (
a: MyNat
a ^ 
m: MyNat
m) ^ 
n: MyNat
n = 
a: MyNat
a ^ (
m: MyNat
m * 
n: MyNat
n) := by
a, m, n: MyNat
(a ^ m) ^ n = a ^ (m * n)
  induction 
n: MyNat
n with
a, m, n: MyNat
(a ^ m) ^ n = a ^ (m * n)
  | 
zero: MyNat
zero =>
a, m: MyNat
zero
(a ^ m) ^ zero = a ^ (m * zero)
    rw [
a, m: MyNat
zero
(a ^ m) ^ zero = a ^ (m * zero)
zero_is_0: zero = 0
zero_is_0
a, m: MyNat
zero
(a ^ m) ^ 0 = a ^ (m * 0)]
a, m: MyNat
zero
(a ^ m) ^ 0 = a ^ (m * 0)
    rw [
a, m: MyNat
zero
(a ^ m) ^ 0 = a ^ (m * 0)
mul_zero: ∀ (a : MyNat), a * 0 = 0
mul_zero
a, m: MyNat
zero
(a ^ m) ^ 0 = a ^ 0]
a, m: MyNat
zero
(a ^ m) ^ 0 = a ^ 0
    repeat
a, m: MyNat
zero
(a ^ m) ^ 0 = a ^ 0 rw [
a, m: MyNat
zero
1 = a ^ 0
pow_zero: ∀ (m : MyNat), m ^ 0 = 1
pow_zero
Goals accomplished! 🐙]
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
n: MyNat
n 
ih: (a ^ m) ^ n = a ^ (m * n)
ih =>
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
(a ^ m) ^ succ n = a ^ (m * succ n)
    rw [
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
(a ^ m) ^ succ n = a ^ (m * succ n)
pow_succ: ∀ (m n : MyNat), m ^ succ n = m ^ n * m
pow_succ
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
(a ^ m) ^ n * a ^ m = a ^ (m * succ n)]
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
(a ^ m) ^ n * a ^ m = a ^ (m * succ n)
    rw [
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
(a ^ m) ^ n * a ^ m = a ^ (m * succ n)
ih: (a ^ m) ^ n = a ^ (m * n)
ih
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
a ^ (m * n) * a ^ m = a ^ (m * succ n)]
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
a ^ (m * n) * a ^ m = a ^ (m * succ n)
    rw [
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
a ^ (m * n) * a ^ m = a ^ (m * succ n)
mul_succ: ∀ (a b : MyNat), a * succ b = a * b + a
mul_succ
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
a ^ (m * n) * a ^ m = a ^ (m * n + m)]
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
a ^ (m * n) * a ^ m = a ^ (m * n + m)
    rw [
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
a ^ (m * n) * a ^ m = a ^ (m * n + m)
pow_add: ∀ (a m n : MyNat), a ^ (m + n) = a ^ m * a ^ n
pow_add
a, m, n: MyNat
ih: (a ^ m) ^ n = a ^ (m * n)
succ
a ^ (m * n) * a ^ m = a ^ (m * n) * a ^ m]
Goals accomplished! 🐙

Apparently Lean can't find a collectible, even though you feel like you just finished power world so you must have proved something. What should the collectible for this level be called?

But what is this? It's one of those twists where there's another boss after the boss you thought was the final boss! Go to the next level!

Next up Level 8