The Lean Natural Numbers

import MyNat.Addition
import MyNat.Multiplication
namespace MyNat
open MyNat

Level 1: zero_mul

Lemma

For all natural numbers m, we have 0 * m = 0.

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

Next up is Multiplication Level 2.