dsimp が効きそうで効かない例

inductive MyNat : Type where
  | zero : MyNat
  | succ : MyNat → MyNat

namespace MyNat

def add (m n : MyNat) : MyNat :=
  match n with
  | zero => m
  | succ n => succ (add m n)

instance : OfNat MyNat 0 where
  ofNat := .zero

instance : OfNat MyNat 1 where
  ofNat := .succ .zero

instance : Add MyNat where
  add := MyNat.add

@[simp] theorem add_zero (n : MyNat) : n + 0 = n := by rfl
@[simp] theorem zero_add (n : MyNat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    dsimp [Add.add, MyNat.add]
    -- goal state: 0 + n.succ = n.succ
    -- why goal is not changed?

    rw [show 0 + n.succ = .succ (0 + n) from by rfl]
    rw [ih]

Start from the supplied MyNat.zero_add proof and reproduce the goal after dsimp [Add.add, MyNat.add]. Check the surrounding Lean example or documentation to determine why the goal remains unchanged, then update the explanation or example so the expected simplification and proof outcome are clear.