Rewriting in just one place (newbie)

Stream: new members

[Cris Perdue]

I am playing around with the natural numbers game online, trying out variations on some proofs.
I want to rewrite a hypothesis

ab : b + a = a

using zero_add, to get ab: b + a = 0 + a

with the step: rw ← zero_add a at ab,

I get: ab : b + (0 + a) = 0 + a (rewriting both occurrences of "a")

Is there a nice idiom that would give the desired result?

[Martin Dvořák]

You might try change for definitional equivalence or convert_to for other other. The latter might create additional goals.

[Martin Dvořák]

There is also nth_rewrite which first takes a zero-based index and then a rewrite lemma.

[Kevin Buzzard]

zero_add isn't definitional and NNG is running on a very old Lean so might well not have convert_to or nth_rewrite

[Kevin Buzzard]

The way I usually solve this sort of thing in NNG is have ab' : b + a = 0 + a, and prove this with rw zero_add, exact ab.

[Patrick Johnson]

NNG has tactic#conv

conv at ab {to_rhs, rw ←zero_add a}

[Kevin Buzzard]

indeed conv was in core Lean 3.4.1

[Cris Perdue]

Thanks much!