Need help with induction proof in Lean for $0+d=d$

Question

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

Answer 1

I managed to figure it out.

Going back to proving $0+\operatorname{succ}(d)=\operatorname{succ}(d)$, it turns out all I needed to do was rw [add_succ] to turn it into $\operatorname{succ}(0+d)=\operatorname{succ}(d)$ and then use rw [hd] to turn it into $\operatorname{succ}(d)=\operatorname{succ}(d)$ (because I forgot to rewrite what I had as the hypothesis because I could have done that in the first place) and then I could use rfl to finally complete my proof by induction.

Full proof (plus original step proving $0+n=n$):

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

Where I probably went wrong in my original attempt:

succ_eq_add_one doesn't help because then I am going to be stuck proving that $0+d+1$ is identical to $d+1$, which in turn looped me back to where I had started.