abel_nf bug

Stream: mathlib4

[Heather Macbeth]

This seems to be a bug in abel_nf -- I can't investigate it immediately, but recording it now in case someone can!

example {E : Type*} [AddCommGroup E] (y z : E) (P : E → Prop) :
    P (y - z + z) := by
  abel_nf
  sorry

This produces ⊢ P (y + -1 • z + z), but surely it ought to produce ⊢ P y.

[Aaron Liu]

concerning

import Mathlib

example {E : Type*} [AddCommGroup E] (y z : E) :
    y - z + z = y := by
  -- `abel` works but `abel_nf` does not
  -- abel
  -- abel_nf
  sorry

[Heather Macbeth]

#29778 fixes this bug.