How to rewrite when names do not match

Stream: new members

[Timo Schneider]

I am new to lean and I have a very basic question:

theorem plus_0_n (n:nat): 0+n = n :=
begin
induction n, refl, generalize : n_n.succ = n_n, exact n_ih,
end

I get stuck in this proof, because the names of the variables do not match up, i.e. my induction hypothesis is 0 + n_n = n_n , and n_n : nat. But somehow lean does not want to apply this to the goal, rewriting n_n.succ to n_n - (which I find strange, since both are of type nat). When I try to use the generalize tactic lean changes the name to n_n1, again not allowing me to use rewrite.

Can someone point me to the right tactic to use here?

[Johan Commelin]

You need to do something before you can apply the induction hypothesis

[Johan Commelin]

n_ih is only about n_n, not about n_n + 1.

[Timo Schneider]

Johan Commelin said:

You need to do something before you can apply the induction hypothesis

Yes, I think I want to get this into a form like succ(0+n) = succ(n), in coq I can do so using simplification:

Theorem plus_O_n : forall n : nat, n + 0 = n.
Proof.
  intros n. induction n. reflexivity.
  simpl. rewrite IHn. reflexivity. Qed.

I guess i need a small theorem to rewrite the goal first in lean.

[Johan Commelin]

@Timo Schneider Right. So just tell lean. (In this case it will work.)

show succ (0 + n_n) = succ n_n,

[Timo Schneider]

Johan Commelin [said](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic

Thanks, I got it to work now, but I need to read a bit more about the show tactic to understand what it does.

theorem plus_0_n (n:nat): 0+n = n :=
begin
induction n, refl, show nat.succ (0 + n_n) = nat.succ n_n, simp, assumption,
end