import MyNat.Addition
import MyNat.Multiplication
import AdditionWorld.Level1 -- zero_add
import AdditionWorld.Level5 -- one_eq_succ_zero, succ_eq_add_one
namespace MyNat
open MyNat

Multiplication World

Level 3: one_mul

These proofs from addition world might be useful here:

• one_eq_succ_zero : 1 = succ 0
• succ_eq_add_one a : succ a = a + 1

We just proved mul_one, now let's prove one_mul. Then we will have proved, in fancy terms, that 1 is a "left and right identity" for multiplication (just like we showed that 0 is a left and right identity for addition with add_zero and zero_add).

Lemma

For any natural number m, we have 1 * m = m.

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

Next up is Multiplication Level 4.