Incorrect proof in NaturalNumbers

[paulch42]

In level 4 of Advanced Multiplication World there is a proof of:

theorem mul_left_cancel (a b c : MyNat) (ha : a ≠ 0) : a * b = a * c → b = c

Near the end of the proof is the line apply hd which is flagged in VS Code as an error with the message:

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

Using a clone of the latest lean4-samples from GitHub.