How can I apply a rewrite to only one term?

Question

In Lean I occasionally want to apply a rw tactic to exactly one of multiple identical terms. For example I have the goal

⊢ 0 = 0

and I want to rw it to

⊢ a * 0 = 0

I also have

mul_zero (a : mynat) :
  a * 0 = 0

Now I should be able to just rewrite the 0 to a * 0. However trying

rw ← zero_mul a,

gives me

⊢ a * 0 = a * 0

Which is not what I want!

Is there a reason lean does this and is there some way to apply a rewrite to only one term?

Hidie

Answer 1

rw rewrites all identical terms simultaneously. There is a different tactic nth_rewrite which only rewrites a specific occurrence of a term. You need mathlib for nth_rewrite, and I'm not sure if it is available in the Natural Number Game.

import tactic
example : 0 = 0 :=
begin
  nth_rewrite 0 [← nat.mul_zero 2],
  -- ⊢ 2 * 0 = 0
end

Weaks

it is available in the Natural Number game – Horbal

Answer 2

You can use the conv tactics for this

lemma a : 0 = 0 :=
begin
  conv {
    to_lhs, 
    rw ← nat.mul_zero 2,
  },
end

see: https://leanprover-community.github.io/extras/conv.html

Diffuse