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.

[paulch42]

The following proof works (only change is in the last few lines):

theorem mul_left_cancel (a b c : MyNat) (ha : a ≠ 0) : a * b = a * c → b = c := by
  induction c generalizing b with
  | zero =>
    rw [zero_is_0]
    rw [mul_zero]
    intro h
    cases (eq_zero_or_eq_zero_of_mul_eq_zero _ _ h) with
    | inl h1 =>
      exfalso
      apply ha
      assumption
    | inr h2 =>
      assumption
  | succ d hd =>
    intro hb
    cases b with
    | zero =>
      rw [zero_is_0] at hb
      rw [mul_zero] at hb
      rw [zero_is_0]
      exfalso
      apply ha
      have hb := hb.symm
      cases (eq_zero_or_eq_zero_of_mul_eq_zero _ _ hb) with
      | inl h =>
        exact h
      | inr h =>
        exfalso
        exact succ_ne_zero _ h
    | succ c =>
      rw [mul_succ] at hb
      rw [mul_succ] at hb
      have aceqad := add_right_cancel _ _ _ hb
      have ceqd := hd c aceqad
      rw [ceqd]

There is also a missing import for add_right_cancel - AdvancedAdditionWorld.Level5.