## Stream: general

### Topic: Natural Number Game Level 4

#### Icaro Costa (Jan 22 2023 at 20:14):

I am solving the last level of the (Advanced Multiplication World)[https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=9&level=4]

This is what I have so far:

theorem mul_left_cancel (a b c : mynat) (ha : a  0) : a * b = a * c  b = c :=
begin
induction c with d hd generalizing b,
rw mul_zero,
intro g,
rw mul_eq_zero_iff at g,
cases g,
exfalso,
exact ha g,
rw g,
refl,

cases b,
intro g,
rw mul_zero at g,
symmetry at g,
rw mul_eq_zero_iff at g,
cases g,
exfalso,
exact ha g,
exfalso,
exact succ_ne_zero d g,

repeat {rw mul_one},

end

With state

case mynat.succ
a : mynat,
ha : a  0,
d : mynat,
hd :  (b : mynat), a * b = a * d  b = d,
b : mynat
a * b = a * d  b = d

I was expecting to do something like exact hd to finish the proof, but the forall symbol doesn't match. What to do in this situation?

#### Yaël Dillies (Jan 22 2023 at 20:16):

exact hd b to feed in b to hd, or alternatively exact hd _ to let Lean figure that it should set b := b

#### Icaro Costa (Jan 22 2023 at 20:16):

Yaël Dillies said:

exact hd b to feed in b to hd, or alternatively exact hd _ to let Lean figure that it should set b := b

Oh yeah, thanks

Last updated: Dec 20 2023 at 11:08 UTC