nth_rewrite

Stream: mathlib4

[Kevin Buzzard]

a NNG user just reported this and it's reproducible in mathlib:

import Mathlib.Tactic

example (b c : ℕ) : 0 + b = 0 + c := by
  nth_rewrite 2 [zero_add]
/-
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  0 + b
b c : ℕ
⊢ 0 + b = 0 + c
-/

Is that expected behaviour? My guess is that Lean is deciding that it's going to be rewriting the second occurrence of 0 + b rather than the second occurrence of 0 + ?.

[Kim Morrison]

This is lean4#2539, which I'm trying to get merged. :-)

[Kevin Buzzard]

I added a link to @Nikolai Morin 's post on the issue.

[Michael Stoll]

Another thread.

[Michael Stoll]

And here.

[Kim Morrison]

Please make sure they are all linked at lean4#2539. :-)

[Kim Morrison]

Happily this has now been merged, as so will become available in Mathlib at the end of January.