Natural Number Game Level 4

Stream: general

[Icaro Costa]

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 succ_eq_add_one},
repeat {rw mul_add},
repeat {rw mul_one},
repeat {rw add_right_cancel_iff},


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]

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]

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