import MyNat.Power
import MultiplicationWorld.Level2 -- mul_one
namespace MyNat
open MyNat

Power World

Level 4: one_pow

Lemma

For all naturals m, 1 ^ m = 1.

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

Next up Level 5