import MyNat.Power
import MultiplicationWorld.Level2 -- mul_one
import MultiplicationWorld.Level9 -- simp additions
namespace MyNat
open MyNat

Power World

Level 6: mul_pow

Here we use the attribute [simp] additions we made in level 9 of Multiplication World so that the simp tactic can simplify expressions involving *.

Lemma

For all naturals a, b, n, we have (ab) ^ n = a ^ nb ^ n.

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

Next up Level 7