import MyNat.Addition
import MyNat.Multiplication
import MultiplicationWorld.Level5
import MultiplicationWorld.Level8
namespace MyNat
open MyNat

Multiplication World

Level 9: mul_left_comm

You are equipped with

  • mul_assoc (a b c : MyNat) : (a * b) * c = a * (b * c)
  • mul_comm (a b : MyNat) : a * b = b * a

Re-read the docs for rw so you know all the tricks. You can see them in the Tactics section on the left.

Lemma

For all natural numbers a b and c, we have a(bc) = b(ac)

lemma 
mul_left_comm: ∀ (a b c : MyNat), a * (b * c) = b * (a * c)
mul_left_comm (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) : 
a: MyNat
a * (
b: MyNat
b * 
c: MyNat
c) = 
b: MyNat
b * (
a: MyNat
a * 
c: MyNat
c) := 
a, b, c: MyNat
a * (b * c) = b * (a * c)

  
a, b, c: MyNat
a * (b * c) = b * (a * c)
a, b, c: MyNat
a * b * c = b * (a * c)
a, b, c: MyNat
a * b * c = b * (a * c)

  
a, b, c: MyNat
a * b * c = b * (a * c)
a, b, c: MyNat
b * a * c = b * (a * c)
a, b, c: MyNat
b * a * c = b * (a * c)

  
a, b, c: MyNat
b * a * c = b * (a * c)
a, b, c: MyNat
b * (a * c) = b * (a * c)
Goals accomplished! 🐙

And now you can teach the simp tactic these new tricks:

attribute [simp] 
mul_assoc: ∀ (a b c : MyNat), a * b * c = a * (b * c)
mul_assoc 
mul_comm: ∀ (a b : MyNat), a * b = b * a
mul_comm 
mul_left_comm: ∀ (a b c : MyNat), a * (b * c) = b * (a * c)
mul_left_comm

and all of a sudden Lean can automatically do levels which are very boring for a human, for example:

example: ∀ (a b c d e : MyNat), a * b * c * d * e = c * (b * e * a) * d
example (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c 
d: MyNat
d 
e: MyNat
e : 
MyNat: Type
MyNat) :
  (((
a: MyNat
a*
b: MyNat
b)*
c: MyNat
c)*
d: MyNat
d)*
e: MyNat
e=(
c: MyNat
c*((
b: MyNat
b*
e: MyNat
e)*
a: MyNat
a))*
d: MyNat
d := 
a, b, c, d, e: MyNat
a * b * c * d * e = c * (b * e * a) * d

  
Goals accomplished! 🐙

If you feel like attempting Advanced Multiplication world you'll have to do Function World and the Proposition Worlds first. These worlds assume a certain amount of mathematical maturity (perhaps 1st year undergraduate level).

Your other possibility is Power World.