id in proofs generated by tactics

Stream: general

[Gihan Marasingha]

Printing the proof of foo below gives foo1. In this case, id can be removed. Are there cases where it's important that the proof generated by rw employs id?

Or, to rephrase the question, why does the generated proof use id?

lemma foo (x y : nat): x + y = y + x :=
by rw nat.add_comm

lemma foo1 : ∀ (x y : ℕ), x + y = y + x :=
λ (x y : ℕ),
  @eq.mpr (x + y = y + x) (y + x = y + x)
    (@id (x + y = y + x = (y + x = y + x))
       (@eq.rec ℕ (x + y) (λ (_a : ℕ), x + y = y + x = (_a = y + x)) (@eq.refl Prop (x + y = y + x)) (y + x)
          (@nat.add_comm x y)))
    (@eq.refl ℕ (y + x))

[Floris van Doorn]

I believe the id is to help the type-checker, by giving exactly the expected type of the term it is applied to.

[Mario Carneiro]

It's especially important in long proofs by dsimp, because without it the kernel can get lost figuring out why a long transitivity chain is defeq