import MyNat.Definition
import MultiplicationWorld.Level6 -- succ_mul
import MyNat.Multiplication -- mul_succ, mul_zero
import AdvancedMultiplicationWorld.Level2 -- eq_zero_or_eq_zero_of_mul_eq_zero
namespace MyNat
open MyNat

Advanced Multiplication World

Level 4: `mul_left_cancel`

This is the last of the bonus multiplication levels. mul_left_cancel will be useful in inequality world.

People find this level hard. I have probably had more questions about this level than all the other levels put together, in fact. Many levels in this game can just be solved by "running at it" -- do induction on one of the variables, keep your head, and you're done. In fact, if you like a challenge, it might be instructive if you stop reading after the end of this paragraph and try solving this level now by induction, seeing the trouble you run into, and reading the rest of these comments afterwards. This level has a sting in the tail. If you are a competent mathematician, try and figure out what is going on. Write down a maths proof of the theorem in this level. Exactly what statement do you want to prove by induction? It is subtle.

Ok so here are some spoilers. The problem with naively running at it, is that if you try induction on, say, c, then you are imagining a and b as fixed, and your inductive hypothesis P(c) is ab=ac ⟹ b=c. So for your inductive step you will be able to assume ab=ad ⟹ b=d and your goal will be to show ab=a(d+1) ⟹ b=d+1. When you also assume ab=a(d+1) you will realize that your inductive hypothesis is useless, because ab=ad is not true! The statement P(c) (with a and b regarded as constants) is not provable by induction.

What you can prove by induction is the following stronger statement. Imagine a ≠ 0 as fixed, and then prove "for all b, if ab=ac then b=c" by induction on c. This gives us the extra flexibility we require. Note that we are quantifying over all b in the inductive hypothesis -- it is essential that b is not fixed.

You can do this in two ways in Lean -- before you start the induction you can write revert b. The revert tactic is the opposite of the intro tactic; it replaces the b in the hypotheses with "for all b" in the goal.

Alternatively, you can write induction c generalizing b with as the first line of the proof.

If you do not modify your technique in this way, then this level seems to be impossible (judging by the comments I've had about it!)

Theorem

If a ≠ 0, b and c are natural numbers such that ab = ac, then b = c.

set_option trace.Meta.Tactic.simp true
theorem mul_left_cancel: ∀ (a b c : MyNat), a ≠ 0 → a * b = a * c → b = c
mul_left_cancel (a: MyNat
a b: MyNat
b c: MyNat
c : MyNat: Type
MyNat) (ha: a ≠ 0
ha : a: MyNat
a ≠ 0: MyNat
0) : a: MyNat
a * b: MyNat
b = a: MyNat
a * c: MyNat
c → b: MyNat
b = c: MyNat
c := bya, b, c: MyNat
ha: a ≠ 0
a * b = a * c → b = c
  induction c: MyNat
c generalizing b: MyNat
b witha, b, c: MyNat
ha: a ≠ 0
a * b = a * c → b = c
  | zero: MyNat
zero =>a: MyNat
ha: a ≠ 0
b: MyNat
zeroa * b = a * zero → b = zero
    rw [a: MyNat
ha: a ≠ 0
b: MyNat
zeroa * b = a * zero → b = zerozero_is_0: zero = 0
zero_is_0a: MyNat
ha: a ≠ 0
b: MyNat
zeroa * b = a * 0 → b = 0]a: MyNat
ha: a ≠ 0
b: MyNat
zeroa * b = a * 0 → b = 0
    rw [a: MyNat
ha: a ≠ 0
b: MyNat
zeroa * b = a * 0 → b = 0mul_zero: ∀ (a : MyNat), a * 0 = 0
mul_zeroa: MyNat
ha: a ≠ 0
b: MyNat
zeroa * b = 0 → b = 0]a: MyNat
ha: a ≠ 0
b: MyNat
zeroa * b = 0 → b = 0
    intro h: a * b = 0
ha: MyNat
ha: a ≠ 0
b: MyNat
h: a * b = 0
zerob = 0
    cases (eq_zero_or_eq_zero_of_mul_eq_zero: ∀ (a b : MyNat), a * b = 0 → a = 0 ∨ b = 0
eq_zero_or_eq_zero_of_mul_eq_zero _: MyNat
_ _: MyNat
_ h: a * b = 0
h) witha: MyNat
ha: a ≠ 0
b: MyNat
h: a * b = 0
x✝: a = 0 ∨ b = 0
zerob = 0
    | inl: ∀ {a b : Prop}, a → a ∨ b
inl h1: a = 0
h1 =>a: MyNat
ha: a ≠ 0
b: MyNat
h: a * b = 0
h1: a = 0
zero.inlb = 0
      exfalsoa: MyNat
ha: a ≠ 0
b: MyNat
h: a * b = 0
h1: a = 0
zero.inl.hFalse
      apply ha: a ≠ 0
haa: MyNat
ha: a ≠ 0
b: MyNat
h: a * b = 0
h1: a = 0
zero.inl.ha = 0
      assumptionGoals accomplished! 🐙
    | inr: ∀ {a b : Prop}, b → a ∨ b
inr h2: b = 0
h2 =>a: MyNat
ha: a ≠ 0
b: MyNat
h: a * b = 0
h2: b = 0
zero.inrb = 0
      assumptionGoals accomplished! 🐙
  | succ: MyNat → MyNat
succ d: MyNat
d hd: ∀ (b : MyNat), a * b = a * d → b = d
hd =>a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
b: MyNat
succa * b = a * succ d → b = succ d
    intro hb: a * b = a * succ d
hba: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
b: MyNat
hb: a * b = a * succ d
succb = succ d
    cases b: MyNat
b witha: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
b: MyNat
hb: a * b = a * succ d
succb = succ d
    | zero: MyNat
zero =>a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: a * zero = a * succ d
succ.zerozero = succ d
      rw [a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: a * zero = a * succ d
succ.zerozero = succ dzero_is_0: zero = 0
zero_is_0a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: a * 0 = a * succ d
succ.zerozero = succ d]a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: a * 0 = a * succ d
succ.zerozero = succ d at hb: a * zero = a * succ d
hba: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: a * 0 = a * succ d
succ.zerozero = succ d
      rw [a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: a * 0 = a * succ d
succ.zerozero = succ dmul_zero: ∀ (a : MyNat), a * 0 = 0
mul_zeroa: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: 0 = a * succ d
succ.zerozero = succ d]a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: 0 = a * succ d
succ.zerozero = succ d at hb: a * 0 = a * succ d
hba: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: 0 = a * succ d
succ.zerozero = succ d
      rw [a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: 0 = a * succ d
succ.zerozero = succ dzero_is_0: zero = 0
zero_is_0a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: 0 = a * succ d
succ.zero0 = succ d]a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: 0 = a * succ d
succ.zero0 = succ d
      exfalsoa: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: 0 = a * succ d
succ.zero.hFalse
      apply ha: a ≠ 0
haa: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb: 0 = a * succ d
succ.zero.ha = 0
      have hb: a * succ d = 0
hb := hb: 0 = a * succ d
hb.symm: ∀ {α : Type} {a b : α}, a = b → b = a
symma: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb✝: 0 = a * succ d
hb: a * succ d = 0
succ.zero.ha = 0
      cases (eq_zero_or_eq_zero_of_mul_eq_zero: ∀ (a b : MyNat), a * b = 0 → a = 0 ∨ b = 0
eq_zero_or_eq_zero_of_mul_eq_zero _: MyNat
_ _: MyNat
_ hb: a * succ d = 0
hb) witha: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb✝: 0 = a * succ d
hb: a * succ d = 0
x✝: a = 0 ∨ succ d = 0
succ.zero.ha = 0
      | inl: ∀ {a b : Prop}, a → a ∨ b
inl h: a = 0
h =>a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb✝: 0 = a * succ d
hb: a * succ d = 0
h: a = 0
succ.zero.h.inla = 0
        exact h: a = 0
hGoals accomplished! 🐙
      | inr: ∀ {a b : Prop}, b → a ∨ b
inr h: succ d = 0
h =>a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb✝: 0 = a * succ d
hb: a * succ d = 0
h: succ d = 0
succ.zero.h.inra = 0
        exfalsoa: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
hb✝: 0 = a * succ d
hb: a * succ d = 0
h: succ d = 0
succ.zero.h.inr.hFalse
        exact succ_ne_zero: ∀ (a : MyNat), succ a ≠ 0
succ_ne_zero _: MyNat
_ h: succ d = 0
hGoals accomplished! 🐙
    | succ: MyNat → MyNat
succ c: MyNat
c =>a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
c: MyNat
hb: a * succ c = a * succ d
succ.succsucc c = succ d
      have h: Prop
h := c: MyNat
c = d: MyNat
da: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
c: MyNat
hb: a * succ c = a * succ d
h: Prop
succ.succsucc c = succ d
      apply hd: ∀ (b : MyNat), a * b = a * d → b = d
hdError: tactic 'apply' failed, failed to unify
  ?b = d
with
  succ c = succ d
case succ.succ
a : MyNat
ha : a ≠ 0
d : MyNat
hd : ∀ (b : MyNat), a * b = a * d → b = d
c : MyNat
hb : a * succ c = a * succ d
h : Prop
⊢ succ c = succ d
a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
c: MyNat
hb: a * succ c = a * succ d
h: Prop
succ.succsucc c = succ d
      rw [mul_succ] at hb
      rw [mul_succ] at hb
      apply add_right_cancel _ _ _ hb
      rw [h]a: MyNat
ha: a ≠ 0
d: MyNat
hd: ∀ (b : MyNat), a * b = a * d → b = d
c: MyNat
hb: a * succ c = a * succ d
h: Prop
succ.succsucc c = succ d

You should now be ready for Inequality World.

The Lean Natural Numbers

Advanced Multiplication World

Level 4: mul_left_cancel

Theorem

Level 4: `mul_left_cancel`