nth_rw broken?

Stream: mathlib4

[Michael Stoll]

I think I may have seen a thread on that, but can't find it (searching for nth_rw or nth_rewrite om Zulip seems to ignore the nth_ part...).
The following certainly does not work as expected.

import Mathlib

example (x y z : ℤ) : x^2 + y^2 = x^2 + y*y := by
  nth_rw 2 [pow_two] -- leaves `x ^ 2 + y ^ 2 = x * x + y * y`
  sorry

It seems that nth_rw n [lemma] finds the first match for the lemma (here x^2) and then rewrites the nth occurrence of that match instead of the nth occurrence of some match.
Is this a know bug (and if so, is something being done about it)?

[Patrick Massot]

Yes, it is known.

[Patrick Massot]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/How.20to.20use.20nth_rewrite.20in.20NNG4.3F/near/397991051

[Scott Morrison]

In particular for anyone coming to this thread later, lean4#2539 is the fix.