Need help with tutorial

Stream: new members

[Leandro Caniglia]

This is level 3 of Advanced Addition World

Objects:
xy: ℕ
Assumptions:
a: x + y = y
Goal:
x = 0

I would like to replace the RHS y of Assumption a with 0 + y, using something like \l zero_add. All my attempts failed. How can I do that?

[Ruben Van de Velde]

You should be able to use nth_rewrite instead

[Leandro Caniglia]

Ruben Van de Velde said:

You should be able to use nth_rewrite instead

When I try

nth_rewrite 3 [← zero_add] at a

I get

tactic 'rewrite' failed, pattern is a metavariable
  ?n
from equation
  ?n = 0 + ?n
xy: ℕ
a: x + y = y
⊢ x = 0

[Mario Carneiro]

try using zero_add y instead of just zero_add, which will apply to every term

[Leandro Caniglia]

Mario Carneiro said:

try using zero_add y instead of just zero_add, which will apply to every term

Thanks! That worked

nth_rewrite 2 [← zero_add y] at a