## 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: Aug 03 2023 at 10:10 UTC