import MyNat.Addition
import MyNat.Multiplication
import MultiplicationWorld.Level1 -- zero_mul
import MultiplicationWorld.Level6 -- succ_mul
namespace MyNat
open MyNat

Multiplication World

Level 7: add_mul

We proved mul_add already, but because we don't have commutativity yet we also need to prove add_mul. We have a bunch of tools now, so this won't be too hard. You know what -- you can do this one by induction on any of the variables. Try them all! Which works best? If you can't face doing all the commutativity and associativity, remember the high-powered simp tactic mentioned at the bottom of Addition World level 6, which will solve any puzzle which needs only commutativity and associativity. If your goal looks like a+(b+c)=c+b+a or something, don't mess around doing it explicitly with add_comm and add_assoc, just try simp.

Lemma

Addition is distributive over multiplication. In other words, for all natural numbers a, b and t, we have (a + b) * t = at + bt.

lemma 
add_mul: ∀ (a b t : MyNat), (a + b) * t = a * t + b * t
add_mul (
a: MyNat
a 
b: MyNat
b 
t: MyNat
t : 
MyNat: Type
MyNat) : (
a: MyNat
a + 
b: MyNat
b) * 
t: MyNat
t = 
a: MyNat
a * 
t: MyNat
t + 
b: MyNat
b * 
t: MyNat
t := by
a, b, t: MyNat
(a + b) * t = a * t + b * t
  induction 
b: MyNat
b with
a, b, t: MyNat
(a + b) * t = a * t + b * t
  | 
zero: MyNat
zero =>
a, t: MyNat
zero
(a + zero) * t = a * t + zero * t
    rw [
a, t: MyNat
zero
(a + zero) * t = a * t + zero * t
zero_is_0: zero = 0
zero_is_0
a, t: MyNat
zero
(a + 0) * t = a * t + 0 * t]
a, t: MyNat
zero
(a + 0) * t = a * t + 0 * t
    rw [
a, t: MyNat
zero
(a + 0) * t = a * t + 0 * t
zero_mul: ∀ (m : MyNat), 0 * m = 0
zero_mul
a, t: MyNat
zero
(a + 0) * t = a * t + 0]
a, t: MyNat
zero
(a + 0) * t = a * t + 0
    rw [
a, t: MyNat
zero
(a + 0) * t = a * t + 0
add_zero: ∀ (a : MyNat), a + 0 = a
add_zero
a, t: MyNat
zero
a * t = a * t + 0]
a, t: MyNat
zero
a * t = a * t + 0
    rw [
a, t: MyNat
zero
a * t = a * t + 0
add_zero: ∀ (a : MyNat), a + 0 = a
add_zero
a, t: MyNat
zero
a * t = a * t]
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
b: MyNat
b 
ih: (a + b) * t = a * t + b * t
ih =>
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
(a + succ b) * t = a * t + succ b * t
    rw [
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
(a + succ b) * t = a * t + succ b * t
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
succ (a + b) * t = a * t + succ b * t]
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
succ (a + b) * t = a * t + succ b * t
    rw [
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
succ (a + b) * t = a * t + succ b * t
succ_mul: ∀ (a b : MyNat), succ a * b = a * b + b
succ_mul
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
(a + b) * t + t = a * t + succ b * t]
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
(a + b) * t + t = a * t + succ b * t
    rw [
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
(a + b) * t + t = a * t + succ b * t
ih: (a + b) * t = a * t + b * t
ih
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
a * t + b * t + t = a * t + succ b * t]
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
a * t + b * t + t = a * t + succ b * t
    rw [
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
a * t + b * t + t = a * t + succ b * t
succ_mul: ∀ (a b : MyNat), succ a * b = a * b + b
succ_mul
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
a * t + b * t + t = a * t + (b * t + t)]
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
a * t + b * t + t = a * t + (b * t + t)
    rw [
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
a * t + b * t + t = a * t + (b * t + t)
add_assoc: ∀ (a b c : MyNat), a + b + c = a + (b + c)
add_assoc
a, t, b: MyNat
ih: (a + b) * t = a * t + b * t
succ
a * t + (b * t + t) = a * t + (b * t + t)]
Goals accomplished! 🐙

A mathematician would now say that you have proved that the natural numbers are a semiring. This sounds like a respectable result.

def 
right_distrib: ∀ (a b t : MyNat), (a + b) * t = a * t + b * t
right_distrib := 
add_mul: ∀ (a b t : MyNat), (a + b) * t = a * t + b * t
add_mul -- alternative name

-- instance : semiring MyNat := by structure_helper
-- BUGBUG

Lean would add that you have also proved that they are a distrib. However this concept has no mathematical name at all -- this says something about the regard with which mathematicians hold this collectible. This is an artifact of the set-up of collectibles in Lean. You consider politely declining Lean's offer of a distrib collectible. You are dreaming of the big collectible at the end of Power World.

-- instance : distrib MyNat := by structure_helper --
-- BUGBUG

On to Level 8