So I have been trying to learn Lean and have managed to find this resource called the "Natural Number Game" which is supposed to help me learn Lean.

I am learning Lean to help me understand the art of proof writing, which has never really been a strong suit of mine, as well as to learn how to use a proof assistant.

Now, it has been going pretty well so far (except for proving $2+2=4$, which took me around a half hour) except now I'm stuck trying to prove $0+n=n$ by induction.

I have been able to prove the two intermediate steps (for $0+n=n$ and $0+\operatorname{succ}(d)=\operatorname{succ}(d)$), but I don't know how to prove it for $\operatorname{succ}(0+\operatorname{succ}(d))=\operatorname{succ}(\operatorname{succ}(d))$. Here is what I have tried so far:

rw [succ_eq_add_one]
rw [one_eq_succ_zero]
rw [add_succ]
rw [add_zero]

although I must have done something wrong, since I ended up with $\operatorname{succ}(0+\operatorname{succ}(d))=\operatorname{succ}(\operatorname{succ}(d))$, which is what I want to prove. My question is: What am I doing wrong here that made me end up with the original statement that I wanted to prove, and how do I prove that $\operatorname{succ}(0+\operatorname{succ}(d))=\operatorname{succ}(\operatorname{succ}(d))$?

Here is the code from proving the intermediate steps:

First intermediate step ($0+n=n$)

induction n with d hd
rw [add_zero]
rfl

Second intermediate step ($0+\operatorname{succ}(d)=\operatorname{succ}(d)$)

rw [add_succ]
induction d with d hd
rw [add_zero]
rfl