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

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]


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
rfl


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

rw [add_succ]
induction d with d hd
rfl

• Can you explain better the problem? If you want to prove 0+d=d by induction (that is a very good idea), the two cases should be 0+0=0 and 0 + succ d = succ d knowing that 0 + d = d. Jan 19 at 15:54
• Ah, I see, you are trying to prove even the induction step by induction. Well, this is not a very good idea. But notice that you now have a new assumption! Jan 19 at 16:01
• Just use induction once :-) Jan 19 at 16:23

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

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.