import MyNat.Addition
import MyNat.Multiplication
import MultiplicationWorld.Level1
import MultiplicationWorld.Level6
namespace MyNat
open MyNat

Multiplication World

Level 8: mul_comm

Finally, the boss level of multiplication world. But you are well-prepared for it -- you have zero_mul and mul_zero, as well as succ_mul and mul_succ. After this level you can of course throw away one of each pair if you like, but I would recommend you hold on to them, sometimes it's convenient to have exactly the right tools to do a job.

Lemma

Multiplication is commutative.

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

You've now proved that the natural numbers are a commutative semiring! That's the last collectible in Multiplication World.

-- instance MyNat.comm_semiring : comm_semiring MyNat := by structure_helper
-- BUGBUG

But don't leave multiplication just yet -- prove mul_left_comm, the last level of the world, and then we can beef up the power of simp.

On to Level 9