Natural Numbers
❱
Addition World
❱
Multiplication World
❱
Power World
❱
Function World
❱
Proposition World
❱
Advanced Proposition World
❱
Advanced Addition World
❱
Advanced Multiplication World
❱
Inequality World
❱
Tactics
❱

The Lean Natural Numbers

import MyNat.Power
import MyNat.Addition -- add_zero
import MultiplicationWorld.Level2 -- mul_one
import MultiplicationWorld.Level5 -- mul_assoc
namespace MyNat
open MyNat

Power World

Level 5: `pow_add`

Lemma

For all naturals a, m, n, we have a^(m + n) = a ^ m a ^ n.

lemma pow_add: ∀ (a m n : MyNat), a ^ (m + n) = a ^ m * a ^ n
pow_add (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 * a: MyNat
a ^ n: MyNat
n := bya, m, n: MyNat
a ^ (m + n) = a ^ m * a ^ n
  induction n: MyNat
n witha, m, n: MyNat
a ^ (m + n) = a ^ m * a ^ n
  | zero: MyNat
zero =>a, m: MyNat
zeroa ^ (m + zero) = a ^ m * a ^ zero
    rw [a, m: MyNat
zeroa ^ (m + zero) = a ^ m * a ^ zerozero_is_0: zero = 0
zero_is_0a, m: MyNat
zeroa ^ (m + 0) = a ^ m * a ^ 0]a, m: MyNat
zeroa ^ (m + 0) = a ^ m * a ^ 0
    rw [a, m: MyNat
zeroa ^ (m + 0) = a ^ m * a ^ 0add_zero: ∀ (a : MyNat), a + 0 = a
add_zeroa, m: MyNat
zeroa ^ m = a ^ m * a ^ 0]a, m: MyNat
zeroa ^ m = a ^ m * a ^ 0
    rw [a, m: MyNat
zeroa ^ m = a ^ m * a ^ 0pow_zero: ∀ (m : MyNat), m ^ 0 = 1
pow_zeroa, m: MyNat
zeroa ^ m = a ^ m * 1]a, m: MyNat
zeroa ^ m = a ^ m * 1
    rw [a, m: MyNat
zeroa ^ m = a ^ m * 1mul_one: ∀ (m : MyNat), m * 1 = m
mul_onea, m: MyNat
zeroa ^ m = a ^ m]Goals accomplished! 🐙
  | succ: MyNat → MyNat
succ n: MyNat
n ih: a ^ (m + n) = a ^ m * a ^ n
ih =>a, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ (m + succ n) = a ^ m * a ^ succ n
    rw [a, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ (m + succ n) = a ^ m * a ^ succ nadd_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succa, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ succ (m + n) = a ^ m * a ^ succ n]a, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ succ (m + n) = a ^ m * a ^ succ n
    rw [a, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ succ (m + n) = a ^ m * a ^ succ npow_succ: ∀ (m n : MyNat), m ^ succ n = m ^ n * m
pow_succa, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ (m + n) * a = a ^ m * a ^ succ n]a, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ (m + n) * a = a ^ m * a ^ succ n
    rw [a, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ (m + n) * a = a ^ m * a ^ succ npow_succ: ∀ (m n : MyNat), m ^ succ n = m ^ n * m
pow_succa, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ (m + n) * a = a ^ m * (a ^ n * a)]a, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ (m + n) * a = a ^ m * (a ^ n * a)
    rw [a, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ (m + n) * a = a ^ m * (a ^ n * a)ih: a ^ (m + n) = a ^ m * a ^ n
iha, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ m * a ^ n * a = a ^ m * (a ^ n * a)]a, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ m * a ^ n * a = a ^ m * (a ^ n * a)
    rw [a, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ m * a ^ n * a = a ^ m * (a ^ n * a)mul_assoc: ∀ (a b c : MyNat), a * b * c = a * (b * c)
mul_assoca, m, n: MyNat
ih: a ^ (m + n) = a ^ m * a ^ n
succa ^ m * (a ^ n * a) = a ^ m * (a ^ n * a)]Goals accomplished! 🐙

Remember you can combine all the rw rules into one with rw [add_succ, pow_succ, pow_succ, ih, mul_assoc] but we have broken it out here so you can more easily see all the intermediate goal states.

Next up Level 6